Ferreira, FernandoFerreira, Gilda2021-02-152021-02-1520150039-3215http://hdl.handle.net/10400.2/10490It is known that there is a sound and faithful translation of the full intuitionistic propositional calculus into the atomic polymorphic system Fat, a predicative calculus with only two connectives: the conditional and the second-order universal quantifier. The faithfulness of the embedding was established quite recently via a model-theoretic argument based in Kripke structures. In this paper we present a purely proof-theoretic proof of faithfulness. As an application, we give a purely proof-theoretic proof of the disjunction property of the intuitionistic propositional logic in which commuting conversions are not needed.engPredicative polymorphismFaithfulnessNatural deductionIntuitionistic proposicional calculusDisjunction propertyStrong normalizationjournal article10.1007/s11225-015-9620-5