Abstract

We show how to interpret intuitionistic propositional logic into a predicative second-order intuitionistic propositional system having only the conditional and the universal second-order quantifier. We comment on this fact. We argue that it supports the legitimacy of using classical logic in a predicative setting, even though the philosophical cast of predicativism is nonrealistic. We also note that the absence of disjunction and existential quantifications allows one to have a process of normalization of proofs that avoids the use of "commuting conversions.".