Concerning formulas of the types A→B ν C,A →(Ex)B(x) in intuitionistic formal systems

In a previous paper [1] it was proved, among other results, that a closed disjunction of intuitionistic elementary number theory N can be proved if and only if at least one of its disjunctands is provable and that a closed formula of the type (Ex)B(x) is provable in N if and only if B(n) is provable for some numeral n . The method of proof was to show that, as far as closed formulas are concerned, N is equivalent to a calculus N 1 for which the result is immediate. The main step in the proof consisted in showing that the set of provable formulas of N 1 is closed under modus ponens. This was done by obtaining a subset of the set which is closed under modus ponens and contains all members of the original set, with which it is therefore identical.