The Russell-Prawitz embedding and the atomization of universal instantiation

Registro completo de metadados
MetadadosDescriçãoIdioma
Autor(es): dc.creatorEspírito Santo, José-
Autor(es): dc.creatorFerreira, Gilda-
Data de aceite: dc.date.accessioned2022-02-15T14:07:55Z-
Data de disponibilização: dc.date.available2022-02-15T14:07:55Z-
Data de envio: dc.date.issued2021-02-14-
Data de envio: dc.date.issued2022-01-31-
Data de envio: dc.date.issued2019-
Fonte completa do material: dc.identifierhttp://hdl.handle.net/10400.2/10493-
Fonte: dc.identifier.urihttp://educapes.capes.gov.br/handle/10400.2/10493-
Descrição: dc.descriptionGiven the recent interest in the fragment of system F where universal instantiation is restricted to atomic formulas, a fragment nowadays named system Fat, we study directly in system F new conversions whose purpose is to enforce that restriction. We show some benefits of these new atomization conversions: (1) They help achieving strict simulation of proof reduction by means of the Russell-Prawitz embedding of IPC into system F; (2) They are not stronger than a certain “dinaturality” conversion known to generate a consistent equality of proofs; (3) They provide the bridge between the Russell-Prawitz embedding and another translation, due to the authors, of IPC directly into system Fat; (4) They give means for explaining why the Russell-Prawitz translation achieves strict simulation whereas the translation into Fat does not.-
Descrição: dc.descriptioninfo:eu-repo/semantics/publishedVersion-
Idioma: dc.languageen-
Publicador: dc.publisherOxford Academic-
Relação: dc.relationUIDB/00013/2020-
Relação: dc.relationUIDP/00013/2020-
Relação: dc.relationUID/MAT/04561/2019-
Relação: dc.relationUID/CEC/00408/2019-
Direitos: dc.rightsopenAccess-
Palavras-chave: dc.subjectIntuitionistic propositional calculus-
Palavras-chave: dc.subjectSystem F-
Palavras-chave: dc.subjectPredicative polymorphism-
Palavras-chave: dc.subjectRussell-Prawitz translation-
Palavras-chave: dc.subjectProof reduction-
Título: dc.titleThe Russell-Prawitz embedding and the atomization of universal instantiation-
Tipo de arquivo: dc.typelivro digital-
Aparece nas coleções:Repositório Aberto - Universidade Aberta (Portugal)

Não existem arquivos associados a este item.