Canonical proof nets for classical logic

McKinley, Richard (2013). Canonical proof nets for classical logic. Annals of pure and applied logic, 164(6), pp. 702-732. Elsevier 10.1016/j.apal.2012.05.007

[img] Text
1-s2.0-S0168007212000838-main.pdf__tid=cc9c9004-c548-11e3-b89c-00000aab0f02&acdnat=1397640401_1907bfd57a8d0e358ed0b6e7723f4e65 - Published Version
Restricted to registered users only
Available under License Publisher holds Copyright.

Download (393kB) | Request a copy

Proof nets provide abstract counterparts to sequent proofs modulo rule permutations; the idea being that if two proofs have the same underlying proof-net, they are in essence the same proof. Providing a convincing proof-net counterpart to proofs in the classical sequent calculus is thus an important step in understanding classical sequent calculus proofs. By convincing, we mean that (a) there should be a canonical function from sequent proofs to proof nets, (b) it should be possible to check the correctness of a net in polynomial time, (c) every correct net should be obtainable from a sequent calculus proof, and (d) there should be a cut-elimination procedure which preserves correctness. Previous attempts to give proof-net-like objects for propositional classical logic have failed at least one of the above conditions. In Richard McKinley (2010) [22], the author presented a calculus of proof nets (expansion nets) satisfying (a) and (b); the paper defined a sequent calculus corresponding to expansion nets but gave no explicit demonstration of (c). That sequent calculus, called LK∗ in this paper, is a novel one-sided sequent calculus with both additively and multiplicatively formulated disjunction rules. In this paper (a self-contained extended version of Richard McKinley (2010) [22]), we give a full proof of (c) for expansion nets with respect to LK∗, and in addition give a cut-elimination procedure internal to expansion nets – this makes expansion nets the first notion of proof-net for classical logic satisfying all four criteria.

Item Type: Journal Article (Original Article)
Division/Institute: 08 Faculty of Science > Institute of Computer Science (INF) > Logic and Theory Group (LTG)
08 Faculty of Science > Institute of Computer Science (INF)
UniBE Contributor: Mc Kinley, Richard
Subjects: 000 Computer science, knowledge & systems
500 Science > 510 Mathematics
ISSN: 0168-0072
Publisher: Elsevier
Submitter: Florian Ranzi
Date Deposited: 16 Apr 2014 11:28
Last Modified: 16 Jan 2015 11:12
Publisher DOI: 10.1016/j.apal.2012.05.007
Uncontrolled Keywords: Proof nets, Identity of proofs, Classical logic, Cut elimination
BORIS DOI: 10.7892/boris.45208
URI: http://boris.unibe.ch/id/eprint/45208

Actions (login required)

Edit item Edit item
Provide Feedback