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 I:
Propositional Logic
6.
Intuitionistic Logic
6.4
Tableaux for Intuitionistic Logic
Brief summary:
(6.4.1) Our tableaux for intuitionistic logic will build from those for modal logic, but with some modifications. In modal logic, the nodes take one of two forms: {1} A,i, where A is a formula and i is a natural number indicating the world in which the formula holds, or {2} irj, where i is a natural number for a world that accesses world j, also given as a natural number (the r stays as r). For our intuitionistic tableaux, “The first modification is that a node on the tableau is now of the form A,+i or A,−i. The first means, intuitively, that A is true at world i; the second means that A is false at i” (107) Previously we did not need this information in the tableaux about truth and falsity, because A’s being false in a world was equivalent to its negation being true, and so we would represent that with ¬A,i. (It seems then that being “false” or at least lacking a proof, here in intuitionistic systems, means either that {1} within some world, there is a disproof (a proof that there is no proof) for a formula, in other words, that for instance ⇁A in world 0 (maybe written as vwo (⇁A) = 1 and) symbolized as ⇁A,+0 in the tableaux, which means that it is the case that there is a disproof for A in world 0, or that {2} there is currently neither a proof for a formula nor a disproof for that formula (I am not sure how that is written normally, maybe for instance as vwo (A) = 0, but it is) written as A,−0 in the tableaux, meaning that it is not the case that there is a proof for A in world 0. (If there were a disproof, and thus if vwo (⇁A) = 1, then I think still you would thereby have vwo (A) = 0).) (6.4.2) We form the initial list of our tableaux by setting all premises to true in world 0, thus as: B,+0. And the conclusion is set to false in world 0, thus as: A,−0. (6.4.3) We close a branch on our tableau when we obtain a contradiction, that is, “just when we have nodes of the form A,+i and A,−i. (6.4.4) Priest then gives the tableaux rules (see below. The list includes the accessibility rules from the next section also).
| Conjunction Development, True (∧D,+) |
| A ∧ B,+i ↓ A,+i B,+i |
| Conjunction Development, False (∧D,−) |
| A ∧ B,−i ↙ ↘ A,−i B,−i |
| Disjunction Development, True (∨D,+) |
| A ∨ B,+i ↙ ↘ A,+i B,+i |
| Disjunction Development, False (∨D,−) |
| A ∨ B,−i ↓ ¬A,−i ↓ ¬B,−i |
| Conditional Development, True (⊐D,+) |
| A ⊐ B,+i irj ↙ ↘ A,−j B,+j
applied for every j on the branch |
| Conditional Development, False (⊐D,−) |
| A ⊐ B,−i ↓ irj A,+j ↓ B,−j
the j is new |
| Negation Development, True (⇁D,+) |
| ⇁A,+i irj ↓ A,−j
applied for every j on the branch |
| Negation Development, False (⇁D,−) |
| ⇁A,−i ↓ irj A,+j
the j is new |
| Heredity, True (hD,+) |
| p,+i irj ↓ p,+j . p is any propositional parameter, applied to every j (distinct from i) |
(modified from p.108, section 6.4.4)
| ρ, Reflexivity (ρrD) |
| ρ . ↓ iri |
| τ, Transitivity (τrD) |
| τ irj jrk ↓ irk |
Priest has us “Note that, in particular, we can never ‘tick off’ any node of the form A ⊐ B,+i or ⇁A,+i, since we may have to come back and reapply the rule if anything of the form irj turns up” (108-109). (6.4.5) We also have the ρ reflexivity and τ transitivity accessibility rules (shown in the listing above). (6.4.6) Priest next gives an example tableau to show that ⊢I p ⊐ ⇁⇁p. (6.4.7) Priest next gives another example tableau that shows that p ⊐ q ⊬I ⇁p ∨ q. (6.4.8) “Counter-models are read off from an open branch of a tableau in a natural way. The worlds and accessibility relation are as the branch of the tableau specifies. If a node of the form p,+i occurs on the branch, p is set to true at wi ; otherwise, p is false at wi . (In particular, if a node of the form p,−i occurs on the branch, p is set to false at wi )” (110). (6.4.9) Priest then gives a more visual portrayal of the counter-model from above section 6.4.8. Here “We indicate the fact that p is true (at a world) by +p, and the fact that it is false by −p” (110). (6.4.10) “The tableaux are sound and complete with respect to the semantics” (111). (6.4.11) Priest then gives an example of an infinite open tableau. (6.4.12) Priest then shows how it is easier to directly make a counter-model in cases of infinite tableaux.
[The Node Formulation in Intuitionistic Tableaux]
[The Initial List]
[Branch Closure]
[The Tableaux Rules]
[The ρ Reflexivity and τ Transitivity Accessibility Rules]
[Tableau Example 1: Valid]
[Tableau Example 2: Invalid]
[Counter-Models Explained]
[Counter-Model Illustrations]
[The Soundness and Completeness of the Tableaux]
[Infinite Open Tableaux]
[Counter-Models for Infinite Tableaux]
Summary
[The Node Formulation in Intuitionistic Tableaux]
[Our tableaux for intuitionistic logic will build from those for modal logic, but with some modifications. In modal logic, the nodes take one of two forms: {1} A,i, where A is a formula and i is a natural number indicating the world in which the formula holds, or {2} irj, where i is a natural number for a world that accesses world j, also given as a natural number (the r stays as r). For our intuitionistic tableaux, “The first modification is that a node on the tableau is now of the form A,+i or A,−i. The first means, intuitively, that A is true at world i; the second means that A is false at i” (107) Previously we did not need this information in the tableaux about truth and falsity, because A’s being false in a world was equivalent to its negation being true, and so we would represent that with ¬A,i. (It seems then that being “false” or at least lacking a proof, here in intuitionistic systems, means either that {1} within some world, there is a disproof (a proof that there is no proof) for a formula, in other words, that for instance ⇁A in world 0 (maybe written as vwo (⇁A) = 1 and) symbolized as ⇁A,+0 in the tableaux, which means that it is the case that there is a disproof for A in world 0, or that {2} there is currently neither a proof for a formula nor a disproof for that formula (I am not sure how that is written normally, maybe for instance as vwo (A) = 0, but it is) written as A,−0 in the tableaux, meaning that it is not the case that there is a proof for A in world 0. (If there were a disproof, and thus if vwo (⇁A) = 1, then I think still you would thereby have vwo (A) = 0).)]
[We will now learn how to construct tableaux for intuitionistic logic. Let us first review some relevant matters. In section 6.2, Priest discussed the basic motivations for intuitionistic logic. He first noted that we can understand the meaning of sentences we never heard of before (6.2.1). One explanation for this is compositionality, which says that “the meaning of a sentence is determined by the meanings of its parts, and of the grammatical construction which composes these” (p.103, section 6.2.2). If meaning is given by truth-conditions, then by compositionality the meaning of sentences built-up using connectives is based on the truth-functionality of the connectives (6.2.3). Truth itself according to a correspondence theory is the correspondence of what a formula says and the facts of an extra-linguistic reality. But what about mathematical formulas? Are there real, extra-linguistic mathematical objects? (6.2.4) Mathematical realists hold that there is an extra-linguistic reality corresponding to the truths of mathematical formulations like “2 + 3 = 5;” they think for example that there are “objectively existing mathematical objects, like 3 and 5.” Intuitionists however think rather that we should not apply the correspondence theory of truth to mathematical formulations (6.2.5). Intuitionism expresses a statement’s meaning on the basis of its proof conditions, which are the conditions under which the sentence is proved (6.2.6). The proof condition of a simple sentence is whatever we would take to be a sufficient proof, and those for complex sentences that are built up using connectives will be similar to the normal conditions only now using the notion of proof (note that ⇁ and ⊐ symbolize negation and the conditional):
A proof of A ∧ B is a pair comprising a proof of A and a proof of B.
A proof of A ∨ B is a proof of A or a proof of B.
A proof of ⇁A is a proof that there is no proof of A.
A proof of A ⊐ B is A construction that, given any proof of A, can be applied to give a proof of B.
(104, section 6.2.7)
Lastly, Priest noted that these proof conditions cannot validate excluded middle, because there are formulas that cannot be proved nor can it be proven that there is no proof for them (6.2.8). Then in section 6.3, Priest outlined the semantics for intuitionistic logic. He first notes that there is a possible worlds semantics that “arguably captures the above ideas” (6.3.1). The only connectives in our intuitionist logic are ∧, ∨, ⇁ and ⊐ (with the last two being negation and the conditional, respectively) (6.3.2). Our intuitionistic possible worlds semantics takes the structure ⟨W, R, v⟩. It is mostly the same as logic Kρτ, meaning that it is a normal modal logic in which the R accessibility relation is reflexive (all worlds have access to themselves) and transitive (whenever a first world has access to a second and that second to a third, then the first has access to that third as well.) There is one additional constraint, called the heredity condition, which means that when a proposition is true in one world, it it is true in all other worlds that are accessible from it (6.3.3). By means of certain rules we evaluate molecular formulas. Negation and the conditional involve accessible worlds (6.3.4). The heredity condition holds not just for propositional parameters but for all formulas (6.3.5).To see how the above interpretation captures intuitionist ideas, we first conceive of the way that information accumulates over time as being like one world (like our world at one moment) as being a set of proven things and another world accessible from the first having the same proven things and maybe more (like our world progressing later into a world perhaps with more information) (6.3.6). The possible world semantics for intuitionism captures the ideas in the proof conditions (6.3.7). We define validity in intuitionistic logic as truth preservation over all worlds of all interpretations, and we write intuitionistic logical consequence as ⊨I (6.3.8). If there is only one world, the intuitionistic interpretation is equivalent to a classical one. And intuitionistic logic is a sub-logic of classical logic, because everything that is intuitionistically valid is classical valid, but not everything classical valid is intuitionistically valid (6.3.9). (We turn now to the current section). Now, our intuitionistic tableaux will be a modification of normal modal logic tableaux (see section 2.4). Recall in particular from section 2.4.1 that tableaux in modal logic take the same branching node structure as those for propositional logic. However, the nodes themselves have a different structure, and there are two possible ones. {1} A, i, where A is a formula and i is a natural number indicating the world in which the formula holds, or {2} irj, where i is a natural number for a world that accesses world j, also given as a natural number (the r stays as r). Priest says now that for our intuitionistic tableaux, “The first modification is that a node on the tableau is now of the form A,+i or A,−i. The first means, intuitively, that A is true at world i; the second means that A is false at i.” Previously we did not need this information about truth and falsity, because A’s being false in a world was equivalent to its negation being true, and so we would represent that with ¬A. (I am not certain about the situation yet, but it seems to me now to be the following. Being “false” or at least lacking a proof, here means either that {1} within some world, there is a disproof (a proof that there is no proof) for a formula, in other words, that for instance ⇁A in world 0 (maybe written as vwo (⇁A) = 1 and) symbolized as ⇁A,+0 in the tableaux, which means that it is the case that there is a disproof for A in world 0, or that {2} there is currently neither a proof for a formula nor a disproof for that formula (I am not sure how that is written normally, maybe for instance as vwo (A) = 0, but it is) written as A,−0 in the tableaux, meaning that it is not the case that there is a proof for A in world 0. (If there were a disproof, and thus if vwo (⇁A) = 1, then I think still you would thereby have vwo (A) = 0).)]
To obtain tableaux for intuitionist logic, we modify those for normal modal logics. The first modification is that a node on the tableau is now of the form A,+i or A,−i. The first means, intuitively, that A is true at world i; the second means that A is false at i. For previous modal logics, the fact that A was false at a world was indicated by ¬A, i. But now, A may be false at a world without ⇁A being true there.
(107)
[The Initial List]
[We form the initial list of our tableaux by setting all premises to true in world 0, thus as: B,+0. And the conclusion is set to false in world 0, thus as: A,−0.]
[ditto]
The initial list of a tableau for a given inference now comprises B,+0, for every premise, B, and A,−0, where A is the conclusion.
(107)
[Branch Closure]
[We close a branch on our tableau when we obtain a contradiction, that is, “just when we have nodes of the form A,+i and A,−i.]
[ditto]
Closure of a branch occurs just when we have nodes of the form A,+i and A,−i.
(108)
[The Tableaux Rules]
[Priest then gives the tableaux rules (see below). Priest has us “Note that, in particular, we can never ‘tick off’ any node of the form A ⊐ B,+i or ⇁A,+i, since we may have to come back and reapply the rule if anything of the form irj turns up” (108-109).]
[ditto]
The rules of the tableau for the connectives are as follows:
| Conjunction Development, True (∧D,+) |
| A ∧ B,+i ↓ A,+i B,+i |
| Conjunction Development, False (∧D,−) |
| A ∧ B,−i ↙ ↘ A,−i B,−i |
| Disjunction Development, True (∨D,+) |
| A ∨ B,+i ↙ ↘ A,+i B,+i |
| Disjunction Development, False (∨D,−) |
| A ∨ B,−i ↓ ¬A,−i ↓ ¬B,−i |
| Conditional Development, True (⊐D,+) |
| A ⊐ B,+i irj ↙ ↘ A,−j B,+j
applied for every j on the branch |
| Conditional Development, False (⊐D,−) |
| A ⊐ B,−i ↓ irj A,+j ↓ B,−j
the j is new |
| Negation Development, True (⇁D,+) |
| ⇁A,+i irj ↓ A,−j
applied for every j on the branch |
| Negation Development, False (⇁D,−) |
| ⇁A,−i ↓ irj A,+j
the j is new |
| Heredity, True (hD,+) |
| p,+i irj ↓ p,+j . p is any propositional parameter, applied to every j (distinct from i) |
(modified from p.108, section 6.4.4)
The rules for ∧ and ∨ are self-explanatory. The first rule for each of ⊐ and ⇁ is applied for every j on the branch. In the second, for each, the j is new. The rules are easier to remember if one recalls that A ⊐ B means, in effect, □(A ⊃ B), and ⇁A means, in effect, □¬A. Note that, in particular, we can never ‘tick off’ any node of the form A ⊐ B,+i or ⇁A,+i, since we may have to come back and reapply the rule if anything of the form irj turns up. The final rule is applied only to propositional parameters, and, again, to every j (distinct from i). The rule is required by the heredity condition, and we will refer to it as the heredity rule. Note that there is no corresponding rule for p, −i.
(108-109)
[The ρ Reflexivity and τ Transitivity Accessibility Rules]
[We also have the ρ reflexivity and τ transitivity accessibility rules.]
| ρ, Reflexivity (ρrD) |
| ρ . ↓ iri |
| τ, Transitivity (τrD) |
| τ irj jrk ↓ irk |
]
[Recall from section 3.2.3 the constraints on the accessibility relation that generate variations of a modal logic:
ρ (rho), reflexivity: for all w, wRw.
σ (sigma), symmetry: for all w1, w2, if w1Rw2, then w2Rw1.
τ (tau), transitivity: for all w1, w2, w3, if w1Rw2 and w2Rw3, then w1Rw3.
η (eta), extendability: for all w1, there is a w2 such that w1Rw2.
(p.36, section 3.2.3)
And recall the ρ, σ, and τ tableau rules from section 3.3.2.
| Tableaux Rules for Kρ, Kσ, and Kτ | ||
| ρ . ↓ iri . . “ρrD” | σ irj ↓ jri . . “σrD” | τ irj jrk ↓ irk . “τrD” |
(p.38, section 3.3.2 , with my naming additions)
Now recall from section 6.3.6 the idea that intuitionism can be understood in the following way. Successive times are worlds, but their relativities are such that there is heredity for affirmed information (so what is affirmed now is affirmed at all future worlds). But because of the “arrow of time,” something found true later does not mean it must be found true in the past. So the worlds do not have symmetrical access. And also note from the section above that the heredity rule is only for true statements. So something’s being false now does not mean it must be false in the future, event though if it is true now it must be true in the future.
Think of a world as a state of information at a certain time; intuitively, the things that hold at it are those things which are proved at this time. uRv is thought of as meaning that v is a possible extension of u, obtained by finding some number (possibly zero) of further proofs. Given this understanding, R is clearly reflexive and transitive. (For τ: any extension of an extension is an extension.) And the heredity condition is also intuitively correct. If something is proved, it stays proved, whatever else we prove.
(p.106, section 6.3.6)
Thus we do not have the symmetry σ rule, but just the ones for ρ (reflexivity) and τ (transitivity).]
We also have the rules ρ and τ (of 3.3.2), as required for the reflexivity and transitivity of R.
(109)
[Tableau Example 1: Valid]
[Priest next gives an example tableau to show that ⊢I p ⊐ ⇁⇁p.]
[ditto]
As an example, here is a tableau to show that ⊢I p ⊐ ⇁⇁p
| ⊢I p ⊐ ⇁⇁p | ||
| 1. .
2. .
3. .
4. .
5. .
6. .
7. .
8. .
9. .
10. .
11. .
12. | p ⊐ ⇁⇁p,−0 ↓ 0r0 ↓ 0r1 ↓ p,+1 ↓ ⇁⇁p,−1 ↓ 1r1 ↓ 1r2 ↓ ⇁p,+2 ↓ 2r2 ↓ 0r2 ↓ p,−2 ↓ p,+2 × | P .
1ρ .
1⊐− .
1⊐− .
1⊐− .
4ρ .
5⇁− .
5⇁− . 8ρ . 3,7τ . 8,9⇁+ .. 4,7h (12×11)
valid |
(enumeration and step accounting are my own and are probably mistaken)
(2)–(4) are obtained from (1) by the rule for false ⊐. (5) and (6) are obtained from (4) by the rule for false ⇁. (7) is obtained from (6) by the rule for true ⇁ (and the fact that 2r2). Finally, (8) is obtained from (3) by the heredity rule (and the fact that 1r2).4
(109)
4. Note a distinctive feature of intuitionist tableaux. Suppose that we had constructed the tableau using, not a propositional parameter, p, but an arbitrary formula, A. Then we could not apply the heredity rule to close off the tableau in the same way. But since anything of the form A ⊐⇁⇁A is logically true, and the tableau system is complete, tableaux for all such formulas will close, though not in a uniform way. (That is, for each sentence that A represents, the tableau will continue to closure in a different way.) This could be changed by making the heredity rule apply to all formulas, not just propositional parameters. And since heredity does hold for arbitrary formulas (6.3.5), this rule is sound. But this complicates tableaux enormously, and, by completeness, is unnecessary anyway.
(109)
[Tableau Example 2: Invalid]
[Priest next gives another example tableau that shows that p ⊐ q ⊬I ⇁p ∨ q.]
[ditto]
Here is another example to demonstrate that p ⊐ q ⊬I ⇁p ∨ q. (Since the inference is classically valid – when ⊐ and ⇁ are replaced by ⊃ and | ¬ – this shows that intuitionist logic is a proper sub-logic of classical logic.)
| p ⊐ q ⊬I ⇁p ∨ q | ||
| 1. .
2. .
3. .
4. .
5. .
6. .
7. .
8. .
9. .
10. | p ⊐ q,+0 ↓ ⇁p ∨ q,−0 ↓ 0r0 ↓ ⇁p,−0 ↓ q,−0 ↓ 0r1 ↓ p,+1 ↓ 1r1 ↙ ↘ p,−0 q,+0 ↙ ↘ × p,−1 q,+1 × | P .
P .
1ρ .
2∨− .
2∨− .
4⇁− .
4⇁− .
7ρ .
1,3⊐+ (9b×5) 2⊐+ (10a×7) open invalid |
(enumeration and step accounting are my own and are probably mistaken)
The sixth and seventh lines are given by the rule for false ⇁, applied to the fourth line. Both splits are caused by an application of the rule for true ⊐ to the first line, to worlds 0 and 1, respectively. Note that there are no possible applications of the heredity rule.
(109-110)
[Counter-Models Explained]
[“Counter-models are read off from an open branch of a tableau in a natural way. The worlds and accessibility relation are as the branch of the tableau specifies. If a node of the form p,+i occurs on the branch, p is set to true at wi ; otherwise, p is false at wi . (In particular, if a node of the form p,−i occurs on the branch, p is set to false at wi )” (110).]
[ditto]
Counter-models are read off from an open branch of a tableau in a natural way. The worlds and accessibility relation are as the branch of the tableau specifies. If a node of the form p,+i occurs on the branch, p is set to true at wi ; otherwise, p is false at wi . (In particular, if a node of the form p,−i occurs on the branch, p is set to false at wi .) Thus, reading from the open branch of the tableau of 6.4.7, W = {w0 , w1 }; w0 Rw0 , w0Rw1 and w1Rw1 ; vwo (p) = vwo (q) = 0 and vw1 (p) = vw1 (q) = 1.
(110)
[Counter-Model Illustrations]
[Priest then gives a more visual portrayal of the counter-model from above section 6.4.8. Here “We indicate the fact that p is true (at a world) by +p, and the fact that it is false by −p” (110).]
[ditto]
In pictures:
xx↷xxxxx↷
xxw0xx→xxw1
xx−pxxxx +p
xx−q xxxx+q
We indicate the fact that p is true (at a world) by +p, and the fact that it is false by −p. It is a simple matter to check directly that the interpretation is a counter-model. At every world accessible from w0 , p is false or q is true. | Hence, p ⊐ q is true at w0 . p is true at w1 ; hence ⇁p is false at w0 . But q is also false there. Hence, ⇁p ∨ q is false there.
(110-111)
[The Soundness and Completeness of the Tableaux]
[“The tableaux are sound and complete with respect to the semantics” (111).]
[ditto]
The tableaux are sound and complete with respect to the semantics. This is demonstrated in 6.7.
(111)
[Infinite Open Tableaux]
[Priest then gives an example of an infinite open tableau.]
[Recall from section 6.4.4 above that “we can never ‘tick off’ any node of the form A ⊐ B,+i or ⇁A,+i, since we may have to come back and reapply the rule if anything of the form irj turns up” (p.108, section 6.4.4). Here we will see how by obtaining ⇁⇁p,+i in one line, that means we must derive ⇁p,–j in another line by the true negation rule and transitivity. But then by the false negation rule, we will get a new world related to the previous one, causing us to redo the ⇁⇁p,+i line in that new world, which then means the pattern continues without termination.]
Note that, as for Kρτ , open tableaux for intuitionist logic may be infinite. Here, for example, is the start of a tableau which establishes that ⊬I ⇁⇁p ⊐ p :
⊬I ⇁⇁p ⊐ p
1.
.
2.
.
3.
.
4.
.
5.
.
6.
.
7.
.
8.
.
9.
.
10.
.
11.
.
12.
⇁⇁p ⊐ p,−0
↓
0r0
↓
0r1
↓
⇁⇁p,+1
↓
p,−1
↓
1r1
↓
⇁p,−1
↓
1r2
↓
p,+2
↓
2r2
↓
0r2
↓
⇁p,−2
↓
2r3
⫶
P
.
1ρ
.
1⊐−
.
1⊐−
.
1⊐−
.
4ρ
.
4⇁+
.
7⇁−
.
7⇁−
.
9ρ
.
3,8τ
.
4,8⇁+
..
12⇁−
open
invalid
(enumeration and step accounting are my own and are probably mistaken)
Every time we open a new world, i, the fourth line (and transitivity) requires us to write ⇁p, −i there; but this requires us to open a new world, j, such that irj and p, +j, and so on.
(111)
[Counter-Models for Infinite Tableaux]
[Priest then shows how it is easier to directly make a counter-model in cases of infinite tableaux.]
[ditto]
Again, as with Kρτ , in such cases it is usually easier to con- struct counter-models directly. Thus, for ⇁⇁p ⊐ p, the following will work:
xx↷xxxxx↷
xxw0xx→xxw1
xx−pxxxx +p
Since p is true at w1 , ⇁p is false at w0 and w1. Hence, ⇁⇁p is true at w0 . Since p is false there, ⇁⇁p ⊐ p is false at w0.
(111)
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