Ferreira, Gilda2020-03-022020-03-0220180168-0072http://hdl.handle.net/10400.2/9416We 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.engPredicative polymorphismIntuitionistic predicate calculusExistence propertyNatural deductionNormalizationFaithfulnessjournal article10.1016/j.apal.2018.08.004