| Article ID | Journal | Published Year | Pages | File Type |
|---|---|---|---|---|
| 11010144 | Annals of Pure and Applied Logic | 2018 | 14 Pages |
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.
Related Topics
Physical Sciences and Engineering
Mathematics
Logic
Authors
Gilda Ferreira,