Two threads of research have been pursued in parallel in logic and artificial intelligence. On the one hand, in artificial intelligence, logic-based theories have been developed to study and formalize belief change and the so-called “common sense reasoning”, i.e. the actual reasoning of humans. On the other hand, in logic, substructural logics, i.e. logics lacking some of the structural rules of classical logic, have been studied in depth from a theoretical point of view. However, the powerful (prooftheoretical) techniques and methods developed in logic have not yet been applied to artificial intelligence. Conditional logic and belief revision theory are prominent theories in artificial intelligence dealing with common sense reasoning. We show in this article that they can both be embedded within the framework of substructural logics and can both be seen as extensions of the Lambek calculus. This allows us to compare and relate them to each other systematically, via a natural formalization of the Ramsey test. I thank Philippe Besnard for discussions. I thank three anonymous reviewers for comments.
In everyday life, the way we update and revise our beliefs plays an important role in our representation of the surrounding world and therefore also in our decision making process. This has lead researchers in artificial intelligence and computer science to develop logic-based theories that study and formalize belief change and the so-called “common sense reasoning”. The rationale underlying the development of such theories is that it would ultimately help us understand our everyday life reasoning and the way we update our beliefs, and that the resulting work could subsequently lead to the development of tools that could be used for example by artificial agents in order to act autonomously in an uncertain and changing world.
A number of theories have been proposed to capture
different kinds of updates and the reasoning styles that they
induce, using di erent formalisms and under various
assumptions: dynamic epistemic logic [van Benthem, 2011], default
and non-monotonic logics [Makinson, 2005], belief revision
theory [Ga¨rdenfors, 1988], conditional logic [Nute and Cross,
2001], etc. . . However, a generic and general framework
encompassing all these theories is still lacking. Instead, the
current state of the art is such that we are left with various
formalisms which are di cult to relate formally to each other
despite numerous attempts [Makinson and Ga¨rdenfors, 1989;
Aucher, 2004; Baltag and Smets, 2008], partly because they
rely on di erent kinds of formalisms. This is problematic if
logic is to be viewed ultimately as a unified and unifying field
and if we want to avoid that logic goes on “riding o madly
in all directions”
Our objective in this article is to show that conditional logic and belief revision can be reformulated meaningfully and naturally within the very general framework of substructural logics [Restall, 2000]. More specifically, we will show that conditional logic and belief revision theory are extensions of the well-known Lambek calculus with appropriate structural inference rules. This will allow us to compare and relate them to each other systematically. In particular, our approach will shed new lights on Ga¨rdenfors’ impossibility theorem that draws attention to certain formal di culties in defining a conditional connective from a revision operation, via the Ramsey test. We will also pinpoint the key to non-monotonicity and we will show that it depends crucially on a constrained application of the (left) weakening rule.
Other proof theoretical approaches to non-monotonic reasoning have already been proposed, notably by Bonatti and Olivetti [2002][1992]. However, they deal with nonmonotonicity at the meta-logical level by introducing specific inference relations like j or B. Instead of it, we will deal with non-monotonicity at the object-language level by means of the substructural connective and the introduction of appropriate structural rules.
The article is organized as follows. In Section 2, we briefly recall elementary notions of substructural logics and we observe that the ternary relation can be interpreted intuitively as a kind of update. In Section 3, we recall the basics of conditional logic and belief revision theory and recall how they are formally connected. In Section 4, we show how each of them can be embedded within the framework of substructural logic that was introduced in Section 2 by adding specific structural inference rules. In Section 5, we discuss Ga¨rdenfors’ impossibility theorem. Finally, we conclude in Section 6.
Substructural logics are a family of logics lacking some of the structural rules of classical logic. A structural rule is a rule of inference which is closed under substitution of formulas. The structural rules for classical logic are given in Fig. 1: they are called Weakening, Contraction, Permutation and Associativity (see Definition 2 for explanations about the notations used). The comma in these sequents has to be interpreted as a conjunction in an antecedent and as a disjunction in a consequent. While Weakening and Contraction are often dropped like in relevance logic and linear logic, the rule of Associativity is often preserved. When some of these rules are dropped, the comma ceases to behave as a conjunction (in the antecedent) or a disjunction (in the succedent). In that case, the comma corresponds to other substructural connectives and we often introduce new punctuation marks which do not fulfill all these structural rules to deal with these new substructural connectives.
Our exposition of substructural logics is based on [Restall,
2000, 2006]
In the sequel, P is a non-empty and finite set of propositional letters.
Definition 1 (Language L ; ; ). The language L ; ; is defined inductively by the following grammar in BNF: ' ::= (' ?
j ') j (' p
j (' ^ ') j (' ! ') ') j (' ') where p ranges over P. Also, ! is material implication whereas and are Lambek implications. If Con f^; ! ; ; ; g, then the language LCon is the language L ; ; restricted to the connectives of Con. The propositional language LPL is the language LCon with Con := f^; !g.
We will use the following abbreviations: :' := ' ! ?, > := :?, ' $ := (' ! ) ^ ( ! '), and ' _ := :(:'^: ). We use the following ranking of binding strength for parenthesis: :; ; ; ; ^; _; !; $.
Definition 2 (LCon–structure, LCon–sequent and LCon–hypersequent). Let Con f^; !; ; ; g. LCon– structures are defined by the following grammar in BNF: SRLCon : Y ::= ' j (Y ; Y)
SLLCon : X ::= ' j (X ; X) j (X ; X) where ' ranges over LCon. [X] denotes a LCon–structure containing as substructure the LCon–structure X, and [Z] denotes the LCon–structure [X] where X is uniformly substituted by the structure Z. LCon–structures are denoted U; X; Y or Z and we write ' 2 X when ' is a substructure of X.
A LCon–sequent is an expression of the form X Y, Y or X
where X 2 SLLCon , Y 2 SRLCon . A LCon– hypersequent has the form X1 Y1 : : :
Xn
Yn where X1 Y1; : : : Xn Yn are LCon–sequents.
fined inductively as follows: d(') := 0, d((X ; Y)) = maxfd(X); d(Y)g and d((X ; Y)) := maxfd(X); d(Y)g + 1. The depth of a LCon–sequent X Y is defined by d(X Y) := maxfd(X); d(Y)g.
The semantics of substructural logics is based on the ternary relation of the frame semantics for relevant logic originally introduced by Routley and Meyer [1972a,b, 1973]; Routley et al. [1982].
Definition 3 (Point set). A point set P = (P; v) is a set P together with a partial order v on P. We abusively write x 2 P for x 2 P.
The partial order v (introduced for dealing with intuitionistic reasoning) will not be used in this article.
Definition 4 (Model). A model is a tuple M = (P; R; I) where:
P = (P; v) is a point set; I : P ! 2P is an interpretation function;
R P P P is a ternary relation on P.
We abusively write x 2 M for x 2 P, and (M; x) is called a pointed model.
A model stripped out from its interpretation corresponds to
a frame as defined in [Restall, 2000, Def. 11.8] without truth
sets
Definition 5 (Truth conditions). Let M be a model, x 2 M and ' 2 L ; ; . The relation M; x ' is defined inductively as follows:
M; x M; x M; x M; x M; x M; x
M; x Let Con tion
M; x M; x
Let X model.
M; x
M; x
never ? p
i p 2 I(x) ' ^ i M; x ' and M; x ' ! i if M; x ' then M; x ' i there are y; z 2 P such that Ryzx;
M; y ' and M; z ' i for all y; z 2 P where Rxyz;
if M; y ' then M; z ' i for all y; z 2 P where Ryxz
if M; y ' then M; z f^; !; ; ; g. We extend the scope of the relato also relate points to LCon–structures:
X ; Y X ; Y i i
M; x X and M; x Y there are y; z 2 M such that Ryzx;
M; y X and M; z Y X
Y be a LCon–sequent and let (M; x) be a pointed We say that X Y is true at (M; x), written
Y, when the following holds: X
Y i if M; x X, then there is ' 2 Y such that M; x ': written X1 Xn
Yn. that the LCon–hypersequent X1
when for all pointed models (M; x), M; x X Y. We say Y1 : : : Xn Yn is valid, Y1 : : :
Xn
Yn, when X1
Y1 or . . . or
Here is a key inference of substructural logics, more precisely of the Lambek Calculus: ; ' i '
The ternary relation of the Routley and Meyer semantics was
introduced originally for technical reasons: any 2-ary (n-ary)
connective of a logical language can be given a semantics by
resorting to a 3-ary (resp. n + 1-ary) relation on worlds.
Subsequently, a number of philosophical interpretations of this
ternary relation have been proposed
I proposed in [Aucher, 2014] a new dynamic interpretation. The proposal is based on the observation that an update can be represented abstractly as a ternary relation: the first argument of the ternary relation represents the initial situation/state, the second the event that occurs in this initial situation (the informative input) and the third the resulting situation/state after the occurrence of the event. With this interpretation in mind, Rxyz reads as ‘the occurrence of event y in world x results in the world z’ and the corresponding conditional ' reads as ‘the occurrence in the current world of an event satisfying property ' results in a world satisfying ’.
This interpretation is coherent with a number of interpretations of the ternary relation proposed in substructural logic. Keeping in mind the truth conditions for the connective of Definition 5, the following quote makes perfect sense: “To be committed to A B is to be committed to B whenever we gain the information that A. To put it another way, a body of information warrants A B if and only if whenever you update that information with new information which warrants A, the resulting (perhaps new) body of information warrants B.” (my emphasis) [Restall, 2006, p. 362]
Our sequent calculus extends the Lambek calculus with propositional connectives.
Definition 6 (Sequent calculi LCon). Let Con f^; !; ; ; g. The sequent calculus for LCon, denoted LCon, is the sequent calculus of Fig. 1 whose logical rules are restricted to the rules for the connectives of Con. The sequent calculus for propositional logic (where Con := f^; !g) is denoted LPL.
A LCon–sequent X Y is provable in LCon, written X LCon Y, when it can be derived from the axioms and inference rules of LCon in a finite number of steps. A formula ' 2 LCon is LCon–consistent when it is not the case that ' LCon . We also write LCon X for > LCon X.
Note that the following rules are derivable in LPL: X ; '
Y [']
U
Theorem 2
_L: :R U U U X X X X X Y
Default reasoning, sometimes identified with non-monotonic reasoning and formalized by conditional logics, involves making default assumptions and reasoning with the most typical or “normal” situations. Belief revision, on the other hand, deals with the representation of mechanisms for revising our beliefs. Even if the phenomena that are studied seem to be di erent, we will see in Section 3.3 that default reasoning and belief revision are in fact “two sides of the same coin”. 3.1
Default reasoning arises frequently in everyday life. It involves leaping to conclusions. For example, if an agent sees a bird, she may conclude that it flies. However, not all birds fly: penguins and ostriches do not fly, nor do newborn birds, dead birds, or birds made of clay. Nevertheless, birds typically fly, and by default, in everyday life, we often reason with such abusive simplifications that are revised only after we receive more information. This explains informally why default reasoning is non-monotonic: adding new information may withdraw and invalidate some of our previous inferences. Definition 7 (Language for defaults LDEF). The language for defaults is defined by LDEF := f'; ' j '; 2 LPLg.
The formula ' can be read in various ways, depending on the application. For example, it can be read as “if ' (is the case) then typically (is the case)”, “if ', then normally ”, “if ', then by default ”, and “if ', then is very likely”.
Numerous semantics have been proposed for default
statements, such as preferential structures [Kraus et al., 1990],
semantics [Adams, 1975], the possibilistic structures [Dubois
and Prade, 1991] and -ranking [Spohn, 1988]. They all have
in common that they define the same set of validities
axiomatized by the same proof system P
Definition 8 (System P). The proof system P for LDEF is defined by the following axiom and inference rules, where all formulas are propositional.
If LPL ' $ '0, then from ' ! 0, then from ' infer '0 infer ' 1 and '
and '2 1 and ' 2 infer '
infer '1 _ '2 2 infer ' ^ 2 1 ^ 2 3.2
In the so-called AGM belief revision theory of Alchourro´n et al. [1985], the beliefs of the agent are represented by a belief set, denoted K . These propositional formulas represent the beliefs of the agent. The revision of K with ', written K ', consists of adding ' to K , but in order that the resulting set be consistent, some formulas are removed from K . Because this can be done in various ways, 8 AGM rationality postulates have been elicited as reasonable principles for revision.
If LPL '
' From ' From '1 From ' 1: 0 (LLE) (RW) (REF) (AND) (OR) (CM)
Formally, A belief set K is a set of propositional formulas of LPL such that Cn(K ) = K (where Cn(K ) := n' 2 LPL j '1 ; : : : ; 'n LPL ' for some '1; : : : ; 'n 2 K o). Let K be a belief set and let ' 2 LPL. As argued by Katsuno and Mendelzon, because P is finite, a belief set K can be equivalently represented by a mere propositional formula . This formula is also called a belief base. Then, ' 2 K if and only if ' 2 Cn( ).
We define the expansion of K by ', written K + ', as
follows: K + ' = Cn(K [ f'g). Then, one can easily show that
2 K + ' if and only if 2 Cn( ^ '). So, in this approach,
the expansion of the belief base by ' is the belief base ^',
which is possibly an inconsistent formula. Now, given a
belief base and a formula ', ' denotes the revision of by
'. But in this case, ' is supposed to be consistent if ' is.
Given a revision operation on belief sets, one can define a
corresponding revision operation on belief bases as follows:
' ! if, and only if, 2 Cn( ) '. Then, we have that:
Lemma 3
' is also LPL–consistent $ 0 and ' $ '0, ' $
0 '0 ') ^ '0 !
A well-known result, originally suggested by Ramsey [1929], connects closely non-monotonic reasoning with belief revision. Informally, from ' I can non-monotonically infer if, and only if, I believe after revising my belief base with '. This lead Makinson and Ga¨rdenfors [1989][1991] to show formally that non-monotonic reasoning and belief revision are “two sides of the same coin”.
Theorem 4
Suppose that a revision operation satisfies (R1)–(R6). Fix a belief base , and define a relation on propositional formulas by taking ' to hold i ' ! . Then, satisfies all the properties of P as well as Rational Monotonicity:
if ' Moreover, ' 1 and not '
: 2; then ' ^ 2 1 ? if, and only if, ' is not satisfiable. (Rat) Conversely, suppose that is a relation on formulas that satisfies the properties of P and Rational Monotonicity (Rat), and ' ? if, and only if, ' is not satisfiable. Let K = f 2 LPL j > g. Then, K is a belief set. Let be its corresponding belief base. Then, if is defined by taking ' ! if, and only if, ! (' ), then the postulates (R1)–(R6) hold for and . 1 ' 2 ; ' 2 2 L
W0
L ^R W0
L _L
U
Y (W ; (X ; Z))
Y ((W ; X); Z)
RM We show that the main systems of common sense reasoning can be reformulated in the proof-theoretical setting of substructural logics.
Because we resort to the structural connective ; we need to introduce and add the logical connective to the system P: Definition 9 (Proof systems P+ and LP+ ).
The calculus P+ for L ; is the calculus P to which we add the following (bidirectional) inference rule:
i (RT2) ' ! ! ' The sequent calculus LP+ for L is the sequent calculus L where the structural rules are restricted to the L – sequents of depth 0, with rules R1 and W0L of Fig. 2. Proposition 5. The cut rule can be eliminated from any proof of LP+ . Moreover, all the rules of LP+ are invertible. Proof sketch. It can be adapted from [Restall, 2000, Th. 6.11] and [Troelstra and Schwichtenberg, 2000, Prop. 3.5.4].
LP+ ' i
P+ ' Proof. In this proof and the following, we will use the mappings t1 : SLLCon ! LCon and t2 : SRLCon ! LCon defined inductively as follows: t1(') := ' t2(') := ' t1(X ; Y) := t1(X) ^ t1(Y) t2(X ; Y) := t2(X) _ t2(Y) t1(X ; Y) := t1(X) t1(Y) We can prove by induction on the number of steps used that X LCon Y i
t1(X) LCon t2(Y)
The proof of Theorem 6 is by induction on the number of inference steps used in a proof. This boils down to show that each rule of inference and each axiom of LP+ is derivable in P+, and, vice versa, each rule and each axiom of P+ is derivable in LP+ . First, we prove that rules (LLE), (RW), (REF), (CM), (AND) and (OR) are derivable in LP+ (in this order): '0 ' ' ' ; '0 '0 ' ; ' 1 L
W0
L W0
L As for rule (RT2), because the rules of LP+ are invertible (Proposition 5), we have that ; ' LP+ i LP+ ' , by rule R. We derive (RT2) by applying Expression 1. The derivability of modus ponens follows from the cut rule.
Now, consider the right to left direction. Cut elimination holds for LP+ (Proposition 5) and LP+ satisfies the subformula LP+ ' property. Because what we prove is of the form with ; '; 2 LPL, this entails that the L –sequent will all be of depth at most 1 (see Definition 2). So, in what follows, we only consider L –structures of depth at most 1.
The rules of LPL are all derivable in P+, because LPL P+. We consider the rules R; L; R1 and W0L (we do not consider Cut because of Proposition 5). First, we prove that R is derivable in P+, the proof for L is similar. Assume that X ; LP+ '; we must prove that X LP+ '. That is, by Expression 1, we must prove that from t1(X) ! ', we can infer t1(X) ! ( ') in P+. This last inference follows from (RT2) of P+. Second, we consider R1. Assume that X LP+ Y; we must prove that (Z ; X) LP+ Y. That is, by Expression 1 and (RT2), we must prove that from t1(X) ! t2(Y) ( ), we can infer t1(Z) ! (t1(X) t2(Y)) ( ). By (RW) and (REF), we can prove t1(X) t2(Y) from ( ), and therefore also ( ). Third, we consider W0L. Assume that (X ; Y) LP+ U, we must prove that (X ; Z) ; Y LP+ U. That is, by Expression 1 and (RT2), we must prove that from t1(X) LP+ t1(Y) we can prove t1(X) ^ t1(Z) LP+ t1(Y) t2(U). This is true in t2(U) ( )
Based on the rationality postulates (R1)–(R6), we can define a Hilbert-like proof system. It is not a genuine Hilbert system because inference rules are not of the standard form: some premises refer to the satisfiability of formulas. This drawback is avoided in our sequent calculus reformulation by resorting to hypersequents [Pottinger, 1983; Avron, 1996].1 Definition 10 (Proof systems AGM and LAGM).
L 1In all the hypersequent calculi that we define in the sequel 1 R (based on already defined sequent calculi) we always take the internal version of the structural rules. See [Avron, 1996] for details. (1)
LPL.
' ' '; 2 ' ' ^ 2 '
WL ^L R6 ; ' ' '
^R ; ' ' '
^ ' ^ ' ; ' ^ ' ; ' ^ ' ' ! ^ ' ^ ' ^ '
Rb2 L ^L !R
; ('; '0) ( ; '); '0 ( '; '0 ( ') ^ '0 ' ' '0 '0 '; '0 ' ^ '0
culus of propositional logic to which we add the axioms and inference rules (R1)–(R6) of Lemma 3 (where LPL– consistency is replaced by AGM–consistency).
calculus L to which we add the rules of Figure 3. Proposition 7. The cut rule can be eliminated from any proof of LAGM. Moreover, all the rules of LAGM are invertible. Proof sketch. Similar to the proof of Proposition 5.
' LAGM i ' AGM Proof sketch. The proof follows the same methodology as Theorem 6. For the left to right direction, we prove (R1), (R4), (R2) (a and b) and (R5) (rule (R6) is proved similarly). ' ' ; ' ' ' ' ' ! '
R1 L !R 1
2 '1 '2 1 ; '1 1 '1 2 '2 2 '2 rules are invertible (Proposition 7), we have that ; ' LAGM . So, by Rule R3, we have that ' LAGM .
The right to left direction is proved similarly and relies also on the fact that (hyper)sequents are of depth 1 because of our cut elimination result (Proposition 7). ( ') ^ '0 ! ' LAGM . Then, because the logical We are going to reformulate Theorem 4 in our sequent calculi, and obtain a new formalization of the Ramsey test. Note the similarity between Expressions (RT1), (RT2) and (RT3). Definition 11 (Hypersequent calculus LNMR). The hypersequent calculus LNMR for L is the sequent calculus LP+ to which we add the structural rule (RM) of Fig. 2.
Theorem 9 (Ramsey test). Let ; '; lowing holds:
LNMR ' i ' LAGM (RT3) Proof sketch. We define the Hilbert calculus NMR := LP+ + (RM). Theorem 4 can be reformulated in our setting as follows: if ; '; 2 LPL, then NMR ' i ' AGM . So, if we prove that NMR and LNMR are provably equivalent, then we will have proved the theorem, because we already know by Theorem 6 that AGM and LAGM are provably equivalent. To prove that, it su ces to show that the inference rule (RM) is derivable in LNMR and, vice versa, that the inference rule (Rat) is derivable in NMR. It is proved without di culty. 5
As to the Ramsey test, a famous result [Ga¨rdenfors, 1988] states a di culty in introducing a connective such that ' 2 K i 2 K '. Indeed, an immediate consequence means that if K K 0 then K ' K 0 ', which is a property essentially incompatible with the AGM postulates for . Accordingly, we retrieve Ga¨rdenfors’ result as follows: > > > ? ? ; >
L
R3 >
Inconsistency of L ; extended with R3 reflects, in a way reminiscent of Ga¨rdenfors’ proof, that conditionals capturing defaults do not easily lend themselves to the role of premises. 6
Drawing intuitions from a dynamic interpretation of substructural concepts in terms of updating, we have reformulated conditional logic and belief revision in the substructural framework as extensions of the Lambek calculus. We thus retrieve some well-known results and provide new axiomatizations of belief revision and default reasoning.
In particular, our results show that the key to nonmonotonicity is a constrained application of the left weakening rule: our inferences stay the same if our knowledge of the initial situation is made more precise, but we may cancel some of them if we are forced to update our knowledge in face of new information (see rule W0L and definition of LP+ ).
The range of belief revision and default reasoning clearly calls for further work. For example, in our setting, given our reading of ternary relations as updates and given our truth conditions, the connective represents some sort of abduction (see Definition 5). This notion of abduction can now be studied within our substructural framework in interaction with the notions of revision, update and non-monotonicity.