loading...
On the Geometry of Interaction for Classical Logic
Turku, Finland July 13-July 17
DOI Bookmark: http://doi.ieeecomputersociety.org/10.1109/LICS.2004.131961519th Annual IEEE Symposium on Logic i ...
 This Article 
 
PDF
HTML
 
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
Carsten F?hrmann, University of Bath, England, UK
David Pym, University of Bath, England, UK
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.
Citation:
Carsten F?hrmann, David Pym, "On the Geometry of Interaction for Classical Logic," lics, pp.211-220, 19th Annual IEEE Symposium on Logic in Computer Science (LICS'04), 2004
Usage of this product signifies your acceptance of the Terms of Use.