A carregar...
Publicação
Rasiowa–Harrop disjunction property
| Nome: | Descrição: | Tamanho: | Formato: | |
|---|---|---|---|---|
| 343.85 KB | Adobe PDF |
Autores
Orientador(es)
Resumo(s)
We show that there is a purely proof-theoretic proof of the Rasiowa–Harrop disjunction property for the full intuitionistic propositional calculus (IPC), via natural deduction, in which commuting conversions are not needed. Such proof is based on a sound and faithful embedding of IPC into an atomic polymorphic system. This result strengthens a homologous result for the disjunction property of IPC (presented in a recent paper co-authored with Fernando Ferreira) and answers a question then posed by Pierluigi Minari.
Descrição
Palavras-chave
Mathematical logic Rasiowa–Harrop disjunction property Intuitionistic propositional calculus Predicative polymorphism Natural deduction Strong normalization
Contexto Educativo
Citação
Ferreira, Gilda - Rasiowa–Harrop disjunction property. "Stud Logica" [Em linha]. ISSN 0039-3215 (Print) 1572-8730 (Online). Vol. 105, nº 3 (2017), p. 649-664
Editora
Springer