Ferreira, FernandoFerreira, Gilda2018-02-092018-09-302017Ferreira, 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-5390933-5846 (Print)1432-0665(Online)http://hdl.handle.net/10400.2/7089We 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.engMathematical logicFunctional interpretationsFirst-order logicStar combinatory calculusFinite setsTautologiesHerbrand’s theoremjournal article10.1007/s00153-017-0555-6