A Simple Propositional S5 Tableau System

We give a sound and 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 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.

• Type: Journal
• Year: 1999
• Where: APAL
• Authors: Melvin Fitting
• Keywords: APAL 1999, Easy Completeness Proof, Propositional Modal Logics, Propositional S5 Tableau