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.

• Type: Conference
• Year: 2005
• Where: TLCA
• Authors: François Lamarche, Lutz Straßburger
• Keywords: Classical Proof Nets, Proof Nets, Sequentialization Theorem, Theoretical Computer Science, TLCA 2005