Stronger Systems

Philosophy 244: #5—Stronger Systems Modalities Modalities are modal statuses, like being necessary, or possible, or not necessarily possibly necessary, or possibly necessarily necessary, or none of these. An ”iterated” modality is a finite number of boxes and diamonds all lined up in a row, e.g., 22323. Systems stronger than T are mainly to be distinguished from T and from each other by their handling of iterated modalities. The question is, how many logically distinct such modalities does a system recognize? Which iterated modalities are equivalent to simpler, shorter, such modalities, in particular modalities of length one? A formula like 33α ≡ 3α, which tells us that a longer string of boxes and diamonds is equivalent to a shorter one, is called a reduction law. The obvious candidates to begin with are 3α ≡ 23α 2α ≡ 32α. 3α ≡ 33α 2α ≡ 22α R1 R2 R3 R4 One half of each equivalence is already a theorem of T, so the formulas to focus on are R1a R2a R3a R4a 3α ⊃ 23α 32α ⊃ 2α. 33α ⊃ 3α 2α ⊃ 22α As it turns out, R1a and R2a are equivalent in T, and likewise R3a and R4a. So it’ll be enough to consider R1a and R4a as candidate axioms. R4a for its part is deducible from R1a. So there are really two candidate axioms to considered here: R4a by itself, or (for a stronger system) R1a by itself. The systems that result are S4 (= T + 2α ⊃ 22α), and S5 (= T + 3α ⊃ 23α). Start with the weaker system, S4. Our first theorem is to confirm that R3a really does follow from R4a. S4(1) 33p ⊃ 3p 1 2¬p ⊃ 22¬p T[¬p/p] 2 ¬3p ⊃ ¬33p (1)xLMI 3 33p ⊃ 3p (2)xPC S4(2) 2p ≡ 22p – easy S4(3) 3p ≡ 33p – easy S4(4) 323p ⊃ 3p 1 23p ⊃ 3p T[3p/p] 2 323p ⊃ 33p (1)xDR3 3 323p ⊃ 3p (2), S4(1)xSyll S4(5) 23p ⊃ 2323p 1 23p ⊃ 323p T1[23p/p] 2 223p ⊃ 2323p (1)xDR1 3 23p ⊃ 2323p (2), S4(2)xSyll S4(6) 23p ≡ 2323p S4(7) 32p ≡ 32323p — S4(5), other direction by S4(4)xDR1 — use LMI 1 Hughes and Cresswell say that “whenever a proposition is logically necessary, this is never a matter of accident but is alway something which is logically bound to be the case” (52). Is that right? Certainly it’s not a matter of accident but logical necessity involves more than that. On the obvious reading, where the logically necessary is that which can be proved in pure logic, it seems questionable. Is it supposed to be a theorem of logic that p ⊃p is a theorem of logic? “theorem of logic” is not even part of the formal language. Arthur Pap had a whole book (Semantics and Necessary Truth) trying to figure out the modal logic of analyticity. Is it true by virtue of meaning that p⊃p is true by virtue of meaning? Philosophically one has to tread carefully here; formally things are not so difficult. Modalities in S4 A modality is any unbroken sequence of zero or more monadic operators: ¬, 2, 3. A pure or affirmative modality contains only 2 and 3. Given LMI , any modality can be expressed as a pure modality with or without a ¬ in front. (Why?) So expressed the modality is in standard form; we’ll assume that all modalities from now on are in standard form. A modality (in standard form!) is iterated if it contains more than one modal operator. It’s affirmative or negative according to whether it starts with a ¬ (the only place ¬ can go in a standard form modality). Modalities A and B are equivalent if intersubstitutable everywhere in all theorems of the relevant system. Given our rules that’s the same as Ap ≡ Bp being a theorem. Time to count some modalities! Fact S4 has (up to equivalence) exactly fourteen modalities, to wit: (i) ¬, (ii) 2, (iii) 3, (iv) 23 , (v) 32, (vi) 232, (vii) 323, and their negations. Proof of at most 14: Consider “pure” or “affirmative” modalities first. (i) is the only 0-operator pure modality, and (ii) and (iii) are the only one-operator pure modalities. (iv) and (v) are the only irreducibly two-operator pure modalities because by S4(2) and S4(3), double 2 and double 3 are equivalent to single 2 and 3. For the same reason, the only “new” three-operator modalities are (vi) and (vii). Adding a fourth operator to any of these is always redundant by S4(2) and S4(3), or else gives you back (iv) or (v) byu S4(6) or S4(7). Likewise for the negative cases. At least 14. We have to show that these are distinct; that’s for later. The implication relations are set out in this diagram (from p. 56), << 2α 232α >> << >> 23α α >> << 32α << 323α >> 3α Validity for S4 An S4 frame is a such that R is a reflexive and transitive relation on W, that is, each w sees R itself, and w seesR any world that is visibleR from a world visibleR from w can seeR . A wff is S4-valid iff it’s valid in all reflexive, transitive frames (S4frames). To establish soundness it suffices by Prop. 2.2 to show that the characteristic S4 axiom 2p⊃22p is valid in all transitive frames. So: let be a transitive frame and a model on that frame, and suppose for contradiction that for some w in W, V (2α⊃22α,w )=0. Then 1. V (2p,w )=1 and V (22p,w )=0, so 2. V (p,u)=1 for all u visible from w, while V (2p,u)=0 for some such world, so 3. V (p,u)=1 for all u visible from w, but V (p,v )=0 for some v visible from u 2 You might wonder at this point how many distinct modalities T contains. The answer is ”infinitely many.” It’s worse even than that; T has no reduction laws whatsoever. Lengthening a modality always gives you something of a new logical strength. Contradiction since v is visible from w by transitivity; V (p,v )=0 by (iii) yet V (p,v ) must be 1 by (i). 2p=1, 22p=0 w v >> ∧ !!! p = 0 (u), p = 1 (w ) >u p = 1 (w ), 2p = 0 (w ) System S5 This is defined as system T plus R1a from the first page, now called E. E 3p⊃23p To show that S5 is indeed stronger than S4 we need to derive 4 in S5. Here goes: 4 1 2 3 4 2p⊃ 22q 2p ⊃ 32p 32p ≡ 232p 2p ⊃ 232p 2p ⊃ 22p S5(1) 32p ⊃ 2p S5(2) 3p ≡ 23p S5(3) 2p ≡ 23p T1[2p /p] S5(2)[2p/p] (1),(2)xEq (3),S5(3)xEq] The proofs are like those of S4(1-3) except using E instead of 4. A few more theorems: How do we show that S5 is a proper extension of S4? One way would be to argue by induction that E is not provable in S4; but that gives no insight and takes forever. Better to show that there’s an S4-frame on which E comes out false. The frame has two worlds w and u; each can see itself, and w can see u, but u cant see w. (So accessibility isn’t symmetric.) Let V be a valuation making p true in w but not u. Then E’s antecedent 3p is V-true at w because w can see itself; but its consequent is not V-true at w because w can see a world at which 3p is untrue, namely u. p = 1, 3p = 1, 23p = 0 w <  Some theorems bearing on the number of modalities in S5. >u S5(4) S5(5) S5(6) S5(7) 2(p∨2q) ≡ 2p∨2q 3(p∨2q) ≡ 2p∨3q 3(p ∨3q) ≡ 3p ∨3q 3(p∨2q) ≡ 3p∨2q p = 0, 3p = 0 All the four reduction laws R1-4 hold in S5. The result is that given any (affirmative) iterated modality, you can ignore all the operators except the last. From this we see that S5 has at most six distinct modalities, viz. (i) null, (ii) 2, (iii) 3, and their negations. The six are clearly distinct, so S5 has exactly six modalities. Validity in S5 An S5-frame is one whose accessibility relation is reflexive, transitive, and symmetric, ie., an equivalence relation. Am equivalence relation partitions the domain of worlds into disjoint, jointly exhaustive cells (equivalence classes). If there is more than one equivalence class the frame might as well be considered a bunch of different frames, one for each equivalence class of worlds, and where R is universal on each class. This is a boring complication so we choose to think of an S5-frame as one whose accessibility relation is universal on the given domain of worlds. (Think of the game analogy; you’ve essentially got different subgroups each unaware of the others other, playing distinct but indiscernible games.) For soundness it’s enough to show that E is valid on all equivalence frames. Is it? Suppose for contradiction that 3p=1 in w while 23p=0. Then p is true in every world w can see but 3p is false in some such world. So then what? 3 Examples of equivalence relations: equinumerosity, parallelism, same shape, same whatever. System B So far it looks like a linear series of ever-stronger systems: K < D < T < S4 < S5. This is not really the situation. The step from T to S5 can be broken up into parts— transitivity and symmetry—and if S4 takes the first substep without the second, there should be a system taking the second substep without the first. That system is B for some reason to do with Brouwer. Consider the following two theorems of S5. S5(8) p⊃23p S5(9) 32p⊃ p Neither of these is a theorem of S4. Adding either of them to S4 yieldss S5. But then, instead of axiomatizing S5 with K, T, and E T 2p⊃p E 3p ⊃23p, as we have done above, we could have used T 2p⊃p 4 2p⊃22p B p⊃23p Brouwer developed a logic— intuitionistic logic—that has p⊃∼∼p as a theorem but not ∼∼p⊃p. (Reductio proofs are suspect for Brouwer; deriving a contradiction from ∼p doesn’t really show why p show why p would be true, only that it had better not be false. Classical logicians are apt to think of Brouwer as interpreting negation “modally”: ∼p = 2¬p. Double-negation elimination assumes that what can’t be refuted is true, which is not obvious. ∼∼p⊃p says on this interpretation that p ⊃2¬2¬p, that is, 23p; p⊃∼∼p says that p⊃23p, which is axiom B. So a better map is If we had added B to T instead of 4, would have arrived at B = K+T,B instead of S4 = K + T,4. Basic Facts about B S5 B A B-frame is a frame whose accessibility relation is reflexive and symmetrical. B-validity is validity in every B-frame. To prove soundness we recall that (thanks to Propn. 2.2) it’s enough to show the wffs T and B are valid in every reflexive, symmetrical frame. We know T is valid in every reflexive frame, so ETS that B is valid in every symmetrical one. Suppose not; then there’s a w s.t. (i) V(p,w )=1 and (ii) V(23p,w )=0. By (ii), w can see a u s.t. V(3p)=0, whence u can’t see any v s.t. V(p,v )=1. But by symmetry, w itself is such a v ; u can see w and V(p,w )=1. Contradiction. Working in S4 + B, we can prove E (see book). So S4 + B is at least as strong as S4 + E is at least as strong as T + E =df S5. That adding B to S4 gives you a strictly stronger system shows that B was not already a theorem of S4. It can likewise be shown that 4 is not a theorem of B; find a B-frame that invalidates 4. Any reflexive, symmetrical, intransitive frame will do. So B and S4 are independent; neither is an extension of the other. But then B is not as strong as S5, since S5 and S4 are not independent. So the right diagram is the one we have drawn above: a diamond with S5 at the top and T at the bottom and S4 and B on either side. > < S4 > T < ∨ K ETS = ”It’s enough to show ...” s.t. = ”such that” Upward and onward? Stronger systems than S5 are rarely considered. But ones not weaker than S5 are, such as system is G for Godel. 2 in G is supposed to model provability in Peano Arithmetic. A modal wff like 2p⊃22p is meant to be theorem of G iff it’s a theorem of PA if something is provable it’s provably provable. G rejects the T axiom 2p⊃p in favor of 2(2p⊃p)⊃2p. G is not a theorem of S5. Why not? The intended interpretation is, roughly: a system can’t prove its own reliability with respect to a hypothesis, except by proving that hypothesis. Arithmetic, say, can’t establish its own reliability. G-frames are transitive, finite, and irreflexive. 4 It is not a theorem of PA that what’s provable is the case. If it were then by contraposition we’d get if something is false it’s not provable. PA can’t prove that on pain of proving its own consistency, which is not allowed by the Second Incompleteness Theorem. PA is an anti-expert about its own consistency; it proves it iff it is inconsistent.