A herbrandized functional interpretation of classical first-order logic

Ferreira, Fernando; Ferreira, Gilda

http://hdl.handle.net/10400.2/7089

Use this identifier to reference this record.

Name:	Description:	Size:	Format:
SH interpretation.pdf		300.53 KB	Adobe PDF	Download

Send Feedback

Authors

Ferreira, Fernando

Ferreira, Gilda

Abstract(s)

We introduce a new typed combinatory calculus with a type constructor that, to each type σ, associates the star type σ^∗ of the nonempty finite subsets of elements of type σ. We prove that this calculus enjoys the properties of strong normalization and confluence. With the aid of this star combinatory calculus, we define a functional interpretation of first-order predicate logic and prove a corresponding soundness theorem. It is seen that each theorem of classical first-order logic is connected with certain formulas which are tautological in character. As a corollary, we reprove Herbrand’s theorem on the extraction of terms from classically provable existential statements.

Keywords

Mathematical logic Functional interpretations First-order logic Star combinatory calculus Finite sets Tautologies Herbrand’s theorem

URI

http://hdl.handle.net/10400.2/7089

Citation

Ferreira, Fernando; Ferreira, Gilda - A herbrandized functional interpretation of classical first-order logic. "Archive for Mathematical Logic" [Em linha]. ISSN 0933-5846 (Print) 1432-0665 (Online). Vol. 56, nº 5-6 (2017), p. 523-539