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 [9, 15], or multipleconclusion calculi for classical logic [22, 23, 24]).

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 (the proof of cut-elimination is a simple generalisation of the systematic cut-elimination proof in Belnap's Display Logic [5, 21, 26]) and the circuit proofs are normalising.