A simple propositional S5 tableau system Original Research Article

We give a sound and weakly complete propositional S5 tableau system of a particularly simple sort, having an easy completeness proof. It sheds light on why the satisfiability problem for S5 is less complex than that for most other propositional modal logics. We believe the system remains complete when appropriate quantifier rules are added. If so, it would allow us to get partway to an interpolation theorem for first-order S5, a theorem that is known to fail in general.