“Proofnets for S5: sequents and circuits for modal logic,” pages 151–172 in Logic Colloquium 2005, C. Dimitracopoulos, L. Newelski, and D. Normann (eds.), number 28 in Lecture Notes in Logic. Cambridge University Press, 2007.
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.
I’m Greg Restall, and this is my personal website. I teach philosophy and logic as Professor of Philosophy at the University of Melbourne. ¶ Start at the home page of this site—a compendium of recent additions around here—and go from there to learn more about who I am and what I do. ¶ This is my personal site on the web. Nothing here is in any way endorsed by the University of Melbourne.