One of the really fun things I've been doing this summer is working with some really talented students (Graham Bounds, Michael Morrissey, Joel Musser, and Caitlin O Malley) on getting a version of modal logic that both respects the insights of proof theorists from Gentzen to Prawitz to Tennent and Restall and Simpson and that is also very easy to learn and use for students who have only taken an intro logic class and learned a Fitch style system (like the one in Barwise and Etchemendy's book). Alex Simpson's dissertation, which presents intuitionist modal logic in a Prawitz style tree system has made this possible.
Anyhow, I thought I'd share some of this for anyone who is interested. It's not rocket science, but I don't think anyone's done this so far (I might be completely wrong; if someone has, I'll publicize it here). Here I'll just present K and in another post show how one can get T, S4, and S5 by progressively adding inference rules that force accessibility to be reflexive, transitive, and symmetric.
First, some sample key proofs, the characteristic K axiom as well as the interderivability of possibility and necessity in K (as one would expect, one direction involves non-intuitionistic resources).
Proof:
1. | x: [](A --> B) for --> introduction
2. | | x: []A for --> introduction
3. | | | xRy for [] introduction
4. | | | y: A 2,3 [] elimination
5. | | | y: A --> B 1,3 [] elimination
6. | | | y: B 4,5 --> elimination
7. | | x: []B 3-6 [] introduction
8. | x: ([]A --> []B) 2-7 --> introduction
9. x:[](A --> B) --> ([]A --> []B) 1-8 --> introduction
Claim: |-K <>A --> ~[]~A
Proof:
1. | x: <>A for --> introduction
2. | | xRy for <> elimination
3. | | y: A for <> elimination
4. | | | x: []~A for ~ introduction
5. | | | y: ~A 2,4 [] elimination
6. | | | y: # 3,5 ~ elimination
7. | | x: ~[]~A 4-6 ~introduction
8. | x: ~[]~A 1,2/3-7 <>elimination
9. <>A --> ~[]~A 1-8 --> introduction
2b. Claim: |-K ~[]~A --> <>A
Proof:
1. | x: ~[]~A for --> introduction
2. | | x: ~<>A for ~ introduction
3. | | | xRy for [] introduction
4. | | | | y: A for ~ introduction
5. | | | | x: <>A 3,4 <> introduction
6. | | | | x: # 2,5 ~ elimination
7. | | | y: ~A 4-6 ~introduction
8. | | x: []~A 3-7 [] introduction
9. | | x: # 1, 8 ~elimination
10.| x: ~~<>A 2-9 ~introduction
11. | x: <>A 10 DNE
12. x: ~[]~A --> <>A 1-11--> introduction
The system just makes two changes to a normal Fitch style proper natural deduction system of classical logic. First, lines in the proofs are indexed to worlds. Second, introduction and elimination rules for possibility and necessity are added. For years people have kind of understood that something analogous to the way arbitrary names/eigenvariables are treated in first-order logic proofs is happening in modal logic proofs too, and I think people first did this explicitly with tableu systems of modal logic. But Simpson really nailed it down with his system.
In my presentation of K, the only major departure from Simpson (besides the system being Fitch style as opposed to Prawitz style) is that I do not define negation in terms of absurdity and the conditional. If you do it Simpson's original way, you can't define an independent minimal modal logic! I thought this was actually an interesting enough result to get another Analysis paper (my and Roy Cook's first publication showed something similar with respect to negation, implication, and zero equals one). But via e-mail Simpson showed me that you could still get a proper minimal modal logic with negation defined in terms of conditional and absurdity by adding a rule to his system that states that if absurdity holds at one world, it holds at all worlds. Since I can't see anything wrong with such a rule, there goes the sequal to me and Roy's paper (which is very sad, because we all know that The Empire Strikes Back is by far the best in the series). But nonetheless, I still treat negation in the manner of Neil Tennant, with its own set of rules, because if the sequal to me and Roy's paper can be rebooted in light of Simpon's response, it's going to be in terms of what is necessary for pursuing Fitch style proper natural deduction systems of relevant modal logics.
Otherwise, everything for K is strictly analogous to Simpson's Prawitz tree style treatment (for T, S4, and S5 there are more extreme deviations which simplify the Fitch proofs; I'll show those in the next post).
So first, here are the propositional rules
1. World indexed Minimal Logic Propositional Rules-
m. x: A
n. x: A m, reiteration
m. x: A m. x: (A & B)
n. x: B n. x: A m & elimination
o. x: (A & B) m, n & introduction
m. x: (A & B)
n. x: B m & elimination
m. x: A m. x: (A v B)
n. x: (A v B) m v introduction n. | x: A for v elimination
| :
m. x: B o. | y: C
n. x: (A v B) m v introduction p. | x: B for v elimination
| :
q. | y: C
r. y: C m, n-o,p-q v elimination
[Note: y can be equal to x!]
m. |x: A for --> introduction m. x: (A --> B)
| : n. x: A
n. | x: B o. x: B m, n --> elimination
o. x: (A --> B) m-n --> introduction
m. | x: A for ~ introduction m. x: A
| : n. x: ~A
n. | y: # o. y: # m, n ~ elimination
o. x: ~A m-n ~ introduction [Note: y can be equal to x!]
[Note: y can be equal to x!]
2. World Indexed Intuitionist Absurdity rule:
m. x: #
:
n. y: A m # elimination
[Note again that y can be equal to x.]
3. World Indexed Double Negation Elimination (to get full classical logic)
m. x: ~~A
n. x: A m, DNE
4. Introduction and elimination rules for [] and <>.
These rules allow us to introduce statements that world y is accessible from world x, via xRy. Then, possibility elimination and necessity introduction have restrictions with the variables referring to arbitrary worlds that are exactly analogous to restrictions on arbitrary names in existential elimination and universal introduction in proper natural deduction presentations of first-order predicate logic.
If you look at the rules you will see that the disanalogy comes with respect to possibility introduction and necessity elimination, which require much more than existential introduction and universal elimination. For example, the K rule for inferring <>P at world x requires that P be true at some world y, and that xRy. As far as I can tell, the normal modal logics that strengthen K basically make possibility introduction and universal elimination easier to use because they give you more facts about the accessibility relation. In the next post I'll show how this works with T, S4, and S5. But here are the rules. I'm not writing a textbook here, so I won't explain much more, but if you re-examine the proofs above you can see how cleanly they were derived both from the bottom-up in terms of what is required to introduce the operator in question and from the top-down in terms of what is licensed by an assertion of a sentence with that operator dominant. It's very, very easy to discover proofs in this system if you've been taught something like Barwise and Etchemendy's approach to first order logic. And it's consonant with anti-representationalist philosophy of logic that some bloggers here (and by "some" I mean at least one) and friends of the blog like. But cool even if you don't like that philosophy of logic. It's still cool.
m. y:A m. x: <>A
n. xRy n. | xRy for <> elimination
: o. | y: A for <> elimination
: | :
o. x: <>A m, n <> introduction | :
p. | z: B
q. z: B m, n/o-p <> elimination**
m. | xRy for []introduction m. x: []A
| : n. xRy
| : :
n. | y: A :
o. x: []A m-n [] introduction* o. y: A m,n [] elimination
[Note again that with <> introduction and [] elimination the y in question can be equal to the x, though in most proofs it will not. But, for example, showing that the system KD is included in KT requires having them be equal.]
*Restriction on [] introduction: y can only occur in lines m-n [Note that as a result y must be different from x.]
**Restriction on <> elimination: y can only occur in lines n/o-p! [Note that as a result y must be different from x and z. However z and x might be identical!]
These restrictions on the world variables in <> elimination and [] introduction are exactly analogous to restrictions on the use of arbitrary names in Fitch style natural deduction proofs for first order predicate logic. It is this fact that makes proving things in our version of K so easy for anyone competent with a properly presented Fitch style natural deduction system for first order predicate logic.
I'm not a logician, nor do I play one on T.V., so there might still be something subtly wrong with the above. But my students and I have test driven it with respect to lots of theorems and non-theorems of K, and in all the cases the car has stayed on the road.
Recent Comments