=Paper=
{{Paper
|id=Vol-1423/paper1
|storemode=property
|title=When Conditional Logic and Belief Revision Meet Substructural Logics
|pdfUrl=https://ceur-ws.org/Vol-1423/DARe-15_1.pdf
|volume=Vol-1423
|dblpUrl=https://dblp.org/rec/conf/ijcai/Archer15
}}
==When Conditional Logic and Belief Revision Meet Substructural Logics==
https://ceur-ws.org/Vol-1423/DARe-15_1.pdf
When Conditional Logic and Belief Revision Meet Substructural Logics∗
Guillaume Aucher
University of Rennes 1
INRIA
Rennes, France
guillaume.aucher@irisa.fr
Abstract and non-monotonic logics [Makinson, 2005], belief revision
theory [Gärdenfors, 1988], conditional logic [Nute and Cross,
Two threads of research have been pursued in par-
2001], etc. . . However, a generic and general framework en-
allel in logic and artificial intelligence. On the one
compassing all these theories is still lacking. Instead, the cur-
hand, in artificial intelligence, logic-based theories
rent state of the art is such that we are left with various for-
have been developed to study and formalize belief
malisms which are difficult to relate formally to each other
change and the so-called “common sense reason-
despite numerous attempts [Makinson and Gärdenfors, 1989;
ing”, i.e. the actual reasoning of humans. On the
Aucher, 2004; Baltag and Smets, 2008], partly because they
other hand, in logic, substructural logics, i.e. log-
rely on different kinds of formalisms. This is problematic if
ics lacking some of the structural rules of classical
logic is to be viewed ultimately as a unified and unifying field
logic, have been studied in depth from a theoreti-
and if we want to avoid that logic goes on “riding off madly
cal point of view. However, the powerful (proof-
in all directions” (a metaphor used by van Benthem [2011]).
theoretical) techniques and methods developed in
logic have not yet been applied to artificial intel- Our objective in this article is to show that conditional logic
ligence. Conditional logic and belief revision the- and belief revision can be reformulated meaningfully and nat-
ory are prominent theories in artificial intelligence urally within the very general framework of substructural log-
dealing with common sense reasoning. We show in ics [Restall, 2000]. More specifically, we will show that con-
this article that they can both be embedded within ditional logic and belief revision theory are extensions of the
the framework of substructural logics and can both well-known Lambek calculus with appropriate structural in-
be seen as extensions of the Lambek calculus. This ference rules. This will allow us to compare and relate them
allows us to compare and relate them to each other to each other systematically. In particular, our approach will
systematically, via a natural formalization of the shed new lights on Gärdenfors’ impossibility theorem that
Ramsey test. draws attention to certain formal difficulties in defining a con-
ditional connective from a revision operation, via the Ramsey
test. We will also pinpoint the key to non-monotonicity and
1 Introduction we will show that it depends crucially on a constrained appli-
In everyday life, the way we update and revise our beliefs cation of the (left) weakening rule.
plays an important role in our representation of the surround- Other proof theoretical approaches to non-monotonic rea-
ing world and therefore also in our decision making process. soning have already been proposed, notably by Bonatti
This has lead researchers in artificial intelligence and com- and Olivetti [2002][1992]. However, they deal with non-
puter science to develop logic-based theories that study and monotonicity at the meta-logical level by introducing specific
formalize belief change and the so-called “common sense inference relations like |∼ or B. Instead of it, we will deal
reasoning”. The rationale underlying the development of with non-monotonicity at the object-language level by means
such theories is that it would ultimately help us understand of the substructural connective ⊃ and the introduction of ap-
our everyday life reasoning and the way we update our be- propriate structural rules.
liefs, and that the resulting work could subsequently lead to The article is organized as follows. In Section 2, we briefly
the development of tools that could be used for example by recall elementary notions of substructural logics and we ob-
artificial agents in order to act autonomously in an uncertain serve that the ternary relation can be interpreted intuitively as
and changing world. a kind of update. In Section 3, we recall the basics of condi-
A number of theories have been proposed to capture dif- tional logic and belief revision theory and recall how they are
ferent kinds of updates and the reasoning styles that they in- formally connected. In Section 4, we show how each of them
duce, using different formalisms and under various assump- can be embedded within the framework of substructural logic
tions: dynamic epistemic logic [van Benthem, 2011], default that was introduced in Section 2 by adding specific structural
∗
I thank Philippe Besnard for discussions. I thank three anony- inference rules. In Section 5, we discuss Gärdenfors’ impos-
mous reviewers for comments. sibility theorem. Finally, we conclude in Section 6.
2 Substructural Logics The semantics of substructural logics is based on the
Substructural logics are a family of logics lacking some of ternary relation of the frame semantics for relevant logic orig-
the structural rules of classical logic. A structural rule is a inally introduced by Routley and Meyer [1972a,b, 1973];
rule of inference which is closed under substitution of for- Routley et al. [1982].
mulas. The structural rules for classical logic are given in Definition 3 (Point set). A point set P = (P, v) is a set P
Fig. 1: they are called Weakening, Contraction, Permutation together with a partial order v on P. We abusively write x ∈ P
and Associativity (see Definition 2 for explanations about the for x ∈ P.
notations used). The comma in these sequents has to be inter- The partial order v (introduced for dealing with intuition-
preted as a conjunction in an antecedent and as a disjunction istic reasoning) will not be used in this article.
in a consequent. While Weakening and Contraction are often Definition 4 (Model). A model is a tuple M = (P, R, I)
dropped like in relevance logic and linear logic, the rule of where:
Associativity is often preserved. When some of these rules
• P = (P, v) is a point set;
are dropped, the comma ceases to behave as a conjunction
(in the antecedent) or a disjunction (in the succedent). In that • I : P → 2P is an interpretation function;
case, the comma corresponds to other substructural connec- • R ⊆ P × P × P is a ternary relation on P.
tives and we often introduce new punctuation marks which We abusively write x ∈ M for x ∈ P, and (M, x) is called a
do not fulfill all these structural rules to deal with these new pointed model.
substructural connectives. A model stripped out from its interpretation corresponds to
Our exposition of substructural logics is based on [Restall, a frame as defined in [Restall, 2000, Def. 11.8] without truth
2000, 2006] (see also Ono [1998] for a general introduction). sets (defined in [Restall, 2000, Def. 11.7]). Truth sets are not
2.1 Syntax and Semantics needed for what concerns us here.
In the sequel, P is a non-empty and finite set of propositional Definition 5 (Truth conditions). Let M be a model, x ∈ M
letters. and ϕ ∈ L◦,⊃,⊂ . The relation M, x ϕ is defined inductively
Definition 1 (Language L◦,⊃,⊂ ). The language L◦,⊃,⊂ is de- as follows:
fined inductively by the following grammar in BNF: M, x ⊥ never
ϕ ::= ⊥ | p | (ϕ ∧ ϕ) | (ϕ → ϕ) M, x p iff p ∈ I(x)
(ϕ ◦ ϕ) | (ϕ ⊃ ϕ) | (ϕ ⊂ ϕ) M, x ϕ ∧ ψ iff M, x ϕ and M, x ψ
where p ranges over P. Also, → is material implication M, x ϕ → ψ iff if M, x ϕ then M, x ψ
whereas ⊃ and ⊂ are Lambek implications. If Con ⊆ {∧, → M, x ϕ ◦ ψ iff there are y, z ∈ P such that Ryzx,
, ◦, ⊃, ⊂}, then the language LCon is the language L◦,⊃,⊂ re- M, y ϕ and M, z ψ
stricted to the connectives of Con. The propositional lan- M, x ϕ ⊃ ψ iff for all y, z ∈ P where Rxyz,
guage LPL is the language LCon with Con := {∧, →}. if M, y ϕ then M, z ψ
We will use the following abbreviations: ¬ϕ := ϕ → ⊥, M, x ψ ⊂ ϕ iff for all y, z ∈ P where Ryxz
> := ¬⊥, ϕ ↔ ψ := (ϕ → ψ) ∧ (ψ → ϕ), and ϕ ∨ ψ :=
if M, y ϕ then M, z ψ
¬(¬ϕ∧¬ψ). We use the following ranking of binding strength
for parenthesis: ¬, ◦, ⊃, ⊂, ∧, ∨, →, ↔. Let Con ⊆ {∧, →, ◦, ⊃, ⊂}. We extend the scope of the rela-
Definition 2 (LCon –structure, LCon –sequent and tion to also relate points to LCon –structures:
LCon –hypersequent). Let Con ⊆ {∧, →, ◦, ⊃, ⊂}. LCon – M, x X, Y iff M, x X and M, x Y
structures are defined by the following grammar in BNF: M, x X;Y iff there are y, z ∈ M such that Ryzx,
SLL
Con
: X ::= ϕ | (X, X) | (X ; X) M, y X and M, z Y
SR : Y ::= ϕ | (Y , Y)
LCon
Let X Y be a LCon –sequent and let (M, x) be a pointed
where ϕ ranges over LCon . Γ[X] denotes a LCon –structure model. We say that X Y is true at (M, x), written
containing as substructure the LCon –structure X, and Γ[Z] de- M, x X Y, when the following holds:
notes the LCon –structure Γ[X] where X is uniformly substi-
tuted by the structure Z. LCon –structures are denoted U, X, Y M, x X Y iff if M, x X, then there is ϕ ∈ Y
or Z and we write ϕ ∈ X when ϕ is a substructure of X. such that M, x ϕ.
A LCon –sequent is an expression of the form X Y, We say that the LCon –sequent X Y is valid, written X Y,
Y or X where X ∈ SL L
Con
, Y ∈ SLCon
R . A L Con – when for all pointed models (M, x), M, x X Y. We say
hypersequent has the form X1 Y1 . . . Xn Yn where that the LCon –hypersequent X1 Y1 . . . Xn Yn is valid,
X1 Y1 , . . . Xn Yn are LCon –sequents. written X1 Y1 . . . Xn Yn , when X1 Y1 or . . . or
The depth of a LCon –structure, denoted d(X), is de- Xn Yn .
fined inductively as follows: d(ϕ) := 0, d((X, Y)) =
Here is a key inference of substructural logics, more pre-
max{d(X), d(Y)} and d((X ; Y)) := max{d(X), d(Y)} + 1. The
cisely of the Lambek Calculus:
depth of a LCon –sequent X Y is defined by d(X Y) :=
max{d(X), d(Y)}. χ ; ϕ ψ iff χ ϕ ⊃ ψ (RT1)
2.2 Updates as Ternary Relations
The ternary relation of the Routley and Meyer semantics was Axioms:
introduced originally for technical reasons: any 2-ary (n-ary)
connective of a logical language can be given a semantics by
p p ⊥
resorting to a 3-ary (resp. n + 1-ary) relation on worlds. Sub-
sequently, a number of philosophical interpretations of this
Structural Rules:
ternary relation have been proposed (see [Beall et al., 2012;
Restall, 2006; Mares and Meyer, 2001] for more details).
Weakening: Contraction:
However, one has to admit that providing a non-circular and
conceptually grounded interpretation of this relation remains
problematic. Γ[X] U Γ[(X, X)] U
WL CL
I proposed in [Aucher, 2014] a new dynamic interpretation. Γ[(Y , X)] U Γ[X] U
The proposal is based on the observation that an update can be
represented abstractly as a ternary relation: the first argument U Γ[X] U Γ[(Y , Y)]
of the ternary relation represents the initial situation/state, the WR CR
second the event that occurs in this initial situation (the infor- U Γ[(X, Y)] U Γ[Y]
mative input) and the third the resulting situation/state after
the occurrence of the event. With this interpretation in mind, Permutation: Associativity:
Rxyz reads as ‘the occurrence of event y in world x results in
the world z’ and the corresponding conditional ϕ ⊃ ψ reads Γ[(Y , X)] Z Γ[X, (Y , Z)] U
as ‘the occurrence in the current world of an event satisfying PL BL
Γ[(X, Y)] Z Γ[(X, Y), Z] U
property ϕ results in a world satisfying ψ’.
This interpretation is coherent with a number of interpre-
tations of the ternary relation proposed in substructural logic. U Γ[(Y , X)] U Γ[(X, (Y , Z))]
PR BR
Keeping in mind the truth conditions for the connective ⊃ of U Γ[(X, Y)] U Γ[((X, Y), Z)]
Definition 5, the following quote makes perfect sense:
“To be committed to A ⊃ B is to be committed to B Cut Rule:
whenever we gain the information that A. To put it
another way, a body of information warrants A ⊃ B X ϕ Γ[ϕ] Y
if and only if whenever you update that information Cut
with new information which warrants A, the result- Γ[X] Y
ing (perhaps new) body of information warrants B.”
(my emphasis) [Restall, 2006, p. 362] Logical Rules:
2.3 Proof Systems Propositional Connectives:
Our sequent calculus extends the Lambek calculus with
propositional connectives. X, ψ ϕ Y ψ Γ[ϕ] X
→R →L
Definition 6 (Sequent calculi LCon ). Let Con ⊆ {∧, →, ◦, ⊃ X ψ→ϕ Γ[(ψ → ϕ, Y)] X
, ⊂}. The sequent calculus for LCon , denoted LCon , is the se-
quent calculus of Fig. 1 whose logical rules are restricted to X ϕ Y ψ Γ[(ϕ, ψ)] U
the rules for the connectives of Con. The sequent calculus for ∧R ∧L
propositional logic (where Con := {∧, →}) is denoted LPL . X, Y ϕ∧ψ Γ[(ϕ ∧ ψ)] U
A LCon –sequent X Y is provable in LCon , written
LCon Substructural Connectives:
X Y, when it can be derived from the axioms and in-
ference rules of LCon in a finite number of steps. A formula
X;ψ ϕ Y ψ Γ[ϕ] X
ϕ ∈ LCon is LCon –consistent when it is not the case that ⊃R ⊃L
ϕ
LCon
. We also write
LCon
X for >
LCon
X. X ψ⊃ϕ Γ[(ψ ⊃ ϕ ; Y)] X
Note that the following rules are derivable in LPL :
X ϕ Y ψ Γ[(ϕ ; ψ)] U
X, ϕ Y Γ[ϕ] U Γ[ψ] U ◦R ◦L
¬R ∨L . X;Y ϕ◦ψ Γ[(ϕ ◦ ψ)] U
X Y , ¬ϕ Γ[ϕ ∨ ψ] U
Theorem 1 (Cut elimination [Restall, 2000]). Let Con ⊆ ϕ;Y ψ X ϕ Γ[ψ] Y
{∧, →, ◦, ⊃, ⊂}. The cut rule can be eliminated from any proof ⊂R ⊂L
of LCon . Y ψ⊂ϕ Γ[(X ; ψ ⊂ ϕ)] Y
Theorem 2 (Soundness and completeness [Restall, 2000]).
Let Con ⊆ {∧, →, ◦, ⊃, ⊂}. Then, for all LCon -sequents Figure 1: Our Sequent Calculus
LCon
X Y, it holds that X Y iff X Y.
3 Conditional Logic and Belief Revision Formally, A belief set K is a set of propositional for-
Default reasoning, sometimes identified with non-monotonic mulas of LPL such that Cn(K) = K (where Cn(K) :=
LPL
n o
reasoning and formalized by conditional logics, involves ϕ ∈ LPL | ϕ1 , . . . , ϕn ϕ for some ϕ1 , . . . , ϕn ∈ K ). Let
making default assumptions and reasoning with the most typ- K be a belief set and let ϕ ∈ LPL . As argued by Katsuno and
ical or “normal” situations. Belief revision, on the other hand, Mendelzon, because P is finite, a belief set K can be equiv-
deals with the representation of mechanisms for revising our alently represented by a mere propositional formula χ. This
beliefs. Even if the phenomena that are studied seem to be formula is also called a belief base. Then, ϕ ∈ K if and only
different, we will see in Section 3.3 that default reasoning if ϕ ∈ Cn(χ).
and belief revision are in fact “two sides of the same coin”. We define the expansion of K by ϕ, written K + ϕ, as fol-
lows: K + ϕ = Cn(K ∪ {ϕ}). Then, one can easily show that
3.1 Conditional Logic ψ ∈ K + ϕ if and only if ψ ∈ Cn(χ ∧ ϕ). So, in this approach,
Default reasoning arises frequently in everyday life. It in- the expansion of the belief base χ by ϕ is the belief base χ∧ϕ,
volves leaping to conclusions. For example, if an agent sees which is possibly an inconsistent formula. Now, given a be-
a bird, she may conclude that it flies. However, not all birds lief base χ and a formula ϕ, χ ◦ ϕ denotes the revision of χ by
fly: penguins and ostriches do not fly, nor do newborn birds, ϕ. But in this case, χ ◦ ϕ is supposed to be consistent if ϕ is.
dead birds, or birds made of clay. Nevertheless, birds typ- Given a revision operation ∗ on belief sets, one can define a
ically fly, and by default, in everyday life, we often reason corresponding revision operation ◦ on belief bases as follows:
with such abusive simplifications that are revised only after χ ◦ ϕ → ψ if, and only if, ψ ∈ Cn(χ) ∗ ϕ. Then, we have that:
we receive more information. This explains informally why Lemma 3 (Katsuno and Mendelzon 1992). Let * be a revi-
default reasoning is non-monotonic: adding new information sion operation on belief sets and ◦ its corresponding opera-
may withdraw and invalidate some of our previous inferences. tion on belief bases. Then * satisfies the 8 AGM postulates if,
Definition 7 (Language for defaults LDEF ). The language for and only if, ◦ satisfies the postulates (R1)–(R6) below:
defaults is defined by LDEF := {ϕ, ϕ ⊃ ψ | ϕ, ψ ∈ LPL }. χ◦ϕ→ϕ (R1)
The formula ϕ ⊃ ψ can be read in various ways, depending if χ ∧ ϕ is LPL –consistent, then χ ◦ ϕ ↔ χ ∧ ϕ (R2)
on the application. For example, it can be read as “if ϕ (is the If ϕ is LPL –consistent,
case) then typically ψ (is the case)”, “if ϕ, then normally ψ”,
“if ϕ, then by default ψ”, and “if ϕ, then ψ is very likely”. then χ ◦ ϕ is also LPL –consistent (R3)
Numerous semantics have been proposed for default state- If χ ↔ χ and ϕ ↔ ϕ ,
0 0
ments, such as preferential structures [Kraus et al., 1990], - then χ ◦ ϕ ↔ χ0 ◦ ϕ0 (R4)
semantics [Adams, 1975], the possibilistic structures [Dubois
(χ ◦ ϕ) ∧ ϕ → χ ◦ (ϕ ∧ ϕ )
0 0
(R5)
and Prade, 1991] and κ-ranking [Spohn, 1988]. They all have
in common that they define the same set of validities axiom- If (χ ◦ ϕ) ∧ ϕ0 is LPL –consistent,
atized by the same proof system P (originally introduced by then χ ◦ (ϕ ∧ ϕ0 ) → (χ ◦ ϕ) ∧ ϕ0 (R6)
Kraus et al. [1990]). This remarkable fact is explained by
Friedman and Halpern [2001][2003]. 3.3 “Two Sides of the Same Coin”: Ramsey Test
Definition 8 (System P). The proof system P for LDEF is A well-known result, originally suggested by Ramsey [1929],
defined by the following axiom and inference rules, where all connects closely non-monotonic reasoning with belief revi-
formulas are propositional. sion. Informally, from ϕ I can non-monotonically infer ψ if,
and only if, I believe ψ after revising my belief base with
If
LPL
ϕ ↔ ϕ0 , then from ϕ ⊃ ψ infer ϕ0 ⊃ ψ (LLE) ϕ. This lead Makinson and Gärdenfors [1989][1991] to show
LPL formally that non-monotonic reasoning and belief revision
If ψ → ψ0 , then from ϕ ⊃ ψ infer ϕ ⊃ ψ 0
(RW) are “two sides of the same coin”.
ϕ⊃ϕ (REF) Theorem 4 (Halpern 2003).
From ϕ ⊃ ψ1 and ϕ ⊃ ψ2 infer ϕ ⊃ ψ1 ∧ ψ2 (AND) • Suppose that a revision operation ◦ satisfies (R1)–(R6).
From ϕ1 ⊃ ψ and ϕ2 ⊃ ψ infer ϕ1 ∨ ϕ2 ⊃ ψ (OR) Fix a belief base χ, and define a relation ⊃ on proposi-
From ϕ ⊃ ψ1 and ϕ ⊃ ψ2 infer ϕ ∧ ψ2 ⊃ ψ1 . (CM) tional formulas by taking ϕ ⊃ ψ to hold iff χ ◦ ϕ → ψ.
Then, ⊃ satisfies all the properties of P as well as Ratio-
nal Monotonicity:
if ϕ ⊃ ψ1 and not ϕ ⊃ ¬ψ2 , then ϕ ∧ ψ2 ⊃ ψ1 (Rat)
3.2 Belief Revision
Moreover, ϕ ⊃ ⊥ if, and only if, ϕ is not satisfiable.
In the so-called AGM belief revision theory of Alchourrón et
al. [1985], the beliefs of the agent are represented by a belief • Conversely, suppose that ⊃ is a relation on formulas that
set, denoted K. These propositional formulas represent the satisfies the properties of P and Rational Monotonicity
beliefs of the agent. The revision of K with ϕ, written K ∗ ϕ, (Rat), and ϕ ⊃ ⊥ if, and only if, ϕ is not satisfiable. Let
consists of adding ϕ to K, but in order that the resulting set be K = {ψ ∈ LPL | > ⊃ ψ}. Then, K is a belief set. Let χ
consistent, some formulas are removed from K. Because this be its corresponding belief base. Then, if ◦ is defined by
can be done in various ways, 8 AGM rationality postulates taking χ ◦ ϕ → ψ if, and only if, χ → (ϕ ⊃ ψ), then the
have been elicited as reasonable principles for revision. postulates (R1)–(R6) hold for χ and ◦.
X Y (X ; Y) U ϕ ϕ ψ1 ψ1 ϕ ϕ ψ2 ψ2
R1 W0L ⊃L ⊃L
(Z ; X) Y ((X, Z) ; Y) U ϕ ⊃ ψ1 ; ϕ ψ1 ϕ ⊃ ψ2 ; ϕ ψ2
W0L W0L
(ϕ ⊃ ψ1 , ϕ ⊃ ψ2 ) ; ϕ ψ1 (ϕ ⊃ ψ1 , ϕ ⊃ ψ2 ) ; ϕ ψ2
(W ; X) Y ∧R
RM (ϕ ⊃ ψ1 , ϕ ⊃ ψ2 ) ; ϕ ψ1 ∧ ψ2
(W ; (X, Z)) Y ((W ; X), Z) ⊃R
ϕ ⊃ ψ1 , ϕ ⊃ ψ2 ϕ ⊃ ψ1 ∧ ψ2
Figure 2: Structural Rules for LP+ and LNMR
ϕ1 ϕ1 ψ ψ ϕ2 ϕ2 ψ ψ
⊃L ⊃L
4 Sequent Calculi for Belief Revision and ϕ1 ⊃ ψ ; ϕ1 ψ ϕ2 ⊃ ψ ; ϕ2 ψ
W0L W0L
Conditional Logic (ϕ1 ⊃ ψ, ϕ2 ⊃ ψ) ; ϕ1 ψ (ϕ1 ⊃ ψ, ϕ2 ⊃ ψ) ; ϕ2 ψ
∨L
We show that the main systems of common sense reasoning
(ϕ1 ⊃ ψ, ϕ2 ⊃ ψ) ; ϕ ∨ ϕ1 ϕ
can be reformulated in the proof-theoretical setting of sub- ⊃R
structural logics. ϕ1 ⊃ ψ, ϕ2 ⊃ ψ ϕ1 ∨ ϕ2 ⊃ ϕ
4.1 Conditional Logic in Substructural Logic As for rule (RT2), because the rules of LP+ are invertible
LP+ LP+
Because we resort to the structural connective ; we need to (Proposition 5), we have that χ ; ϕ ψ iff χ ϕ ⊃ ψ,
introduce and add the logical connective ◦ to the system P: by rule ⊃R . We derive (RT2) by applying Expression 1. The
Definition 9 (Proof systems P+ and LP+ ). derivability of modus ponens follows from the cut rule.
Now, consider the right to left direction. Cut elimination
• The calculus P+ for L◦,⊃ is the calculus P to which we
holds for LP+ (Proposition 5) and LP+ satisfies the subformula
add the following (bidirectional) inference rule: LP+
property. Because what we prove is of the form χ ϕ⊃ψ
χ ◦ ϕ → ψ iff χ → ϕ ⊃ ψ (RT2)
with χ, ϕ, ψ ∈ LPL , this entails that the L⊃ –sequent will all be
• The sequent calculus LP+ for L⊃ is the sequent calculus of depth at most 1 (see Definition 2). So, in what follows, we
L⊃ where the structural rules are restricted to the L⊃ – only consider L⊃ –structures of depth at most 1.
sequents of depth 0, with rules R1 and W0L of Fig. 2. The rules of LPL are all derivable in P+ , because LPL ⊆ P+ .
Proposition 5. The cut rule can be eliminated from any proof We consider the rules ⊃R , ⊃L , R1 and W0L (we do not con-
of LP+ . Moreover, all the rules of LP+ are invertible. sider Cut because of Proposition 5). First, we prove that ⊃R
is derivable in P+ , the proof for ⊃L is similar. Assume that
LP+ LP+
Proof sketch. It can be adapted from [Restall, 2000, Th. 6.11] X;ψ ϕ; we must prove that X ψ ⊃ ϕ. That is, by
and [Troelstra and Schwichtenberg, 2000, Prop. 3.5.4]. Expression 1, we must prove that from t1 (X) ◦ ψ → ϕ, we can
Theorem 6. Let χ, ϕ, ψ ∈ LPL . Then, the following holds: infer t1 (X) → (ψ ⊃ ϕ) in P+ . This last inference follows from
LP+
L + + (RT2) of P+ . Second, we consider R1 . Assume that X Y;
χ P ϕ ⊃ ψ iff χ P ϕ ⊃ ψ LP+
we must prove that (Z ; X) Y. That is, by Expression 1
Proof. In this proof and the following, we will use the map-
and (RT2), we must prove that from t1 (X) → t2 (Y) (∗), we
pings t1 : SL L
Con
→ LCon and t2 : SL R
Con
→ LCon defined can infer t1 (Z) → (t1 (X) ⊃ t2 (Y)) (∗∗). By (RW) and (REF),
inductively as follows: we can prove t1 (X) ⊃ t2 (Y) from (∗), and therefore also (∗∗).
t1 (ϕ) := ϕ t2 (ϕ) := ϕ Third, we consider W0L . Assume that (X ; Y)
LP+
U, we must
t1 (X, Y) := t1 (X) ∧ t1 (Y) t2 (X, Y) := t2 (X) ∨ t2 (Y) LP+
t1 (X ; Y) := t1 (X) ◦ t1 (Y) prove that (X, Z) ; Y U. That is, by Expression 1 and
LP+
We can prove by induction on the number of steps used that (RT2), we must prove that from t1 (X) t1 (Y) ⊃ t2 (U) (∗)
LP+
X
LCon
Y iff t1 (X) t2 (Y) (1)
LCon we can prove t1 (X) ∧ t1 (Z) t1 (Y) ⊃ t2 (U). This is true in
LPL .
The proof of Theorem 6 is by induction on the number of
inference steps used in a proof. This boils down to show that 4.2 Belief Revision in Substructural Logic
each rule of inference and each axiom of LP+ is derivable in
P+ , and, vice versa, each rule and each axiom of P+ is deriv- Based on the rationality postulates (R1)–(R6), we can de-
able in LP+ . First, we prove that rules (LLE), (RW), (REF), fine a Hilbert-like proof system. It is not a genuine Hilbert
(CM), (AND) and (OR) are derivable in LP+ (in this order): 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
WL
resorting to hypersequents [Pottinger, 1983; Avron, 1996].1
ϕ, ψ2 ϕ
∧L
Definition 10 (Proof systems AGM and LAGM ).
ϕ0 ϕ ψ ψ ϕ ϕ ψ ψ0 ϕ ϕ ϕ ∧ ψ2 ϕ ψ1 ψ1
⊃L ⊃L R1 ⊃L 1
In all the hypersequent calculi that we define in the sequel
ϕ ⊃ ψ ; ϕ0 ψ ϕ⊃ψ ; ϕ ψ0 > ; ϕ ϕ ϕ ⊃ ψ1 ; ϕ ∧ ψ2 ψ1
⊃R ⊃R ⊃R ⊃R (based on already defined sequent calculi) we always take the in-
ϕ⊃ψ ϕ0 ⊃ ψ ϕ⊃ψ ϕ ⊃ ψ0 > ϕ⊃ϕ ϕ ⊃ ψ1 ϕ ∧ ψ2 ⊃ ψ1 ternal version of the structural rules. See [Avron, 1996] for details.
X Y (X ; Y) Z 4.3 The Ramsey Test in Substructural Logic
R1 Ra2 We are going to reformulate Theorem 4 in our sequent calculi,
(Z ; X) Y (X, Y) Z and obtain a new formalization of the Ramsey test. Note the
similarity between Expressions (RT1), (RT2) and (RT3).
(X ; Y) (X, Y) Z Definition 11 (Hypersequent calculus LNMR ). The hyperse-
R3 Rb2
Y (X ; Y) Z (X, Y) quent calculus LNMR for L⊃ is the sequent calculus LP+ to
which we add the structural rule (RM) of Fig. 2.
(X ; (Y , Z)) U
R5 Theorem 9 (Ramsey test). Let χ, ϕ, ψ ∈ LPL . Then, the fol-
((X ; Y), Z) U lowing holds:
LNMR LAGM
((X ; Y), Z) U χ ϕ ⊃ ψ iff χ ◦ ϕ ψ (RT3)
R6
(X ; (Y , Z)) U ((X ; Y), Z) Proof sketch. We define the Hilbert calculus NMR := LP+ +
(RM). Theorem 4 can be reformulated in our setting as fol-
lows: if χ, ϕ, ψ ∈ LPL , then χ ϕ ⊃ ψ iff χ ◦ ϕ ψ. So,
NMR AGM
Figure 3: Structural Rules for LAGM
if we prove that NMR and LNMR are provably equivalent, then
we will have proved the theorem, because we already know
• The Hilbert-like calculus AGM for L◦ is the Hilbert cal- by Theorem 6 that AGM and LAGM are provably equivalent.
culus of propositional logic to which we add the axioms To prove that, it suffices to show that the inference rule (RM)
and inference rules (R1)–(R6) of Lemma 3 (where LPL – is derivable in LNMR and, vice versa, that the inference rule
consistency is replaced by AGM–consistency). (Rat) is derivable in NMR. It is proved without difficulty.
• The hypersequent calculus LAGM for L◦ is the sequent
calculus L◦ to which we add the rules of Figure 3. 5 Gärdenfors’ Impossibility Result
Proposition 7. The cut rule can be eliminated from any proof As to the Ramsey test, a famous result [Gärdenfors, 1988]
of LAGM . Moreover, all the rules of LAGM are invertible. states a difficulty in introducing a connective ⊃ such that ϕ ⊃
Proof sketch. Similar to the proof of Proposition 5. ψ ∈ K iff ψ ∈ K ∗ ϕ. Indeed, an immediate consequence
means that if K ⊆ K 0 then K ∗ ϕ ⊆ K 0 ∗ ϕ, which is a
Theorem 8. Let χ, ϕ, ψ ∈ LPL . Then, the following holds: property essentially incompatible with the AGM postulates
χ◦ϕ ψ iff χ ◦ ϕ
LAGM
ψ
AGM for ∗. Accordingly, we retrieve Gärdenfors’ result as follows:
Proof sketch. The proof follows the same methodology as > > ⊥
Theorem 6. For the left to right direction, we prove (R1), ⊃L
(R4), (R2) (a and b) and (R5) (rule (R6) is proved similarly). >⊃⊥;>
R3
ψ ψ ϕ ϕ >
◦R
ϕ ϕ ψ1 ψ2 ϕ1 ϕ2 ψ ; ϕ ψ◦ϕ
Inconsistency of L◦,⊃ extended with R3 reflects, in a way
R1 ◦R Ra2 reminiscent of Gärdenfors’ proof, that conditionals capturing
ψ ; ϕ ϕ ψ1 ; ϕ1 ψ2 ◦ ϕ2 ψ, ϕ ψ◦ϕ defaults do not easily lend themselves to the role of premises.
◦L ◦L ∧L
ψ◦ϕ ϕ ψ1 ◦ ϕ1 ψ2 ◦ ϕ2 ψ∧ϕ ψ◦ϕ
→R →R →R 6 Conclusion
ψ◦ϕ→ϕ ψ1 ◦ ϕ1 → ψ2 ◦ ϕ2 ψ∧ϕ→ψ◦ϕ
Drawing intuitions from a dynamic interpretation of sub-
structural concepts in terms of updating, we have reformu-
ϕ ϕ ϕ0 ϕ0
∧R lated conditional logic and belief revision in the substructural
ψ ψ ϕ ϕ ψ ψ ϕ, ϕ0 ϕ ∧ ϕ0 framework as extensions of the Lambek calculus. We thus
∧R ◦R
retrieve some well-known results and provide new axiomati-
ψ, ϕ ψ∧ϕ ψ ; (ϕ, ϕ0 ) ψ ◦ (ϕ ∧ ϕ0 )
Rb2 R5 zations of belief revision and default reasoning.
ψ ; ϕ ψ∧ϕ ψ, ϕ (ψ ; ϕ), ϕ0 ψ ◦ (ϕ ∧ ϕ0 ) In particular, our results show that the key to non-
◦L ◦L
monotonicity is a constrained application of the left weak-
ψ◦ϕ ψ∧ϕ ψ, ϕ (ψ ◦ ϕ, ϕ0 ψ ◦ (ϕ ∧ ϕ0 )
∧L ∧L ening rule: our inferences stay the same if our knowledge of
ψ◦ϕ ψ∧ϕ ψ∧ϕ (ψ ◦ ϕ) ∧ ϕ0 ψ ◦ (ϕ ∧ ϕ0 ) the initial situation is made more precise, but we may cancel
→R →R
some of them if we are forced to update our knowledge in
ψ◦ϕ→ψ∧ϕ ψ∧ϕ (ψ ◦ ϕ) ∧ ϕ0 → ψ ◦ (ϕ ∧ ϕ0 )
face of new information (see rule W0L and definition of LP+ ).
LAGM
As for (R3), assume that ψ◦ϕ . Then, because the logical The range of belief revision and default reasoning clearly
LAGM calls for further work. For example, in our setting, given our
rules are invertible (Proposition 7), we have that ψ ; ϕ .
LAGM reading of ternary relations as updates and given our truth
So, by Rule R3 , we have that ϕ . conditions, the connective ⊂ represents some sort of abduc-
The right to left direction is proved similarly and relies also tion (see Definition 5). This notion of abduction can now
on the fact that (hyper)sequents are of depth 1 because of our be studied within our substructural framework in interaction
cut elimination result (Proposition 7). with the notions of revision, update and non-monotonicity.
References David Makinson and Peter Gärdenfors. Relations between
the logic of theory change and nonmonotonic logic. In
Ernest Adams. The Logic of Conditionals, volume 86 of Syn-
André Fuhrmann and Michael Morreau, editors, The Logic
these Library. Springer, 1975.
of Theory Change, volume 465 of Lecture Notes in Com-
Carlos E. Alchourrón, Peter Gärdenfors, and David Makin- puter Science, pages 185–205. Springer, 1989.
son. On the logic of theory change: Partial meet contrac- David Makinson. Bridges from classical to nonmonotonic
tion and revision functions. J. Symb. Log., 50(2):510–530, logic. King’s College, 2005.
1985.
Edwin D. Mares and Robert K. Meyer. The Blackwell guide
Guillaume Aucher. A combined system for update logic and to philosophical logic, chapter Relevant Logics. Wiley-
belief revision. In Mike Barley and Nikola K. Kasabov, ed- Blackwell, 2001.
itors, PRIMA, volume 3371 of Lecture Notes in Computer
Science, pages 1–17. Springer, 2004. Donald Nute and Charles B Cross. Conditional logic. In Dov
Gabbay and F. Guenthner, editors, Handbook of philosoph-
Guillaume Aucher. DEL as a substructural logic. In Alexan- ical logic, volume 4, pages 1–98. Kluwer Academic Pub,
dru Baltag and Sonja Smets, editors, Outstanding Contri- 2001.
butions: Johan F. A. K. van Benthem on Logical and Infor-
Nicola Olivetti. Tableaux and sequent calculus for minimal
mational Dynamics, Trends in Logic. Springer, 2014.
entailment. Journal of Automated Reasoning, 9(1):99–139,
Arnon Avron. The method of hypersequents in the proof the- 1992.
ory of propositional non-classical logics. In Logic: from Hiroakira Ono. Proof-theoretic methods in nonclassical
foundations to applications, pages 1–32. Clarendon Press, logic –an introduction. In Masako Takahashi, Mitsuhiro
1996. Okada, and Mariangiola Dezani-Ciancaglini, editors, The-
Alexandru Baltag and Sonja Smets. Texts in Logic and ories of Types and Proofs, volume Volume 2 of MSJ Mem-
Games, volume 3, chapter A Qualitative Theory of Dy- oirs, pages 207–254. The Mathematical Society of Japan,
namic Interactive Belief Revision, pages 9–58. Amsterdam Tokyo, Japan, 1998.
University Press, 2008. Garrel Pottinger. Uniform, cut-free formulations of T, S4 and
Jc Beall, Ross Brady, J. Michael Dunn, AP Hazen, Edwin S5. Journal of Symbolic Logic, 48(3):900, 1983.
Mares, Robert K Meyer, Graham Priest, Greg Restall, Frank P. Ramsey. General propositions and causality. In H.A.
David Ripley, John Slaney, et al. On the ternary rela- Mellor, editor, Philosophical Papers. Cambridge Univer-
tion and conditionality. Journal of philosophical logic, sity Press, Cambridge, 1929.
41(3):595–612, 2012.
Greg Restall. An Introduction to Substructural Logics. Rout-
Piero Andrea Bonatti and Nicola Olivetti. Sequent calculi for ledge, 2000.
propositional nonmonotonic logics. ACM Trans. Comput. Greg Restall. Relevant and substructural logics. Handbook
Logic, 3(2):226–278, April 2002. of the History of Logic, 7:289–398, 2006.
Didier Dubois and Henri Prade. Possibilistic logic, prefer- Richard Routley and Robert K Meyer. The semantics of
ential model and related issue. In Proceedings of the 12th entailment—ii. Journal of Philosophical Logic, 1(1):53–
International Conference on Artificial Intelligence (IJCAI), 73, 1972.
pages 419–425. Morgan Kaufman, 1991.
Richard Routley and Robert K Meyer. The semantics of
Nir Friedman and Joseph Y. Halpern. Plausibility measures entailment—iii. Journal of philosophical logic, 1(2):192–
and default reasoning. Journal of the ACM, 48(4):648–685, 208, 1972.
2001.
Richard Routley and Robert K Meyer. The semantics of en-
Peter Gärdenfors. Knowledge in Flux (Modeling the Dynam- tailment. Studies in Logic and the Foundations of Mathe-
ics of Epistemic States). Bradford/MIT Press, Cambridge, matics, 68:199–243, 1973.
Massachusetts, 1988. Richard Routley, Val Plumwood, and Robert K Meyer. Rel-
Peter Gärdenfors. Belief revision and nonmonotonic logic: evant logics and their rivals. Ridgeview Publishing Com-
Two sides of the same coin? In Logics in AI, pages 52–54. pany, 1982.
Springer, 1991. Wolfgang Spohn. Ordinal conditional functions: A dynamic
Joseph Halpern. Reasoning about Uncertainty. MIT Press, theory of epistemic states. In W. L. Harper and B. Skyrms,
Cambridge, Massachussetts, 2003. editors, Causation in Decision, Belief Change, and Statis-
tics, volume 2, pages 105–134. reidel, Dordrecht, 1988.
Hirofumi Katsuno and Alberto Mendelzon. Propositional
knowledge base revision and minimal change. Artificial Anne Sjerp Troelstra and Helmut Schwichtenberg. Basic
Intelligence, 52(3):263–294, 1992. proof theory. Number 43. Cambridge University Press,
2000.
Sarit Kraus, Daniel J. Lehmann, and Menachem Magidor.
Nonmonotonic reasoning, preferential models and cumula- Johan van Benthem. Logical Dynamics of Information and
tive logics. Artificial Intelligence, 44(1-2):167–207, 1990. Interaction. Cambridge University Press, 2011.