 Gentzen [1935] established the disjunction property for closed formulas of intuitionistic predicate logic. From this it follows that if intuitionistic logic is consistent, then \(P \vee \neg P\) is not a theorem if \(P\) is an atomic formula. Kleene [1945, 1952] proved that intuitionistic first-order number theory also has the related (cf. Friedman [1975]) existence property: