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

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 |