19th Annual IEEE Symposium on Logic in Computer Science (LICS'04) On the Geometry of Interaction for Classical Logic Turku, Finland July 13-July 17 ISBN: 0-7695-2192-4
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. | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||