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?