Atomic polymorphism and the existence property

Ferreira, Gilda

http://hdl.handle.net/10400.2/9416

Use this identifier to reference this record.

Name:	Description:	Size:	Format:
existence property.pdf		374.95 KB	Adobe PDF	Download

Send Feedback

Authors

Ferreira, Gilda

Abstract(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.