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)


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


000 Computer science, knowledge & systems
500 Science > 510 Mathematics






Florian Ranzi

Date Deposited:

16 Apr 2014 11:28

Last Modified:

16 Jan 2015 11:12

Publisher DOI:


Uncontrolled Keywords:

Proof nets, Identity of proofs, Classical logic, Cut elimination




Actions (login required)

Edit item Edit item
Provide Feedback