Ferreira, Gilda2018-02-092018-07-312017Ferreira, Gilda - Rasiowa–Harrop disjunction property. "Stud Logica" [Em linha]. ISSN 0039-3215 (Print) 1572-8730 (Online). Vol. 105, nº 3 (2017), p. 649-6640039-3215(Print)1572-8730(Online)http://hdl.handle.net/10400.2/7090We show that there is a purely proof-theoretic proof of the Rasiowa–Harrop disjunction property for the full intuitionistic propositional calculus (IPC), via natural deduction, in which commuting conversions are not needed. Such proof is based on a sound and faithful embedding of IPC into an atomic polymorphic system. This result strengthens a homologous result for the disjunction property of IPC (presented in a recent paper co-authored with Fernando Ferreira) and answers a question then posed by Pierluigi Minari.engMathematical logicRasiowa–Harrop disjunction propertyIntuitionistic propositional calculusPredicative polymorphismNatural deductionStrong normalizationjournal article10.1007/s11225-016-9704-x