# I am looking for a soundness, completeness and consistency proof for this particular $S5$ calculus.

I know that it suffices to add the axioms

$(T)~\square\psi\rightarrow\psi$
$(K)~\square(\psi\rightarrow\varphi)\rightarrow(\square\psi\rightarrow\square\varphi)$
$(5)~\diamond\psi\rightarrow\square\diamond\psi$

together with the rule of necessitation

$(N)\vdash\psi\Rightarrow~\vdash\square\psi$

to a calculus for propositional logic, in order to get a sound, complete and consistent calculus for the modal logic S5 (regarding Kripke models with equivalence relations as accessibility relation).

But I cannot find any literature to back up my statement. (And my supervisor does not want me to waste space by proving it myself.) Does this extension have a name or something to search for? Or do you know where the above statement is proven? Of course, there are many proofs that show certain calculi to be complete, sound, and consistent in Kripke semantics, but what about this particular calculus?

• Have you checked Chellas' "Modal Logic: An introduction"? I think he uses this axiomatization for S5 but maybe the completeness is done a bit differently. – Apostolos May 5 '17 at 23:04
• This answer appears to be correct. Chellas introduces $S5$ on pages 14-21 with those axioms and the proof on soundness, completeness and consistency (even though he calls it "determination by standard models") can be found on pages 177 ff. – xamid May 10 '17 at 10:22