Utilize este identificador para referenciar este registo:
https://hdl.handle.net/1822/75419
Título: | The Russell-Prawitz embedding and the atomization of universal instantiation |
Autor(es): | Espírito Santo, José Ferreira, Gilda |
Palavras-chave: | Intuitionistic propositional calculus System F Predicative polymorphism Russell-Prawitz translation Proof reduction |
Data: | 2021 |
Editora: | Oxford University Press |
Revista: | Logic Journal of the IGPL |
Resumo(s): | Given 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: (i) they help achieving strict simulation of proof reduction by means of the Russell–Prawitz embedding of IPC into system F, (ii) they are not stronger than a certain ‘dinaturality’ conversion known to generate a consistent equality of proofs, (iii) they provide the bridge between the Russell–Prawitz embedding and another translation, due to the authors, of IPC directly into system Fat and (iv) they give means for explaining why the Russell–Prawitz translation achieves strict simulation whereas the translation into Fat does not. |
Tipo: | Artigo |
URI: | https://hdl.handle.net/1822/75419 |
DOI: | 10.1093/jigpal/jzaa025 |
ISSN: | 1367-0751 |
e-ISSN: | 1368-9894 |
Versão da editora: | https://academic.oup.com/jigpal/article-abstract/29/5/823/5877481 |
Arbitragem científica: | yes |
Acesso: | Acesso aberto |
Aparece nas coleções: | CMAT - Artigos em revistas com arbitragem / Papers in peer review journals |