Repository logo
 
Publication

A herbrandized functional interpretation of classical first-order logic

dc.contributor.authorFerreira, Fernando
dc.contributor.authorFerreira, Gilda
dc.date.accessioned2018-02-09T10:12:00Z
dc.date.available2018-09-30T00:30:23Z
dc.date.issued2017
dc.description.abstractWe 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.versioninfo:eu-repo/semantics/publishedVersionpt_PT
dc.identifier.citationFerreira, 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-539pt_PT
dc.identifier.doi10.1007/s00153-017-0555-6pt_PT
dc.identifier.issn0933-5846 (Print)
dc.identifier.issn1432-0665(Online)
dc.identifier.urihttp://hdl.handle.net/10400.2/7089
dc.language.isoengpt_PT
dc.peerreviewedyespt_PT
dc.publisherSpringerpt_PT
dc.relationTeoria da demonstração: abordagem lógico-computacional
dc.relation.publisherversionhttps://link.springer.com/article/10.1007/s00153-017-0555-6pt_PT
dc.subjectMathematical logicpt_PT
dc.subjectFunctional interpretationspt_PT
dc.subjectFirst-order logicpt_PT
dc.subjectStar combinatory calculuspt_PT
dc.subjectFinite setspt_PT
dc.subjectTautologiespt_PT
dc.subjectHerbrand’s theorempt_PT
dc.titleA herbrandized functional interpretation of classical first-order logicpt_PT
dc.typejournal article
dspace.entity.typePublication
oaire.awardTitleTeoria da demonstração: abordagem lógico-computacional
oaire.awardURIinfo:eu-repo/grantAgreement/FCT/5876/UID%2FMAT%2F04561%2F2013/PT
oaire.awardURIinfo:eu-repo/grantAgreement/FCT/5876/UID%2FCEC%2F00408%2F2013/PT
oaire.awardURIinfo:eu-repo/grantAgreement/FCT//SFRH%2FBPD%2F93278%2F2013/PT
oaire.citation.endPage539pt_PT
oaire.citation.startPage523pt_PT
oaire.citation.titleArchive for Mathematical Logicpt_PT
oaire.fundingStream5876
oaire.fundingStream5876
person.familyNameFerreira
person.givenNameGilda
person.identifier.ciencia-id0B1A-81E7-88B1
person.identifier.orcid0000-0003-1447-9764
person.identifier.ridH-9953-2013
person.identifier.scopus-author-id14037466100
project.funder.identifierhttp://doi.org/10.13039/501100001871
project.funder.identifierhttp://doi.org/10.13039/501100001871
project.funder.identifierhttp://doi.org/10.13039/501100001871
project.funder.nameFundação para a Ciência e a Tecnologia
project.funder.nameFundação para a Ciência e a Tecnologia
project.funder.nameFundação para a Ciência e a Tecnologia
rcaap.embargofctSegundo 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.rightsopenAccesspt_PT
rcaap.typearticlept_PT
relation.isAuthorOfPublicationfd3a6c7d-42b2-4434-834f-fb161900c938
relation.isAuthorOfPublication.latestForDiscoveryfd3a6c7d-42b2-4434-834f-fb161900c938
relation.isProjectOfPublication790cb869-ff08-40ad-8026-fa89e1020bc0
relation.isProjectOfPublicationdecf6855-f566-40f8-af12-50adc657f065
relation.isProjectOfPublicationdab4f1a3-08b3-4ccc-8509-1aa421dd896c
relation.isProjectOfPublication.latestForDiscoverydab4f1a3-08b3-4ccc-8509-1aa421dd896c

Files

Original bundle
Now showing 1 - 1 of 1
Loading...
Thumbnail Image
Name:
SH interpretation.pdf
Size:
300.53 KB
Format:
Adobe Portable Document Format
License bundle
Now showing 1 - 1 of 1
No Thumbnail Available
Name:
license.txt
Size:
2.13 KB
Format:
Item-specific license agreed upon to submission
Description: