Abstract

In this paper I introduce a sequent system for the propositional modal logic S5. Derivations of valid sequents in the system are shown to correspond to proofs in a novel natural deduction system of circuit proofs (reminiscient of proofnets in linear logic, or multiple-conclusion calculi for classical logic). The sequent derivations and proofnets are both simple extensions of sequents and proofnets for classical propositional logic, in which the new machinery—to take account of the modal vocabulary—is directly motivated in terms of the simple, universal Kripke semantics for S5. The sequent system is cut-free and the circuit proofs are normalising.