BIBLIOS

  Sistema de Gestão de Referências Bibliográficas de Ciências

Modo Visitante (Login)
Need help?


Voltar

Detalhes Referência

Tipo
Artigos em Revista

Tipo de Documento
Artigo Completo

Título
A herbrandized functional interpretation of classical first-order logic

Participantes na publicação
Fernando Ferreira (Author)
Dep. Matemática
CMAFcIO
Gilda Ferreira (Author)
LASIGE
CMAFcIO

Resumo
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.

Data de Publicação
2017-05-19

Suporte
Archive for Mathematical Logic

Identificadores da Publicação
ISSN - 0933-5846

Editora
Springer Nature

Volume
56
Fascículo
5-6

Número de Páginas
17
Página Inicial
523
Página Final
539

Identificadores do Documento
DOI - https://doi.org/10.1007/s00153-017-0555-6
URL - http://dx.doi.org/10.1007/s00153-017-0555-6

Identificadores de Qualidade
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


Exportar referência

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 }