A herbrandized functional interpretation of classical first-order logic

Ferreira, Fernando; Ferreira, Gilda

http://hdl.handle.net/10400.2/7089

Utilize este identificador para referenciar este registo.

Nome:	Descrição:	Tamanho:	Formato:
SH interpretation.pdf		300.53 KB	Adobe PDF	Ver/Abrir

Contacte-nos

Autores

Ferreira, Fernando

Ferreira, Gilda

Resumo(s)

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.

Palavras-chave

Mathematical logic Functional interpretations First-order logic Star combinatory calculus Finite sets Tautologies Herbrand’s theorem

URI

http://hdl.handle.net/10400.2/7089

Citação

Ferreira, 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-539