A carregar...
Publicação
η-conversions of IPC implemented in atomic F
| Nome: | Descrição: | Tamanho: | Formato: | |
|---|---|---|---|---|
| 122.51 KB | Adobe PDF |
Autores
Orientador(es)
Resumo(s)
It is known that the β-conversions of the full intuitionistic propositional calculus (IPC) translate into βη-conversions of the atomic polymorphic calculus Fat. Since Fat enjoys the property of strong normalization for βη-conversions, an alternative proof of strong normalization for IPC considering β-conversions can be derived. In the present article, we improve the previous result by analysing the translation of the η-conversions of the latter calculus into a technical variant of the former system (the atomic polymorphic calculus Fat^∧_at). In fact, from the strong normalization of Fat^∧_at we can derive the strong normalization of the full intuitionistic propositional calculus considering all the standard (β and η) conversions.
Descrição
Palavras-chave
Mathematical logic Eta-conversions Predicative polymorphism Intuitionistic propositional calculus Strong normalization Natural deduction
Contexto Educativo
Citação
Gilda Ferreira - η-conversions of IPC implemented in atomic F. "Logic Journal of the IGPL" [Em linha]. ISSN 1367-0751 (Print) 1368-9894 (Online). Vol. 25, nº 2 (2017), p. 115–130
Editora
Oxford University Press