Atomic polymorphism and the existence property |
| |
| Institution: | 1. Departamento de Matemática, Faculdade de Ciências da Universidade de Lisboa, Campo Grande, Ed. C6, 1749-016, Lisboa, Portugal;2. Universidade Aberta, Rua Braamcamp, 90, 1250-052, Lisboa, Portugal |
| |
| Abstract: | 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. |
| |
| Keywords: | Predicative polymorphism Intuitionistic predicate calculus Existence property Natural deduction Normalization Faithfulness |
| 本文献已被 ScienceDirect 等数据库收录！ |
|
