Atomic polymorphism and the existence property

• Author(s): Ferreira, Gilda
• Date: 2018
• Persistent ID: http://hdl.handle.net/10400.2/9416
• Origin: Repositório Aberto da Universidade Aberta
• Subject(s): Predicative polymorphism; Intuitionistic predicate calculus; Existence property; Natural deduction; Normalization; Faithfulness
• Document Type: Journal article
• Language: English
• Contributor(s): Repositório Aberto

Description

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.