Proof nets for Herbrand's Theorem

2010/05/21 by McKinley, Richard
#03F05 #FOS: Computer and information sciences #FOS: Mathematics #Logic (math.LO) #Logic in Computer Science (cs.LO)

paper · doi:10.48550/arxiv.1005.3986

Abstract

This paper explores the connection between two central results in the proof theory of classical logic: Gentzen's cut-elimination for the sequent calculus and Herbrands "fundamental theorem". Starting from Miller's expansion-tree-proofs, a highly structured way presentation of Herbrand's theorem, we define a calculus of weakening-free proof nets for (prenex) first-order classical logic, and give a weakly-normalizing cut-elimination procedure. It is not possible to formulate the usual counterexamples to confluence of cut-elimination in this calculus, but it is nonetheless nonconfluent, lending credence to the view that classical logic is inherently nonconfluent.

Related

• A sequent calculus demonstration of Herbrand's theorem
• Canonical Proof nets for Classical Logic
• Expansion Trees with Cut
• Herbrand's Fundamental Theorem - an encyclopedia article
• Herbrand's Theorem: a short statement and a model-theoretic proof