Tipo
Artigos em Revista
Tipo de Documento
Artigo Completo
Título
A Refined Interpretation of Intuitionistic Logic by Means of Atomic Polymorphism
Participantes na publicação
José Espírito Santo (Author)
Gilda Ferreira (Author)
LASIGE
CMAFcIO
Resumo
We study an alternative embedding of IPC into atomic system F whose translation of proofs is based, not on instantiation overflow, but instead on the admissibility of the elimination rules for disjunction and absurdity (where these connectives are defined according to the Russell–Prawitz translation). As compared to the embedding based on instantiation overflow, the alternative embedding works equally well at the levels of provability and preservation of proof identity, but it produces shorter derivations and shorter simulations of reduction sequences. Lambda-terms are employed in the technical development so that the algorithmic content is made explicit, both for the alternative and the original embeddings. The investigation of preservation of proof-reduction steps by the alternative embedding enables the analysis of generation of “administrative” redexes. These are the key, on the one hand, to understand the difference between the two embeddings; on the other hand, to understand whether the final word on the embedding of IPC into atomic system F has been said.
Data de Publicação
2019-03-27
Suporte
Studia Logica
Identificadores da Publicação
ISSN - 0039-3215,1572-8730
Editora
Springer Science and Business Media LLC
Identificadores do Documento
DOI -
https://doi.org/10.1007/s11225-019-09858-1
URL -
http://dx.doi.org/10.1007/s11225-019-09858-1
Identificadores de Qualidade
SCIMAGO Q1 (2018) - 0.47 - History and Philosophy of Sciences / Logic