On natural deduction in classical first order logic: Curry Howard correspondence, strong normalization and Herbrand's theorem
Abstract 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 an Herbrand disjunction. A by product of our approach is a natural deduction proof and a computational interpretation of Herbrand's Theorem.
Theor. Comput. Sci.