{
  "id": "1203.4084",
  "version": "v1",
  "published": "2012-03-19T12:00:45.000Z",
  "updated": "2012-03-19T12:00:45.000Z",
  "title": "Canonical Proof nets for Classical Logic",
  "authors": [
    "Richard McKinley"
  ],
  "comment": "Accepted for publication in APAL (Special issue, Classical Logic and Computation)",
  "categories": [
    "math.LO",
    "cs.LO"
  ],
  "abstract": "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 [23], 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\\ast 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 [23]), we give a full proof of (c) for expansion nets with respect to LK\\ast, 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.",
  "revisions": [
    {
      "version": "v1",
      "updated": "2012-03-19T12:00:45.000Z"
    }
  ],
  "analyses": {
    "subjects": [
      "03F03"
    ],
    "keywords": [
      "classical logic",
      "canonical proof nets",
      "expansion nets",
      "classical sequent calculus proofs",
      "sequent proofs modulo rule permutations"
    ],
    "note": {
      "typesetting": "TeX",
      "pages": 0,
      "language": "en",
      "license": "arXiv",
      "status": "editable",
      "adsabs": "2012arXiv1203.4084M"
    }
  }
}