A carregar...
Publicação
Atomic polymorphism and the existence property
| Nome: | Descrição: | Tamanho: | Formato: | |
|---|---|---|---|---|
| 374.95 KB | Adobe PDF |
Autores
Orientador(es)
Resumo(s)
We present a purely proof-theoretic proof of the existence property for the full intuitionistic first-order predicate calculus, via natural deduction, in which commuting conversions are not needed. Such proof illustrates the potential of an atomic polymorphic system with only three generators of formulas – conditional and first and second-order universal quantifiers – as a tool for proof-theoretical studies.
Descrição
Palavras-chave
Predicative polymorphism Intuitionistic predicate calculus Existence property Natural deduction Normalization Faithfulness
Contexto Educativo
Citação
Editora
Elsevier