On Natural Deduction in Classical First-Order Logic: Curry-Howard Correspondence, Strong Normalization and Herbrand's Theorem

Federico Aschieri (1) , Margherita Zorzi (2)

1 LIP - Laboratoire de l'Informatique du Parallélisme
2 UNIVR | DI - Department of Computer Science [Verona]

We present a new Curry-Howard correspondence for classical first-order natural deduction. We add to the lambda calculus an operator which represents, from the viewpoint of programming, a mechanism for raising and catching multiple exceptions, and from the viewpoint of logic, the excluded middle over arbitrary prenex formulas. The machinery will allow to extend the idea of learning -- originally developed in Arithmetic -- to pure logic. We prove that our typed calculus is strongly normalizing and show that proof terms for simply existential statements reduce to a list of individual terms forming a Herbrand disjunction. A by-product of our approach is a natural-deduction proof and a computational interpretation of Herbrand's Theorem.

Domaines: Logique [math.LO]; Logique en informatique [cs.LO]

Federico Aschieri, Margherita Zorzi. On Natural Deduction in Classical First-Order Logic: Curry-Howard Correspondence, Strong Normalization and Herbrand's Theorem. Theoretical Computer Science, 2016. ⟨hal-00931128v7⟩