Naming Proofs in Classical Propositional Logic

10 years 9 months ago
Naming Proofs in Classical Propositional Logic
Abstract. We present a theory of proof denotations in classical propologic. The abstract definition is in terms of a semiring of weights, and two concrete instances are explored. With the Boolean semiring we get a theory of classical proof nets, with a geometric correctness criterion, a sequentialization theorem, and a strongly normalizing cut-elimination procedure. This gives us a “Boolean” category, which is not a poset. With the semiring of natural numbers, we obtain a sound semantics for classical logic, in which fewer proofs are identified. Though a “real” sequentialization theorem is missing, these proof nets have a grip on complexity issues. In both cases the cut elimination procedure is closely related to its equivalent in the calculus of structures.
François Lamarche, Lutz Straßburger
Added 28 Jun 2010
Updated 28 Jun 2010
Type Conference
Year 2005
Where TLCA
Authors François Lamarche, Lutz Straßburger
Comments (0)