Publication
A herbrandized functional interpretation of classical first-order logic
dc.contributor.author | Ferreira, Fernando | |
dc.contributor.author | Ferreira, Gilda | |
dc.date.accessioned | 2018-02-09T10:12:00Z | |
dc.date.available | 2018-09-30T00:30:23Z | |
dc.date.issued | 2017 | |
dc.description.abstract | 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. | pt_PT |
dc.description.version | info:eu-repo/semantics/publishedVersion | pt_PT |
dc.identifier.citation | 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 | pt_PT |
dc.identifier.doi | 10.1007/s00153-017-0555-6 | pt_PT |
dc.identifier.issn | 0933-5846 (Print) | |
dc.identifier.issn | 1432-0665(Online) | |
dc.identifier.uri | http://hdl.handle.net/10400.2/7089 | |
dc.language.iso | eng | pt_PT |
dc.peerreviewed | yes | pt_PT |
dc.publisher | Springer | pt_PT |
dc.relation | Teoria da demonstração: abordagem lógico-computacional | |
dc.relation.publisherversion | https://link.springer.com/article/10.1007/s00153-017-0555-6 | pt_PT |
dc.subject | Mathematical logic | pt_PT |
dc.subject | Functional interpretations | pt_PT |
dc.subject | First-order logic | pt_PT |
dc.subject | Star combinatory calculus | pt_PT |
dc.subject | Finite sets | pt_PT |
dc.subject | Tautologies | pt_PT |
dc.subject | Herbrand’s theorem | pt_PT |
dc.title | A herbrandized functional interpretation of classical first-order logic | pt_PT |
dc.type | journal article | |
dspace.entity.type | Publication | |
oaire.awardTitle | Teoria da demonstração: abordagem lógico-computacional | |
oaire.awardURI | info:eu-repo/grantAgreement/FCT/5876/UID%2FMAT%2F04561%2F2013/PT | |
oaire.awardURI | info:eu-repo/grantAgreement/FCT/5876/UID%2FCEC%2F00408%2F2013/PT | |
oaire.awardURI | info:eu-repo/grantAgreement/FCT//SFRH%2FBPD%2F93278%2F2013/PT | |
oaire.citation.endPage | 539 | pt_PT |
oaire.citation.startPage | 523 | pt_PT |
oaire.citation.title | Archive for Mathematical Logic | pt_PT |
oaire.fundingStream | 5876 | |
oaire.fundingStream | 5876 | |
person.familyName | Ferreira | |
person.givenName | Gilda | |
person.identifier.ciencia-id | 0B1A-81E7-88B1 | |
person.identifier.orcid | 0000-0003-1447-9764 | |
person.identifier.rid | H-9953-2013 | |
person.identifier.scopus-author-id | 14037466100 | |
project.funder.identifier | http://doi.org/10.13039/501100001871 | |
project.funder.identifier | http://doi.org/10.13039/501100001871 | |
project.funder.identifier | http://doi.org/10.13039/501100001871 | |
project.funder.name | Fundação para a Ciência e a Tecnologia | |
project.funder.name | Fundação para a Ciência e a Tecnologia | |
project.funder.name | Fundação para a Ciência e a Tecnologia | |
rcaap.embargofct | Segundo a revista (Archive for Mathematical Logic) o post-print pode ser colocado em repositórios 12 meses após a data da publicação. | pt_PT |
rcaap.rights | openAccess | pt_PT |
rcaap.type | article | pt_PT |
relation.isAuthorOfPublication | fd3a6c7d-42b2-4434-834f-fb161900c938 | |
relation.isAuthorOfPublication.latestForDiscovery | fd3a6c7d-42b2-4434-834f-fb161900c938 | |
relation.isProjectOfPublication | 790cb869-ff08-40ad-8026-fa89e1020bc0 | |
relation.isProjectOfPublication | decf6855-f566-40f8-af12-50adc657f065 | |
relation.isProjectOfPublication | dab4f1a3-08b3-4ccc-8509-1aa421dd896c | |
relation.isProjectOfPublication.latestForDiscovery | dab4f1a3-08b3-4ccc-8509-1aa421dd896c |