How to prove the completeness of S5?

Question

I am reading New Introduction to Modal Logic by Hughes and Cresswell, and I don't quite understand the proof described on pages 105-108. I follow up to the point where they prove that for every of WFF a of S5 there exists a WFF a' such that a' is a modal conjunctive normal form and a<=>a' is a theorem of S5. But I can't keep up with the completeness proof of S5, or even their strategy of the proof.

In the first part of the proof they are considering the fact that every WFF that is valid on S5 is such that when it is in modal conjunctive form, all of its conjuncts must always evaluate as true on equivalence frames. If at least one of those conjuncts were false, the WFF couldn't have been S5-valid since the entire conjunction would be false in that model. The proof of that should be fairly simple. If we assume that not all conjuncts in the formula are always true, that means that at least one conjunct won't be in the form of p ∨ ¬p disjunction, but would rather look closer to p ∨ p, which means that when p is false, the entire conjunction could be made to fail, all of which is under equivalence frames, so that would make the formula not S5 valid.

Once they've proven that, they go off to prove that every WFF of the ordered modal conjunctive modal form which passes "the test" is a theorem of S5, which I can't quite follow.

Could you please post some more references I could read, or post an outline for a proof of completeness for S5?

Answer 1

Hughes and Cresswell's proof proceeds roughly as follows:

1. They show that any sentence of S5 is logically equivalent to a modal conjunctive normal form (MCNF) in which a sentence takes the form of a conjunction of a series of disjunctions, with each disjunction having a specific form.
2. They formulate a 'test', whereby a disjunction passes the test iff at least one of its disjuncts is PC-valid (i.e. a tautology of the propositional calculus), and a conjunction of disjunctions passes the test iff each of the disjunctions passes the test.
3. From there they proceed to prove that every valid S5 sentence passes the test. This is done contrapositively by showing that a sentence that fails to pass the test would be invalid.
4. They then show that any S5 sentence that passes the test is a theorem.

Steps 3 and 4 depend on the particular form that the disjunctions take. They consist of a disjunction of a non-modal term, a series of L (necessary) terms, and an M (possible) term. The proof proceeds by considering these individual terms in combination. Step 4 depends on the fact that any PC-valid sentence is a theorem of S5, and also, by the N axiom, its necessity is a theorem also.

If you are interested in other proofs of S5 completeness, this paper provides a review, starting with Kripke's own proofs from 1959 and 1963. "Kripke completeness revisited", by Sara Negri. In this paper, Bentzen uses a computer based theorem prover. "A Henkin-style completeness proof for the modal logic S5", by Bruno Bentzen.