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.
|Titolo:||On natural deduction in classical first-order logic: Curry-Howard correspondence, strong normalization and Herbrand's theorem|
|Data di pubblicazione:||2016|
|Appare nelle tipologie:||01.01 Articolo in Rivista|