The Journal of Symbolic Logic

Research Article

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

Ronald Harrop

University of Durham, Newcastle Upon Tyne

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 N1 for which the result is immediate. The main step in the proof consisted in showing that the set of provable formulas of N1 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.

(Received July 30 1959)


1   The author wishes to thank the editor for many valuable suggestions regarding the presentation of this paper.