Proof nets for Herbrand's Theorem

TL;DR

This paper introduces a new calculus of proof nets for first-order classical logic based on Herbrand's theorem, demonstrating a weakly-normalizing cut-elimination process and discussing the inherent nonconfluence of classical logic.

Contribution

It presents a novel proof net calculus for classical logic derived from Herbrand's theorem, with a cut-elimination procedure and insights into nonconfluence.

Findings

Proof nets for classical logic can be formulated without weakening.

The cut-elimination process is weakly normalizing.

Classical logic exhibits inherent nonconfluence.

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.