by Corry Shores
[Search Blog Here. Index-tags are found on the bottom of the left column.]
[Logic and Semantics, entry directory]
[Graham Priest, entry directory]
[Priest, Introduction to Non-Classical Logic, entry directory]
[The following is summary of Priest’s text, which is already written with maximum efficiency. Bracketed commentary and boldface are my own, unless otherwise noted. I do not have specialized training in this field, so please trust the original text over my summarization. I apologize for my typos and other unfortunate mistakes, because I have not finished proofreading, and I also have not finished learning all the basics of these logics.]
Summary of
Graham Priest
An Introduction to Non-Classical Logic: From If to Is
Part II:
Quantification and Identity
12.
Classical First-order Logic
12.4
Tableaux
Brief summary:
(12.4.1) The tableau rules for classical first-order logic add four quantifier rules to those from propositional logic.
| Double Negation Development (¬¬D) |
| ¬¬A ↓ A |
| Conjunction Development (∧D) |
| A ∧ B ↓ A ↓ B |
| Negated Conjunction Development (¬∧D) |
| ¬(A ∧ B) ↙ ↘ ¬A ¬B |
| Disjunction Development (∨D) |
| A ∨ B ↙ ↘ A B |
| Negated Disjunction Development (¬∨D) |
| ¬(A ∨ B) ↓ ¬A ↓ ¬B |
| Conditional Development (⊃D) |
| A ⊃ B ↙ ↘ ¬A B |
| Negated Conditional Development (¬⊃D) |
| ¬(A ⊃ B) ↓ A ↓ ¬B |
| Biconditional Development (≡D) |
| A ≡ B ↙ ↘ A ¬A B ¬B |
| Negated Biconditional Development (≡D) |
| A ≡ B ↙ ↘ A ¬A ¬B B |
| Negated Existential Development (¬∃D) |
| ¬∃xA ↓ ∀x¬A |
| Negated Universal Development (¬∀D) |
| ¬∀xA ↓ ∃x¬A |
| Universal Instantiation Development (UI,D) |
| ∀xA ↓ Ax(a)
where a is any constant on the branch. (If there are not any, we select one at will.) |
| Particular Instantiation Development (PI,D) |
| ∃xA ↓ Ax(c)
where c is any constant that does not occur so far on the branch. |
(6-8; 266, with names and additional text at the bottom made by me)
Note: we should never check-off lines of the form ∀xA, because it is always possible that we will later introduce a new constant and then need to repeat universal instantiation on it. Yet, it can be useful to write beside the line all the constants it has been instantiated with. (12.4.2) We cannot apply a rule to an internal part of a line but only to the whole line itself. So we should not have:
¬(A ∧ ∀xB)
↓
¬(A ∧ Bx(a))
(12.4.3) Priest will “write Σ ⊢ A to mean that there is a closed tableau whose initial list comprises the members of Σ together with the negation of A” (266-267). (12.4.4) It does not matter what order we apply the tableau rules. (12.4.5) Priest then gives a first example tableau for a valid inference. (12.4.6) Priest next gives a second example tableau for a valid inference. (12.4.7) Priest then gives a third example tableau, this time for an invalid inference. (12.4.8) We construct counter-models from open branches in the following way: “take a domain which contains a distinct object, ∂b, for every constant, b, on the branch. v(b) is ∂b. v(P) is the set of n-tuples ⟨∂b1, . . . , ∂bn⟩ such that Pb1 . . . bn occurs on the branch. Of course, if ¬Pb1 . . . bn is on the branch, ⟨∂b1, . . . , ∂bn⟩ ∉ v(P), since the branch is open. (If a predicate or constant does not occur on the branch, the value given to it by v is a don’t care condition: it can be anything one likes)” (268). (12.4.9) We can check which formulas are true by seeing if the model makes them so. (12.4.10) Tableaux can be infinite. One way this happens is if there is an endless generation of new constants on account of repeating applications of instantiation. (12.4.11) When tableaux are infinite, we can use guesswork to formulate counter-models. (12.4.12) Priest next provides an algorithm for ensuring that infinite tableaux are complete: “(1) For each branch in turn (there is only a finite number at any stage of the construction), we run down the formulas on the branch, applying any rule that generates something not already on the branch. (In the case of a rule such as UI, which has multiple applications, we make all the applications possible at this stage.) (2) We then go back and repeat the process” (270). (12.4.13) “The tableaux are sound and complete with respect to the semantics” (270). (12.4.14) In order to show the behavior of quantifiers, Priest lists the ways that the quantifiers interact with the propositional operators.
In classical logic, the interactions are as follows. ‘A ⊣⊢ B’ means ‘A ⊢ B and B ⊢ A’. C is any closed formula. A * at the end of a line indicates that the converse does not hold, in the sense that there are instances that are not valid. (So, for example, in the first line for Negation, if A is Px, we have ¬∀xPx ⊬ ∀x¬Px.) Where the converse does not hold, there is often a restricted version involving a closed formula that does. Where this exists, it is given on the next line. [...]
1. No Operators
(a) ∀xC ⊣⊢ C
(b) ∃xC ⊣⊢ C
2. Negation
(a) ∀x¬A ⊢ ¬∀xA *
(b) ¬∀xC ⊢ ∀x¬C
(c) ¬∃xA ⊢ ∃x¬A *
(d) ∃x¬C ⊢ ¬∃xC
(e) ¬∃xA ⊣⊢ ∀x¬A
(f) ¬∀xA ⊣⊢ ∃x¬A
3. Disjunction
(a) ∀xA ∨ ∀xB ⊢ ∀x(A ∨ B) *
(b) ∀x(A ∨ C) ⊢ ∀xA ∨ C
(c) ∃xA ∨ ∃xB ⊣⊢ ∃x(A ∨ B)
(d) ∀xA ∨ ∀xB ⊢ ∃x(A ∨ B) *
(e) ∀x(A ∨ B) ⊢ ∃xA ∨ ∃xB *
4. Conjunction
(a) ∀xA ∧ ∀xB ⊣⊢ ∀x(A ∧ B)
(b) ∃x(A ∧ B) ⊢ ∃xA ∧ ∃xB *
(c) ∃xA ∧ C ⊢ ∃x(A ∧ C)
(d) ∀xA ∧ ∀xB ⊢ ∃x(A ∧ B) *
(e) ∀x(A ∧ B) ⊢ ∃xA ∧ ∃xB *
5. Conditional
(a) ∀x(A ⊃ B) ⊢ ∀xA ⊃ ∀xB *
(b) C ⊃ ∀xB ⊢ ∀x(C ⊃ B)
(c) ∃xA ⊃ ∃xB ⊢ ∃x(A ⊃ B) *
(d) ∃x(C ⊃ B) ⊢ C ⊃ ∃xB
(e) ∀x(A ⊃ B) ⊢ ∃xA ⊃ ∃xB *
(f) ∃xA ⊃ C ⊢ ∀x(A ⊃ C)
(g) ∀xA ⊃ ∀xB ⊢ ∃x(A ⊃ B) *
(h) ∃x(A ⊃ C) ⊢ ∀xA ⊃ C
(270-272)
[The Tableau Rules for Classical First-Order Logic]
[A Rule Against Partial Application of Tableau Rules]
[Closed Tableaux Notation]
[The Non-Restriction on Rule Order]
[Tableau Example 1]
[Tableau Example 2]
[Tableau Example 3]
[Counter-Models]
[Checking the Truth Values of Formulas]
[Infinite Tableaux]
[Constructing Counter-Models for Infinite Tableaux]
[Ensuring the Completeness of Infinite Tableaux]
[The Soundness and Completeness of the Tableaux]
Summary
[The Tableau Rules for Classical First-Order Logic]
[The tableau rules for classical first-order logic add four quantifier rules to those from propositional logic. Note: we should never check-off lines of the form ∀xA, because it is always possible that we will later introduce a new constant and then need to repeat universal instantiation on it. Yet, it can be useful to write beside the line all the constants it has been instantiated with.]
Priest now gives the tableau procedures for classical first-order logic. We add four rules for the quantifiers to the set already provided in section 1.4. [Below I give them altogether.]
| Double Negation Development (¬¬D) |
| ¬¬A ↓ A |
| Conjunction Development (∧D) |
| A ∧ B ↓ A ↓ B |
| Negated Conjunction Development (¬∧D) |
| ¬(A ∧ B) ↙ ↘ ¬A ¬B |
| Disjunction Development (∨D) |
| A ∨ B ↙ ↘ A B |
| Negated Disjunction Development (¬∨D) |
| ¬(A ∨ B) ↓ ¬A ↓ ¬B |
| Conditional Development (⊃D) |
| A ⊃ B ↙ ↘ ¬A B |
| Negated Conditional Development (¬⊃D) |
| ¬(A ⊃ B) ↓ A ↓ ¬B |
| Biconditional Development (≡D) |
| A ≡ B ↙ ↘ A ¬A B ¬B |
| Negated Biconditional Development (≡D) |
| A ≡ B ↙ ↘ A ¬A ¬B B |
| Negated Existential Development (¬∃D) |
| ¬∃xA ↓ ∀x¬A |
| Negated Universal Development (¬∀D) |
| ¬∀xA ↓ ∃x¬A |
| Universal Instantiation Development (UI,D) |
| ∀xA ↓ Ax(a)
where a is any constant on the branch. (If there are not any, we select one at will.) |
| Particular Instantiation Development (PI,D) |
| ∃xA ↓ Ax(c)
where c is any constant that does not occur so far on the branch. |
(6-8; 266, with names and additional text at the bottom made by me)
Priest notes that when checking lines to indicate which ones are depleted, we can never check-off lines of the form ∀xA, because it is always possible that we will later introduce a new constant and then need to repeat universal instantiation on it. Yet, Priest offers this tip: “A useful trick is, instead of checking the line, to write beside it all the constants with which it has been instantiated.”]
Tableaux for first-order logic are the same as those for propositional logic (1.4), except that we have four new rules:
Negated Existential
Development (¬∃D)
¬∃xA
↓
∀x¬A
Negated Universal
Development (¬∀D)
¬∀xA
↓
∃x¬A
Universal Instantiation
Development (UI,D)
∀xA
↓
Ax(a)
where a is any constant on the branch. (If there are not any, we select one at will.)
Particular Instantiation
Development (PI,D)
∃xA
↓
Ax(c)
where c is any constant that does not occur so far on the branch.
(266, with names and additional text at the bottom made by me)
The third and fourth rules are called universal and particular instantiation (UI and PI), respectively; the constant in each case is said to instantiate the quantifier. c is a constant that does not occur so far on the branch. a is any constant on the branch. (If there aren’t any, we select one at will.) If one is checking lines to note that one has finished with them, then one can never check a line of the form ∀xA, since it is possible that a new constant will be introduced on the branch (by PI), and hence that we will have to come back and apply UI to the new constant. (A useful trick is, instead of checking the line, to write beside it all the constants with which it has been instantiated.) (266)
[A Rule Against Partial Application of Tableau Rules]
[We cannot apply a rule to an internal part of a line but only to the whole line itself. So we should not have ¬(A ∧ Bx(a) coming after ¬(A ∧ ∀xB).]
[I might not have the next part right, but it seems to be the following. Priest will show something we cannot do, and he will give an example of it. In the example, we apply a rule to one part of a line rather than to a whole line, which we are not allowed to do. He has:
¬(A ∧ ∀xB)
↓
¬(A ∧ Bx(a))
So my impression is that we would need to decompose it first on the basis of the propositional operators, which are main operators here, and only when the universal quantifier becomes a main operator can we then develop the formula it is quantifying over. I may have this wrong however. So please check the quotation.]
Note that the tableaux rules are applied only to whole lines, not to parts thereof. Thus, consider the following:
¬(A ∧ ∀xB)
↓
¬(A ∧ Bx(a))
(for any a on the branch). This is not an application of UI.
(266)
[Closed Tableaux Notation]
[Priest will “write Σ ⊢ A to mean that there is a closed tableau whose initial list comprises the members of Σ together with the negation of A” (266-267).]
[(ditto)]
If Σ is finite, I will write Σ ⊢ A to mean that there is a closed tableau whose initial list comprises the members of Σ together with the negation | of A. (We will come to tableaux where Σ is infinite later.) Note that all the formulas on a tableau are closed.
(266-267)
[The Non-Restriction on Rule Order]
[It does not matter what order we apply the tableau rules.]
[(ditto)]
It is true, though not entirely obvious, that the order in which one applies the rules does not matter. If the tableau closes it will close in whatever order the rules are applied, provided that every rule that can be applied is applied. Similarly if the tableau is open. This is, in fact, a simple corollary of the Soundness and Completeness Lemmas (see 12.8.10), and holds for all tableaux for which appropriate versions of these lemmas can be proved. This includes all the tableau systems that we will meet in this part of the book. Again, I will not keep mentioning the fact.
(267)
[Tableau Example 1]
[Priest then gives a first example tableau for a valid inference.]
[(ditto)]
Here is a tableau to show that ∀x(Px ⊃ Qx), ∀x(Qx ⊃ Sx) ⊢ ∀x(Px ⊃ Sx).
∀x(Px ⊃ Qx), ∀x(Qx ⊃ Sx) ⊢ ∀x(Px ⊃ Sx)
1.
.
2.
.
3.
.
4.
.
5.
.
6.
.
7.
.
8.
.
9.
.
10.
.
11.
.
∀x(Px ⊃ Qx)
↓
∀x(Qx ⊃ Sx)
↓
¬∀x(Px ⊃ Sx)
↓
∃x¬(Px ⊃ Sx)
↓
¬(Pc ⊃ Sc)
↓
Pc
↓
¬Sc
↓
Pc ⊃ Qc
↓
Qc ⊃ Sc
↙ ↘
¬Pc Qc
× ↙ ↘
¬Qc Sc
× ×
P
.
P
.
P
.
3¬∀
.
4PI
.
5¬⊃
.
5¬⊃
.
1UI
.
2UI
.
8⊃
(10×6)
9⊃
(11a×10
;11b×7)
valid.
(267, enumeration and step accounting are my own and are probably mistaken)
[Tableau Example 2]
[Priest next gives a second example tableau for a valid inference.]
[(ditto)]
Here is another to show that ⊢ ∀xA ⊃ ∃xA.
⊢ ∀xA ⊃ ∃xA
1.
.
2.
.
3.
.
4.
.
5.
.
6.
.
¬(∀xA ⊃ ∃xA)
↓
∀xA
↓
¬∃xA
↓
∀x¬A
↓
Ax(a)
↓
¬Ax(a)
×
P
.
1¬⊃
.
1¬⊃
.
3¬∃
.
2UI
.
4UI
(6×5)
valid
(267, enumeration and step accounting are my own and are probably mistaken)
a is any constant that occurs in A, if there is one, or a new one if there isn’t.
(267)
[Tableau Example 3]
[Priest then gives a third example tableau, this time for an invalid inference.]
[(ditto)]
Here is a tableau to show that ∃x(Px ⊃ Qx) ⊬ ∀x¬Qx.
∃x(Px ⊃ Qx) ⊬ ∀x¬Qx
1.
.
2.
.
3.
.
4.
.
5.
.
6.
.
7.
.
∃x(Px ⊃ Qx)
↓
¬∀x¬Qx
↓
Pc ⊃ Qc
↓
∃x¬¬Qx
↓
¬¬Qa
↓
Qa
↙ ↘
¬Pc Qc
P
.
P
.
1PI
.
2¬∀
.
4PI
.
5¬¬
.
3⊃
(open)
invalid
(267, enumeration and step accounting are my own and are probably mistaken)
(268)
[Counter-Models]
[We construct counter-models from open branches in the following way: “take a domain which contains a distinct object, ∂b, for every constant, b, on the branch. v(b) is ∂b. v(P) is the set of n-tuples ⟨∂b1, . . . , ∂bn⟩ such that Pb1 . . . bn occurs on the branch. Of course, if ¬Pb1 . . . bn is on the branch, ⟨∂b1, . . . , ∂bn⟩ ∉ v(P), since the branch is open. (If a predicate or constant does not occur on the branch, the value given to it by v is a don’t care condition: it can be anything one likes)” (268).]
[Priest will now explain how to construct counter-models. Recall from section 12.2.2 that we are dealing with variables, x, y, z and constants a, b, and c etc. We also have formulas A, B, C and predicates P, Q, S etc. In our tableau, we also are using variables and constants. Now, recall from section 12.3.1 that “if c is a constant, v(c) is a member of D.” For our counter-model, it seems, we will be assigning domain objects to constants. For any constant b on the open branch, we designate a domain object ∂b such that v(b) is ∂b. Now, just as the v function assigns objects in the domain to constants, we will assign tuples of domain objects to predicates on the open branch. And, if we have any negations on the open branch, we will say that the corresponding tuple will not be including in the set generated by the v function operating on the predicate in question. If a constant or predicate does not occur on the branch, then we can assign it anything we want. Priest calls this a “don’t care” condition. Priest then makes the counter-model for section 12.4.7 above to illustrate, taking the leftmost branch. There our domain has the objects for constants c and a. So we write: D = {∂c, ∂a}; v(c) = ∂c, v(a) = ∂a. We have two predicates, ¬Pc and Qa. For Qa, we see that we assign the object for a to Q. So we have in our counter-model v(Q) = {∂a}. For the ¬Pc, I am a little confused why we write v(P) = φ. I am guessing it is for the following reason. We know that the object for c cannot be assigned to P on account of the negation in the formulation. But we also have not assigned the object a either. There are only those two in our domain, so v(P) = φ. That is my guess. Priest next makes a depiction for the counter-model. In it, the × means that the object is not in the predicate extension, while the √ means that it is. So:
| ∂c | ∂a | |
| P | × | × |
| Q | × | √ |
(Maybe if we look at the original inference, we will see how this works. It was: ∃x(Px ⊃ Qx) ⊬ ∀x¬Qx. We want to make the premise true and the conclusion false. We can see how this counter-model makes the conclusion false. If a is Q, then of course it is not the case that there are no things that are Q. For the premise, I need to guess, because I am not sure how it works here. We have a conditional, and we know that the consequent is true, because there in fact is an x that is Q, namely, a. But in our counter-model, there are no x’s that are P. So the antecedent is false. That makes the whole conditional true, thus we have the premise as true but the conclusion as false. Here now is the quotation so you can see.]
]
To read off a counter-model from an open branch, we take a domain which contains a distinct object, ∂b, for every constant, b, on the branch. v(b) is ∂b. v(P) is the set of n-tuples ⟨∂b1, . . . , ∂bn⟩ such that Pb1 . . . bn occurs on the branch. Of course, if ¬Pb1 . . . bn is on the branch, ⟨∂b1, . . . , ∂bn⟩ ∉ v(P), since the branch is open. (If a predicate or constant does not occur on the branch, the value given to it by v is a don’t care condition: it can be anything one likes.)3 Thus, in the example of 12.4.7, the counter-model given by the leftmost open branch is an interpretation ⟨D, v⟩, such that D = {∂c, ∂a}; v(c) = ∂c, v(a) = ∂a. For predicates, v(P) = φ, v(Q) = {∂a}; we may depict these in the following table:
∂c ∂a P × × Q × √
The tick means that the object in the column is in the extension of the predicate in the row. A cross means that it is not.
(268)
3. This is not the only interpretation compatible with the information on the branch. What is, in fact, required is that ⟨∂b1, . . . , ∂bn⟩ ∈ v(P) if Pb1 . . . bn is on the branch, and ⟨∂b1, . . . , ∂bn⟩⟩ ∉ v(P) if ¬Pb1 . . . bn is on the branch. Other members of v(P) are, strictly speaking, don’t cares. For other sorts of tableau that we will meet in this part of the book, however, the absence of a piece of information on a branch does not mean that it is a don’t care condition. For uniformity, then, we will stick with the recipe given in the text.
(268)
[Checking the Truth Values of Formulas]
[We can check which formulas are true by seeing if the model makes them so.]
[(I may not entirely grasp the next idea, but it seems to be the following. Our counter-models have limited domains. So suppose we want to know for an interpretation if a formula with an existentially quantified variable is true. So we want to know if ∃xA is true in the interpretation. We would say it is true if there is on the branch some non-negated formula in which a constant substitutes for the existentially quantified variable. So ∃xA is true in the interpretation if there is an Ax(b) that is true (where ‘b’ is a constant on the branch.) Similarly, ∀xA is true in the interpretation if Ax(b) is true for every b on the branch. Given the way the counter-model is set up, we can confirm that the formulas on all the lines of our tableau in section 12.4.7 are true.]
As is clear, every object in the domain has a name on the branch. To check that a formula of the form ∃xA is true in the interpretation, it therefore suffices to show that some sentence of the form Ax(b) is true, where b is some constant on the branch. Similarly, to check that a formula | of the form ∀xA is true in the interpretation, it suffices to show that Ax(b) is true, for every b on the branch. (See 12.3.5.) Bearing this in mind, it is easy to check that the following hold in the interpretation of 12.4.8 (running down each column):
¬Pc ¬¬Qa Pc ⊃ Qc ∃x¬¬Qx ∃x(Px ⊃ Qx) ¬∀x¬Qx
This shows that the interpretation is indeed a counter-model.
(269)
[Infinite Tableaux]
[Tableaux can be infinite. One way this happens is if there is an endless generation of new constants on account of repeating applications of instantiation.]
[(ditto)]
Note that an open branch of a tableau may well be infinite. Thus, consider the following tableau, which shows that ⊬ ∃x∀ySxy.
⊬ ∃x∀ySxy
1.
.
2.
.
3.
.
4.
.
5.
.
6.
.
7.
.
8.
.
¬∃x∀ySxy
↓
∀x¬∀ySxy
↓
¬∀ySay
↓
∃y¬Say
↓
¬Sab
↓
¬∀ySby
↓
∃y¬Sby
↓
¬Sbc
⫶
P
.
¬∃
.
2UI
.
3¬∀
.
4PI
.
2UI
.
6¬∀
.
4PI
(open)
invalid
(267, enumeration and step accounting are my own and are probably mistaken)
At the fifth line the particular quantifier is instantiated with the new constant b. But then we have to go back and instantiate the universal quantifier at line two; and this starts the procedure all over again. The tableau never closes, and goes on to infinity. In this case it is easy to read off the countermodel. The domain comprises ∂a, ∂b, ∂c,…; and the denotation of S (which is a set of ordered pairs) looks like this:
S ∂a ∂b ∂c ∂d . . . ∂a × ∂b × ∂c × ⫶ ⋱ |
Given the recipe of 12.4.8, the blank squares also contain crosses, but it is the ones shown that are essential. Given them, we have the following:
¬Sab
so
¬∀ySay
¬Sbc
so
¬∀ySby
⫶
⫶
so
¬∃x∀ySxy
(269-270)
[Constructing Counter-Models for Infinite Tableaux]
[When tableaux are infinite, we can use guesswork to formulate counter-models.]
[(I could have this next idea wrong, but it might be the following. Since infinite tableaux have no limit to their constants, it is not obvious how to make a counter-model. Priest says you can still determine them using guesswork, and he gives an example for the one above.]
In many cases where a tree is infinite (though not all) a simple finite counter-model can be found by intelligent guesswork. Thus, for 12.4.10 the following will do, as can be checked:
S ∂a ∂b P √ × Q × √
Neither ∂a nor ∂b relates to everything via S.
(270)
[Ensuring the Completeness of Infinite Tableaux]
[Priest next provides an algorithm for ensuring that infinite tableaux are complete: “(1) For each branch in turn (there is only a finite number at any stage of the construction), we run down the formulas on the branch, applying any rule that generates something not already on the branch. (In the case of a rule such as UI, which has multiple applications, we make all the applications possible at this stage.) (2) We then go back and repeat the process” (270).]
[(ditto)]
To make sure that a tableau does not close, it is necessary to ensure that all the rules that can be applied have been applied, that is, that every branch is complete. (A completed branch is not necessarily finite.) It is not entirely obvious for first-order tableaux, and for all the other tableaux with which we will be concerned in this part of the book, that complete branches can always be constructed. A simple algorithm (not necessarily the most efficient) for ensuring that every rule that can be applied is applied is as follows. (1) For each branch in turn (there is only a finite number at any stage of the construction), we run down the formulas on the branch, applying any rule that generates something not already on the branch. (In the case of a rule such as UI, which has multiple applications, we make all the applications possible at this stage.) (2) We then go back and repeat the process. (Needless to say, it is only a few rules – UI in the case of classical first order logic – where repeating the process with formulas already traversed in this process may produce something new on a branch.)
(270)
[The Soundness and Completeness of the Tableaux]
[“The tableaux are sound and complete with respect to the semantics” (270).]
[(ditto)]
The tableaux are sound and complete with respect to the semantics. This is proved in 12.8.
(270)
[Examining the Behavior of Quantifiers in their Interaction with Propositional Operators]
[In order to show the behavior of quantifiers, Priest lists the ways that the quantifiers interact with the propositional operators.]
[(ditto)]
In understanding the behaviour of quantifiers in a logic, perhaps the most important thing is to know how they interact with the propositional operators. In classical logic, the interactions are as follows. | ‘A ⊣⊢ B’ means ‘A ⊢ B and B ⊢ A’. C is any closed formula. A * at the end of a line indicates that the converse does not hold, in the sense that there are instances that are not valid. (So, for example, in the first line for Negation, if A is Px, we have ¬∀xPx ⊬ ∀x¬Px.) Where the converse does not hold, there is often a restricted version involving a closed formula that does. Where this exists, it is given on the next line. Verification of all these facts is left as an exercise.
1. No Operators
(a) ∀xC ⊣⊢ C
(b) ∃xC ⊣⊢ C
2. Negation
(a) ∀x¬A ⊢ ¬∀xA *
(b) ¬∀xC ⊢ ∀x¬C
(c) ¬∃xA ⊢ ∃x¬A *
(d) ∃x¬C ⊢ ¬∃xC
(e) ¬∃xA ⊣⊢ ∀x¬A
(f) ¬∀xA ⊣⊢ ∃x¬A
3. Disjunction
(a) ∀xA ∨ ∀xB ⊢ ∀x(A ∨ B) *
(b) ∀x(A ∨ C) ⊢ ∀xA ∨ C
(c) ∃xA ∨ ∃xB ⊣⊢ ∃x(A ∨ B)
(d) ∀xA ∨ ∀xB ⊢ ∃x(A ∨ B) *
(e) ∀x(A ∨ B) ⊢ ∃xA ∨ ∃xB *
4. Conjunction
(a) ∀xA ∧ ∀xB ⊣⊢ ∀x(A ∧ B)
(b) ∃x(A ∧ B) ⊢ ∃xA ∧ ∃xB *
(c) ∃xA ∧ C ⊢ ∃x(A ∧ C)
(d) ∀xA ∧ ∀xB ⊢ ∃x(A ∧ B) *
(e) ∀x(A ∧ B) ⊢ ∃xA ∧ ∃xB *
5. Conditional
(a) ∀x(A ⊃ B) ⊢ ∀xA ⊃ ∀xB *
(b) C ⊃ ∀xB ⊢ ∀x(C ⊃ B)
(c) ∃xA ⊃ ∃xB ⊢ ∃x(A ⊃ B) *
(d) ∃x(C ⊃ B) ⊢ C ⊃ ∃xB
(e) ∀x(A ⊃ B) ⊢ ∃xA ⊃ ∃xB *
(f) ∃xA ⊃ C ⊢ ∀x(A ⊃ C)
|
(g) ∀xA ⊃ ∀xB ⊢ ∃x(A ⊃ B) *
(h) ∃x(A ⊃ C) ⊢ ∀xA ⊃ C
Most of the logics we will be considering in this book agree with classical logic in cases 1–4, though 1 breaks down in free logic, and there are some very significant differences in cases 2 and 3 (negation and disjunction) for intuitionist logic. In case 5, however – as one might expect in the light of Part I – nearly all the logics diverge (for the appropriate conditional (⥽, ⊐, →, etc.)).
(271-272)
From:
Priest, Graham. 2008 [2001]. An Introduction to Non-Classical Logic: From If to Is, 2nd edn. Cambridge: Cambridge University.
No comments:
Post a Comment