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

277 Views Asked by At

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?