BIBLIOS

  Ciências References Management System

Visitor Mode (Login)
Need help?


Back

Publication details

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 - Centro de Matemática, Aplicações Fundamentais e Investigação Operacional
Gilda Ferreira (Author)
LASIGE - LASIGE
CMAFcIO - Centro de Matemática, Aplicações Fundamentais e Investigação Operacional

Scope
International

Refereeing
Yes

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.

Date of Publication
2017-05-19

Where published
Archive for Mathematical Logic

Publication Identifiers
ISSN - 0933-5846

Publisher
Springer Nature

Volume
56
Number
5-6

Number of pages
17
Starting page
523
Last page
539

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


Export

APA
Fernando Ferreira, Gilda Ferreira, (2017). A herbrandized functional interpretation of classical first-order logic. Archive for Mathematical Logic, 56, 523-539. ISSN 0933-5846. eISSN . http://dx.doi.org/10.1007/s00153-017-0555-6

IEEE
Fernando Ferreira, Gilda Ferreira, "A herbrandized functional interpretation of classical first-order logic" in Archive for Mathematical Logic, vol. 56, pp. 523-539, 2017. 10.1007/s00153-017-0555-6

BIBTEX
@article{36355, author = {Fernando Ferreira and Gilda Ferreira}, title = {A herbrandized functional interpretation of classical first-order logic}, journal = {Archive for Mathematical Logic}, year = 2017, pages = {523-539}, volume = 56 }