BIBLIOS

Document type
Journal articles

Document subtype
Full paper

Title
A herbrandized functional interpretation of classical first-order logic

Participants in the publication
Fernando Ferreira (Author)
Dep. Matemática
CMAFcIO
Gilda Ferreira (Author)
LASIGE
CMAFcIO

Summary
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\\ntheorem on the extraction of terms from classically provable existential statements.


Where published
Archive for Mathematical Logic

Publication Identifiers
ISSN - 0933-5846

Publisher
Springer Nature



Document Identifiers
DOI - https://doi.org/10.1007/s00153-017-0555-6
URL - http://dx.doi.org/10.1007/s00153-017-0555-6

Rankings
SCIMAGO Q1 (2017) - 0.909 - Logic
SCIMAGO Q1 (2017) - 0.909 - Logic

Keywords
Functional interpretations First-order logic Star combinatory calculus Finite sets Tautologies Herbrand's theorem