A carregar...
Publicação
The faithfulness of Fat: a proof-theoretic proof
| Nome: | Descrição: | Tamanho: | Formato: | |
|---|---|---|---|---|
| 238.9 KB | Adobe PDF |
Autores
Orientador(es)
Resumo(s)
It is known that there is a sound and faithful translation of the full
intuitionistic propositional calculus into the atomic polymorphic system
Fat, a predicative calculus with only two connectives: the conditional and
the second-order universal quantifier. The faithfulness of the embedding
was established quite recently via a model-theoretic argument based in
Kripke structures. In this paper we present a purely proof-theoretic proof
of faithfulness. As an application, we give a purely proof-theoretic proof of
the disjunction property of the intuitionistic propositional logic in which
commuting conversions are not needed.
Descrição
Palavras-chave
Predicative polymorphism Faithfulness Natural deduction Intuitionistic proposicional calculus Disjunction property Strong normalization