This paper studies the implication relations between the AGM postulates ( 7) and (+_ 7) under non-classical logics, namely intuitionistic logic, paraconsistent logic, G3 and G3'. In order to do so, some theorems on the implication relations between such postulates are drawn for logics with a special set of axioms. These are later used to deduce similar results under the four logics of interest. Then we discuss a possible solution for our lack of sucient conditions for the implication relations to hold under some of the studied logics.
Introduction
On one hand, the well known AGM theory of belief revision breaks the problem
of dening belief revision operations into two parts: a set of rationality postulates
and constructions (i.e. a framework for dening eective methods) for operators
that aim to fulll such postulates. This theory also assumes some underlying
logic that includes classical propositional logic and that is compact1.[
On the other hand, besides classical logic, there exist the so called nonclassical logics. The motivations for creating and studying them are varied. Examples of such logics are intuitionistic logic , paraconsistent logic , G3 and G3’.
Here we present the rst results of a research aimed to help nding a way of using the AGM theory of belief revision (if possible) under the non-classical logics mentioned. The research is focused only on studying the implication relations between the rationality postulates, with the primary objective of nding sucient conditions for these implications to hold under those logics. The two results are (i) what are sucient conditions for the AGM postulate for contraction ( 7) to hold if the AGM postulate for revision ( +_ 7) holds, and (ii) what are sucient conditions for the AGM postulate for revision ( +_ 7) to hold if the AGM postulate for contraction ( 7) holds.
Since the rationality postulates are the foundation of any construction for a
contraction or revision operation [
The structure of the paper is as follows. Section 2 recalls some logic notions and basic notations. Section 3 briey describes the motivation behind nonclassical logics and introduces the logics studied. Section 4 summarizes the AGM theory and broadens the motivation for this research. Our contribution is given in section 5.
We build on the AGM theory of belief revision [
Background This section is intended to remark our denition of logic and some relevant properties on the notions of logical consequence relation and logical consequence operator implied by such denition. The properties will be particularly important in section 5. 2.1
Formal Propositional Language
In order to talk about a logic, one must rst have a way of coding propositions.
Thus we dene a formal propositional language together with its alphabet :
Denition 1. [
Denition 2. [7] The formal propositional language P is the set whose elements, called formulas, are strings over built recursively using the following rules:
2. If x; y ∈ P, then (x ∧ y) ; (x ∨ y) ; (x → y) ∈ P. 3. If x ∈ P, then ¬x ∈ P.
We will denote atoms with the Greek letters , and . Similarly, we will denote formulas with the letters a, x and y. The notation x ↔ y will be used to abbreviate (x → y) ∧ (y → x).
Auxiliary parenthesis will sometimes be omitted in the writing of formulas. In those cases the usual precedence for connectives applies: ¬, ∧, ∨, → and ↔ should be processed in that same order.
When dealing with formulas, it will be useful to have a name for any set of formulas, thus:
We will use each of the symbols R, S and T to represent any theory. Similarly, T ′ will stand for any nite theory. 2.2
Logic One important denition to keep in mind is that of logic. In this paper a logic is considered simply as a formal theory : Denition 4.
[7] A formal theory or logic F is built from: 1. A countable set SsF of symbols called the symbols of F . Each nite sequence of symbols will be called an expression of F . 2. A subset Swf fF of the expressions of F called the set of well-formed formulas of F . 3. A subset F of Swf fF called the set of axioms of F . 4. A nite set {X1; X2; : : : ; Xn} of n-relations over Swf fF 2, called rules of inference. For each w ∈ Cf bfF , if there are f1; : : : ; fm ∈ Cf bfF and j ∈ {1; : : : ; n} such that ⟨f1; : : : ; fm; w⟩ ∈ Xj , then w is a direct consequence of f1; : : : ; fm by virtue of Xj .
Moreover, from now on the following assumptions are made for all logics:
1. SsF =
2. Swf fF = P
3. The set F is closed under substitution : if a formula x is in
other formula obtained by replacing all occurrences of an atom
another formula y is in F too [
in x with
M:P: d=ef {⟨x; y; z⟩ ∈ P × P × P S y = x → z} :
There are several other ideas related to the concept of logic. Amongst them, proof and logical consequence are of our immediate interest. The former is the base for the later, while the later, together with our denition of logic, imply certain relevant properties presented in the next subsection.
Denition 5. [7] A proof or deduction in a formal theory F for w ∈ Swf fF from ⊆ Cf bfF is a nite sequence f1; : : : ; fn, where f1; : : : ; fn ∈ Cf bfF , that satises the following two conditions: 1. fn = w 2. For each j ∈ {1; : : : ; n} one of the following conditions is satised: fj ∈ or fj ∈ F or fj is a direct consequence of some of the previous well-formed formulas in the sequence by virtue of some rule of inference of F . Denition 6. [6] A w ∈ Cf bfF is a logical consequence in the formal theory F from a ⊆ Swf fF if there is a proof in F for w from . 2 I.e. subsets of the Cartesian product of Swf fF with itself n times. 2.3
Consequence relations and operations Another important concept that should be borne in mind is that of a consequence relation : Denition 7. that
[5] A (logical) consequence relation ⊢F is a binary relation such def ⊢F = {⟨T; x⟩ ∈ ℘ (P) × P S x is a logical consequence in F from T } where F is a logic, ℘ (P) stands for the power set of P and ℘ (P) × P denotes the Cartesian product of ℘ (P) and P.
Subscripts (as in ⊢F ) may be omitted from now on whenever there is no confusion about the underlying logic.
The notation T ⊢ x will be used to denote ⟨T; x⟩ ∈⊢. Similarly, T ⊬ x will be used to denote ⟨T; x⟩ ∉⊢. In the case that T = ∅, we will write ⊢ x to denote that ∅ ⊢ x, and we will use ⊬ x to denote that ∅ ⊬ x.
There are two kinds of consequence relations that are relevant to this work, namely: Denition 8. [5] A consequence relation is an abstract consequence relation if it has the following properties:
If x ∈ T , then T ⊢ x .
If S ⊢ x and S ⊆ T , then T ⊢ x .
If T ⊢ x and for every y ∈ T , S ⊢ y, then S ⊢ x .
Denition 9. [5] A consequence relation is a nitary consequence relation in addition to being abstract it satises: if
Remark 10. The condition introduced in denition 9 is usually called ness. compactProposition 11. [6] All consequence relations assumed in this paper are nitary consequence relations .
Proof. The proof is straightforward given the denition of consequence relation and the denition of logic.
The last two denitions are used in proofs in section 5, and so is a certain kind of consequence operator. This is the motivation for the following two denitions:
℘ (P) such that [5] A (logical) consequence operator is a function Cn⊢ ∶ ℘ (P) →
Cn⊢ (T ) d=ef {x S T ⊢ x} :
The reader should note that whenever a consequence operator Cn⊢ is dened from a consequence relation ⊢F dependent upon a logic F , we will write CnF instead of Cn⊢F .
Remark 13. [5] By denition 12 and set theory, clearly
x ∈ Cn⊢ (T ) if and only if T ⊢ x therefore both notations will be used interchangeably.
Denition 14. [5] A consequence operator is an abstract consequence operator if it has the following properties:
T ⊆ Cn (T ) .
Cn (Cn (T )) = Cn (T ) .
If S ⊆ T , then Cn (S) ⊆ Cn (T ) .
Proposition 15. A consequence operator is abstract if and only if the consequence relation used to dene it is abstract.
Proof. Using set theory, it is a simple exercise to show this.
To end this section, we introduce one last denition that will prove useful later:
The symbol A will be used to denote any cn-theory: i.e. A = Cn (T ), for some T , possibly A itself. 3
Studied Logics
Classical logic was created as a model for studying the truth of propositions
[
In this section we present some logics of interest to this work and a way to
compare them. Denitions of the logics are borrowed from [
Denition 17. Pos (short for positive logic) is the logic whose set of axioms P os has the following elements: → ( . . .
. . . .
Denition 18. Cw is the logic whose set of axioms of P os plus the following two axioms:
Denition 19. Pac (short for paraconsistent logic ) is the logic whose set of axioms P ac has all the elements of Cw plus the following axioms: (( → ) → ) →
.
¬ ( → ) ↔ ( ∧ ¬ ) .
Denition 20. Int (short for intuitionistic logic) is the logic whose set of axioms Int has all the elements of P os plus the following axioms: ¬
→ ( → ) . ( → ) → (( → ¬ ) → ¬ ) .
set of axioms
G3 (also known as the logic of here and there ) is the logic whose G3 has all the elements of Int plus the following axiom: (¬ → ) → ((( → ) → ) → ) .
G3’ is one last logic that we are interested in. A rigorous denition for G3’
is omitted here, but it suces to know than its set of axioms G3′ has all the
elements of Cw plus another four. Such additional axioms can be found in [
Only the last four logics mentioned are of importance in the following
sections. The others just provide insight for comparing those logics, as it will be
made clear shortly. The reader may refer to [
F ⊆
In our case, the following lemma is useful: Lemma 24. Let F and F ′ be each any logic. If than or equal to F .
Proof. This follows from the denition of proof (i.e. denition 5). A detailed proof is omitted.
Example 25. Int is stronger than or equal to Pos, while G3 is stronger than or equal to Int. 4
Taking AGM into Non-classical Logics By AGM theory of belief revision we mean the theory developed by Alchourron, Grdenfors and Makinson in works like [4,9]. It is well known that their work has been dominant in the eld of belief revision [10].
The AGM theory assumes a formal propositional language 3 as the means for
coding propositions and some underlying logic that includes classical
propositional logic and that is compact. Moreover, the AGM theory encompasses three
dierent belief change operations over cn-theories: expansion, where a formula
is introduced into a cn-theory together with all the formulas deducible from the
new cn-theory; contraction, that ensures a formula cannot be deduced from a
resulting cn-theory; and revision, which retracts everything in contradiction with
a new formula and subsequently expands the contraction with the new formula.
Dening the rst of them is trivial, while the other two have to undergo a more
elaborated process. [
The main focus of this theory of belief revision is dening revision and
contraction. This process is split in two main parts: the AGM rationality postulates
(named after the three authors) and constructions (i.e. a framework for dening
eective methods) for operations that comply with those postulates. The former
is concerned with stating what an appropriate revision or contraction operation
is (i.e. the what ); the later is intended to be the scheme of actual
implementations of such operations (i.e. the how ). Both parts are then equivalent by means
of what are called representation theorems . [
We dare to say that the postulates part is the more important of the two. If we are to contribute to nding a way of using this theory under non-classical logics, the postulates can be used to nd out if its rationale holds under such 3 For which some details are left open. We assume this language to be P. logics in the rst place. This is the reason why we have focused this research on the rationality postulates only. It must be noted, however, that even if we were successful, nding a way for the equivalence of the two main parts of this theory of belief revision to hold is yet another issue (which we conjecture would require less eort) in the way to reaching the overall goal.
Moreover, the postulates are further divided in postulates for contraction and
postulates for revision, and for each case there is a basic set of postulates and a
supplementary set [
A x is a cn-theory whenever A is a cn-theory.
A
x ⊆ A .
If x ∉ Cn (A) , then A
x = A .
If x ∉ Cn (∅) , then x ∉ Cn (A
x) .
If Cn ({x}) = Cn ({y}) , then A x = A y .
( 1) ( 2) ( 3) ( 4) ( 5)
A ⊆ Cn ((A x) ∪ {x}) whenever A is a cn-theory. ( 6) Since only two more postulates will be needed by the forthcoming results, the supplementary set for contraction and the complete set for revision are omitted here. Nevertheless, the reader can nd both sets of postulates in [4].
The theory of belief revision also considers ways of bridging, so to speak, the postulates for contraction and the postulates of revision. This is done by means of two identities: the Levi identity and the Harper identity [4]. The former is of interest to this paper:
A+_ x = Cn ((A ¬x) ∪ {x}) .
In [
The research we have carried so far has studied the implication relations
between two AGM (supplementary) postulates and, therefore their possible
equivalence. We have focused primarily on nding sucient conditions for such
relations to hold. These two postulates are:
(Levi)
A+_ (x ∧ y) ⊆ Cn ((A+_ x) ∪ {y}) for any cn-theory A.
(+_ 7)
(A x) ∩ (A y) ⊆ A (x ∧ y) for any cn-theory A. ( 7)
Their intention (aided by the rest of the supplementary postulates) is to
specify the behavior of their corresponding operations when dealing with formulas
in conjunctive form [
Before ending this section, we must not forget to mention a useful lemma: Lemma 26. Let the notation A x stand for the set of formulas that is assigned to A and x by a contraction operation that satises the AGM postulate ( 6) and is dened for a logic with an abstract consequence relation. Then it holds that: If {y} ⊢ x, then A ⊆ Cn ((A x) ∪ {y}).
Proof. The proof is straightforward and thus is omitted. 5
On the Implication Relations between ( 7) and ( _ 7) + We studied several conditions for the implication relations between ( +_ 7) and ( 7) to hold. Amongst the conditions for each case there is a logic, which implies certain properties.
In this section we present those two logics, describe briey their relevant properties and enunciate the most important results on the implication relations. 5.1
elements:
Let LT1 be the logic whose set of axioms
LT 1 has the following
⊢ x ↔ ¬ ((¬x ∨ ¬y) ∧ ¬x) . ⊢ y ↔ ¬ ((¬x ∨ ¬y) ∧ ¬y) .
⊢ ¬ (¬x ∨ ¬y) ↔ (x ∧ y) .
Proof. Detailed proofs are omitted.
(12): Any logic that satises axioms (1) and (2) also satises (12) [
(14): Holds given the denition of abstract consequence relation, axiom (3), (12) and set theory.
(15): Holds given (14) and set theory.
(16), (17) and (18): It is a simple exercise to prove each under LT1.
Remark 29. (12) is usually called deduction theorem (as in [
Proof. Let us assume (+_ 7). We need to show that ( 7) holds. Let By the previous and set theory, to prove ( 7) it suces to show Also by (19) and set theory, both of the following hold a ∈ ((A x) ∩ (A
y)) . a ∈ A ¬ ((¬x ∨ ¬y) ∧ ¬x) . (23) (24) (25) (26) (27) (28) (29) (30) (31) (32) Using only set theory, denition of abstract consequence operation, (Levi) and (+_ 7),
A ¬ ((¬x ∨ ¬y) ∧ ¬x) ⊆ Cn ((A+_ (¬x ∨ ¬y)) ∪ {¬x}) .
Then, by (23), (24) and set theory, it can be deduced that
a ∈ Cn ((A+_ (¬x ∨ ¬y)) ∪ {¬x}) .
Based on (22), (17) and a similar reasoning as the one developed from (23) to (25),
a ∈ Cn ((A+_ (¬x ∨ ¬y)) ∪ {¬y}) .
By set theory, denition of abstract consequence operation and (Levi), (¬x ∨ ¬y) ∈ A+_ (¬x ∨ ¬y) .
a ∈ Cn (A+_ (¬x ∨ ¬y)) .
Recalling that x ∈ Cn (T ) i T ⊢ x and based on (25), (26) and (27), (15) can be used to obtain Given (28), by denition of abstract consequence operation, (Levi), (9), (18), (13) and ( 5), it can be turned into By (21), ( 2), ( 6) and set theory,
(x ∧ y)) ∪ {¬ (x ∧ y)}) .
(x ∧ y)) ∪ {(x ∧ y)}) .
We know that, by (11), ⊢ (x ∧ y) ∨ ¬ (x ∧ y), so by ( 1) it holds that ((x ∧ y) ∨ ¬ (x ∧ y)) ∈ A
Again, by x ∈ Cn (T ) i T ⊢ x, (29), (30) and (31), (15) can be used to get a ∈ Cn (A (x ∧ y)) .
Which by Cn (Cn (T )) = Cn (T ) and ( 1) shows (20). ◻
Given the previous result, the denition of Pac and lemma 24, we have as a direct consequence the following corollary: Corollary 31. Let the notation A x stand for the set of formulas that is assigned to A and x by a contraction operation that satises AGM postulates ( 1), ( 2), ( 5) and ( 6), the Levi identity and is dened over the logic Pac. Such contraction operation satises ( 7) if it satises ( +_ 7).
Remark 32. A similar result could not be veried for the other logics mentioned
earlier due to the steps taken in the proof of theorem 30. Specically (16), (17)
and (18) do not hold for Int, G3 or G3’ 4: only the → side of (16), (17), and the
← side of (18) hold for Int and G3; also, so to speak symmetrically, only the ←
side of (16), (17), and the → side of (18) hold for G3’. Moreover, it is well known
that (11) is not a theorem of Int or G3 (see [
When studying the implication relation from ( 7) to (+_ 7), we found out that the assumption of Int as the underlying logic provides sucient properties for this implication to hold.
Remark 33. The same as in LT1, the deduction theorem, the theorem of introduction of disjunctions in the premises and propositions (13) and (15) hold in Int.
Proposition 34. In addition to the properties mentioned by the previous remark, the following hold in Int:
⊢ ¬x ↔ ¬ (x ∧ y) ∧ (¬x ∨ y) .
Cn (R ∪ T ) ∩ Cn (S ∪ T ) ⊆ Cn ((Cn (R) ∩ Cn (S)) ∪ T ) .
Cn (A ∪ {x ∧ y}) ⊆ Cn ((A (¬x ∨ y)) ∪ {x ∧ y}) .
Proof. Detailed proofs are omitted.
(33): It is a simple exercise to prove under Int.
(34): Holds given the denition of nitary consequence relation, the theorem of introduction of disjunctions in the premises and the axioms of Int dealing with conjunctions and disjunctions.
(35): Clearly {x ∧ y} ⊢ ¬x ∨ y holds under Int, so by denition of abstract consequence relation, lemma 26 and set theory, (35) is easy to prove. Theorem 35. Let the notation A x stand for the set of formulas that is assigned to A and x by a contraction operation that satises AGM postulates ( 1), ( 2), ( 5) and ( 6), the Levi identity and is dened over the logic Int. Such contraction operation satises ( +_ 7) if it satises ( 7).
Proof. Let us assume ( 7). We need to show that ( +_ 7) holds. Let
a ∈ A+_ (x ∧ y) .
4 This is assured by the use of truth tables (see [
(¬ (x ∧ y) ∧ (¬x ∨ y))) ∪ {x ∧ y}) .
Taking into account ( 7), set theory and the denition of abstract consequence operation, it can be shown that
Cn (((A ¬ (x ∧ y)) ∩ (A
(¬x ∨ y))) ∪ {x ∧ y}) ⊆ Cn ((A (¬ (x ∧ y) ∧ (¬x ∨ y))) ∪ {x ∧ y}) .
a ∈ Cn ((A+_ x) ∪ {y}) .
¬x) ∪ {x ∧ y}) .
a ∈ Cn ((A (¬x ∨ y)) ∪ {x ∧ y}) . (43) It is easy to realize that (42) follows from (Levi) and (36). Then, by ( 2), set theory and denition of abstract consequence operation, By the previous and set theory, to prove ( +_ 7) it suces to show Based on (Levi), the denition of abstract consequence relation and the axioms of Int dealing with conjunctions, the previous proposition is equivalent to (37) (38) (39) (40) (41) (42) (44) (45) With the denition of abstract consequence operation, set theory, ( the previous step, it can be shown that 1), (34) and Cn ((A ¬ (x ∧ y)) ∪ {x ∧ y}) ∩ Cn ((A
(¬x ∨ y)) ∪ {x ∧ y}) ⊆ Cn ((A
(¬ (x ∧ y) ∧ (¬x ∨ y))) ∪ {x ∧ y}) .
By (41) and set theory, to prove (39) it suces to show both of the following:
¬ (x ∧ y)) ∪ {x ∧ y}) .
Cn ((A
¬ (x ∧ y)) ∪ {x ∧ y}) ⊆ Cn (A ∪ {x ∧ y}) .
A direct consequence of (42), set theory and the previous is
a ∈ Cn (A ∪ {x ∧ y}) .
Finally, by the previous proposition, (35) and set theory it is easy to see that (43) holds. ◻
Given the previous result, the denition of G3 and lemma 26, we have: Corollary 36. Let the notation A x stand for the set of formulas that is assigned to A and x by a contraction operation that satises AGM postulates ( 1), ( 2), ( 5) and ( 6), the Levi identity and is dened over the logic G3. Such contraction operation satises ( +_ 7) if it satises ( 7).
Remark 37. A similar result could not be veried for the other logics mentioned earlier due to the steps taken in the proof of theorem 35. Specically, only the ← side of (33) does not hold for Pac or G3’.
Avoiding the Problems Found Going from ( 7) to (+_ 7) Given the primary objective of this research (i.e. nding sucient conditions for the implication relations to hold), the author is focused on discovering further useful assumptions. In this subsection we discuss an option that seems promising and is left for future work.
When analyzing the proofs of theorems 30 and 35, one can eventually pose the question of how would the proofs be aected by assuming some containment relation between contractions of the same cn-theory with respect to formulas related in some way. Amongst various candidates for solving this question, the following two examples are particularly interesting at rst glance: If {x} ⊢ y, then A If {x} ⊢ y, then A y ⊆ A y ⊇ A x : x : ( 5′) ( 5′′)
With ( 5′) and using a slightly dierent logic than Pos, it would be possible to deduce similar results as corollary 36 for Pac and G3’. Unfortunately ( 5′) turns out to be in contradiction with the postulates for contraction: one fundamental assumption of it is that x ∉ A y whenever {x} ⊢ y and ⊬ x, but at the same time it can be shown, using ( 1), ( 2) and ( 6), that if ⊢ y, then A y = A.
In the case of ( 5′′), we conjecture that it will not have similar problems as ( 5′). With the help of ( 5′′) it would be possible to bypass some of the problems encountered in nding similar results as corollary 31 for Int, G3 and G3’. 6
Conclusions and Future Work We have introduced some non-classical logics and summarized the AGM theory of belief revision. We have shown several implication relations between the AGM postulates (+_ 7) and ( 7). Finally, we have given an example of an open issue regarding the quest for additional conditions for the implication relations to hold.
Future work will focus on currently open issues and on studying the possible equivalence of other AGM postulates, such as ( +_ 8) and ( 8), under the logics already studied. 4. C. E. Alchourron, P. Grdenfors, and D. Makinson, On the logic of theory change: Partial meet contraction and revision functions, The Journal of Symbolic Logic, vol. 50, no. 2, pp. 510530, June 1985. [Online]. Available: db/journals/jsyml/jsyml50.html#AlchourronGM85 5. R. Jansana, Propositional consequence relations and algebraic logic, in The Stanford Encyclopedia of Philosophy , E. N. Zalta, Ed., Winter 2006. [Online]. Available: http://plato.stanford.edu/archives/win2006/entries/consequence-algebraic/ 6. E. Mendelson, Introduction to mathematical logic; (3rd ed.) . Monterey, CA, USA:
Wadsworth and Brooks/Cole Advanced Books & Software, 1987. 7. J. Arrazola, M. Osorio, and I. Martnez, `lgebras de Heyting y lgica constructiva .
Puebla: BenemØrita Universidad Autnoma de Puebla, 2007, ch. 5, pp. 105166. 8. W. Carnielli and J. Marcos, A taxonomy of c-systems, in Paraconsistency: The Logical Way to the Inconsistent, Proceeding of the II World Congress on Paraconsistency. 9. C. E. Alchourron and M. David, On the logic of theory change: Safe contraction,
Studia Logica, vol. 44, pp. 405422, 1985. 10. S. O. Hansson, Logic of belief revision, in The Stanford Encyclopedia of Philosophy, E. N. Zalta, Ed., Winter 2008. [Online]. Available: http: //plato.stanford.edu/archives/win2008/entries/logic-belief-revision/