Logic in Computer Science (LICS 2004)

Paper: On the Geometry of Interaction for Classical Logic (at LICS 2004)

Authors: Carsten Fuhrmann David Pym

Abstract

It is well-known that weakening and contraction cause naïve categorical models of the classical sequent calculus to collapse to Boolean lattices. We introduce sound and complete models that avoid this collapse by interpreting cut-reduction by a partial order between morphisms. We provide concrete examples of such models by applying the geometry-of-interaction construction to quantaloids with finite biproducts, and show how these models illuminate cut reduction in the presence of weakening and contraction. Our models make no commitment to any translation of classical logic into intuitionistic logic and distinguish non-deterministic choices of cut-elimination.

BibTeX

  @InProceedings{FuhrmannPym-OntheGeometryofInte,
    author = 	 {Carsten Fuhrmann and David Pym},
    title = 	 {On the Geometry of Interaction for Classical Logic},
    booktitle =  {Proceedings of the Nineteenth Annual IEEE Symp. on Logic in Computer Science, {LICS} 2004},
    year =	 2004,
    editor =	 {Harald Ganzinger},
    month =	 {July}, 
    pages =      {211--220},
    location =   {Turku, Finland}, 
    publisher =	 {IEEE Computer Society Press}
  }