Publication
The faithfulness of atomic polymorphism
| dc.contributor.author | Ferreira, Fernando | |
| dc.contributor.author | Ferreira, Gilda | |
| dc.date.accessioned | 2021-02-15T09:47:12Z | |
| dc.date.available | 2021-02-15T09:47:12Z | |
| dc.date.issued | 2014 | |
| dc.description.abstract | It is known that the full intuitionistic propositional calculus can be embedded into the atomic polymorphic system Fat, a calculus with only two connectives: the conditional and the second-order universal quantifier. The embedding uses a translation of formulas due to Prawitz and relies on the so-called property of instantiation overflow. In this paper, we show that the previous embedding is faithful i.e., if a translated formula is derivable in Fat, then the original formula is already derivable in the propositional calculus. | pt_PT |
| dc.description.version | info:eu-repo/semantics/publishedVersion | pt_PT |
| dc.identifier.issn | 1572-6126 | |
| dc.identifier.uri | http://hdl.handle.net/10400.2/10489 | |
| dc.language.iso | eng | pt_PT |
| dc.peerreviewed | yes | pt_PT |
| dc.publisher | Lodz University Press | pt_PT |
| dc.subject | Predicative polymorphism | pt_PT |
| dc.subject | Faithfulness | pt_PT |
| dc.subject | Natural deduction | pt_PT |
| dc.subject | Kripke models | pt_PT |
| dc.subject | Intuitionistic propositional calculus | pt_PT |
| dc.title | The faithfulness of atomic polymorphism | pt_PT |
| dc.type | journal article | |
| dspace.entity.type | Publication | |
| oaire.awardURI | info:eu-repo/grantAgreement/FCT/SFRH/SFRH%2FBPD%2F34527%2F2006/PT | |
| oaire.citation.title | Trends in Logic XIII | pt_PT |
| oaire.fundingStream | SFRH | |
| 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.name | Fundação para a Ciência e a Tecnologia | |
| 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 | 5bccfd46-dece-42cd-ae48-a5bac4911f4f | |
| relation.isProjectOfPublication.latestForDiscovery | 5bccfd46-dece-42cd-ae48-a5bac4911f4f |
Files
Original bundle
1 - 1 of 1