[**Note**: I'm salvaging some of my old newapps posts worth keeping by moving them over here. I'll always note it when this is the case. With the logic ones, it's also a chance to put in proper notation. At some point I'm going to mess around with all things Barcania in this approach. Just clearly stating Kripke's restriction would be cool. I also think that the possibility elimination rule will have to be tightened up just a little bit, at least when you go to full first-order modal logic.]

One of the really fun things I've been doing this [actually 2011's] 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).

_{K}◻(A → B) → (◻A → ◻B)

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.

## Recent Comments