The faithfulness of Fat: a proof-theoretic proof

Registro completo de metadados
MetadadosDescriçãoIdioma
Autor(es): dc.creatorFerreira, Fernando-
Autor(es): dc.creatorFerreira, Gilda-
Data de aceite: dc.date.accessioned2022-02-15T14:07:54Z-
Data de disponibilização: dc.date.available2022-02-15T14:07:54Z-
Data de envio: dc.date.issued2021-02-14-
Data de envio: dc.date.issued2021-02-14-
Data de envio: dc.date.issued2015-
Fonte completa do material: dc.identifierhttp://hdl.handle.net/10400.2/10490-
Fonte: dc.identifier.urihttp://educapes.capes.gov.br/handle/10400.2/10490-
Descrição: dc.descriptionIt is known that there is a sound and faithful translation of the full intuitionistic propositional calculus into the atomic polymorphic system Fat, a predicative calculus with only two connectives: the conditional and the second-order universal quantifier. The faithfulness of the embedding was established quite recently via a model-theoretic argument based in Kripke structures. In this paper we present a purely proof-theoretic proof of faithfulness. As an application, we give a purely proof-theoretic proof of the disjunction property of the intuitionistic propositional logic in which commuting conversions are not needed.-
Descrição: dc.descriptioninfo:eu-repo/semantics/publishedVersion-
Idioma: dc.languageen-
Relação: dc.relationinfo:eu-repo/grantAgreement/FCT/5876/147209/PT-
Relação: dc.relationinfo:eu-repo/grantAgreement/FCT/SFRH/SFRH%2FBPD%2F93278%2F2013/PT-
Direitos: dc.rightsopenAccess-
Palavras-chave: dc.subjectPredicative polymorphism-
Palavras-chave: dc.subjectFaithfulness-
Palavras-chave: dc.subjectNatural deduction-
Palavras-chave: dc.subjectIntuitionistic proposicional calculus-
Palavras-chave: dc.subjectDisjunction property-
Palavras-chave: dc.subjectStrong normalization-
Título: dc.titleThe faithfulness of Fat: a proof-theoretic proof-
Tipo de arquivo: dc.typelivro digital-
Aparece nas coleções:Repositório Aberto - Universidade Aberta (Portugal)

Não existem arquivos associados a este item.