In THIS POST I presented a Fitch style proper natural deduction system for the modal logic K, basically (with minimal deviations involving negation) using Alex Simpson's earlier presentation in a Prawitz style tree system. I presented proofs of the characteristic K axiom as well as the interdefinability of possibility and necessity in classical K. Here I will show that adding inferences that force the accessibility relation to behave in the predicted ways allows you to prove the characteristic inferences for T, S4, and S5.
In the earlier post I should have been clearer about what I meant by a "proper" natural deduction system, since this is what is at issue. A number of textbooks present deductive systems for modal logic that involve more inference rules than modus ponens and substitution and call these "natural deduction" systems. But as far as I am aware, they are all improper. A proper natural deduction system: (1) proceeds by giving an introduction and elimination rule for each operator, that are (2) provably harmonious (2a: the ability to prove uniqueness in the system of an operator shows that the elimination rule is strong enough, given the introduction rule (a relative form of completeness), 2b: the existence of a normal form proof for the system shows that the elimination rule is not too strong given the introduction rule (a proof theoretic relative form of soundness), and such that (3) the system is conservative over at least atomic formula (this is Restall's weak conservativity, to be contrasted with Tennant's strong conservativity, which requires the rules for each operator to be conservative with respect to the fragment of logic with those rules removed). Conservativity is a proof theoretic system-wide soundness requirement. There is no agreement in the literature on what a system-wide completeness requirement would be. I posted an interesting post on this a while ago, using some ideas of Neil Tennant's. A consequence of my idea is that proof theorists motivated by constructivism (and who thus accept a meta-theoretic disjunction property) must accept that undecidability entails incompleteness, and that as a result first-order logic is actually incomplete. I'll do another post on this soon since I was not clear enough about two intuitionistically inequivalent formulations of completeness (the weaker being intuitionistically provable for some semantics, the stronger provably false for first order logic for anyone committed to the disjunction property). Also see this cool post on using Tennant's ideas to come up with a non-monotonic proof theory for modal countermodels.
Anyhow, here are the proofs (again, go HERE for the presentation of K, which the following systems extend). Brief discussion afterwards about how we depart from Simpson.
1. | x: []A for --> Intro
2. | xRx reflexivity
3. | x: A 1,2 []Elim: 1, 2
4. x: []A --> A 1-3 -->Intro
Proof of characteristic S4 axiom, using transitivity of the accessibility relation
1. | x: []A for --> Intro
2. | | xRy for []Intro
3. | | | yRz for []Intro
4. | | | xRz 2,3 transitivity
5. | | | z: A 1,4 []Elim
6. | | y: []A 3-5 []Intro
7. | x: [][]A 2-6 []Intro
8. x:[]A-->[][]A 1-7 -->Intro
Proof of characteristic S5 axiom, using symmetry and transitivity of the accessibility relation
1. | x: <>A for -->Intro
2. | | xRy for []Intro
3. | | | z: A for <>Elim
4. | | | xRz for <>Elim
5. | | | yRx 2 symmetry
6. | | | yRz 5,4 transitivity
7. | | | y: <>A 3, 6 <>Intro
8. | | y: <>A 3/4-6<>Elim
9. | x: []<>A 2-8 []Intro
10. x: <>A-->[]<>A 1-9 -->Intro
Notes: (1) Differences from Simpson: (1a) Simpson's rules involve subproofs that show that if something is provable with the relevant assumption about accessibility then it is provable without it. This involves discharging the assumption and recopying the result. This kind of thing is necessary in a Fitch presentation of existential elimination for predicate logic (and hence <> Elim. in our K), to be able to state the restrictions on eigen-variables, but I can't see why it's necessary here. With Fitch style proofs, the proofs are shorter and easier to discover if we just allow the relevant statements of accessibility to be inferences that follow from no assumptions. I don't know if this makes normalization proofs more difficult, but I don't think it leads to unsoundness. Consider that completely arbitrary worlds in T will be accessible from themselves, so there is no analogous worry about eigenvariables. (1b) Simpson uses Euclideanness for S5 rather than reflexivity, symmettry, and transitivity. I think it's prettier to build up the systems this way. (2) Note that reflexivity is very similar to the standard identity introduction rule of first order predicate logic. And that the standard elimination rule of first order predicate logic allows you to prove transitivity and symmetry. So one could almost certainly get S5 by adding an analog to the identity elimination rule to reflexivity. I've played with this a bit and it seems to work. (3) Thanks again to my independent study students: Graham Bounds, Michael Morrissey, Joel Musser, and Caitlin O Malley.
Recent Comments