A herbrandized functional interpretation of classical first-order logic

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.