Proofnets for S5: sequents and circuits for modal logic

In C. Dimitracopoulos, L. Newelski & D. Normann (eds.), Logic Colloquium 2005. Cambridge: Cambridge University Press. pp. 151-172 (2007)
Download Edit this record How to cite View on PhilPapers
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.
PhilPapers/Archive ID
Upload history
Archival date: 2016-11-02
View other versions
Added to PP index

Total views
246 ( #22,786 of 58,403 )

Recent downloads (6 months)
25 ( #29,943 of 58,403 )

How can I increase my downloads?

Downloads since first upload
This graph includes both downloads from PhilArchive and clicks on external links on PhilPapers.