The disjunction property implies the numerical existence property.
Any recursively enumerable extension of intuitionistic arithmetic which obeys the disjunction property obeys the numerical existence property. Any recursively enumerable extension of intuitionistic arithmetic proves its own disjunction property if and only if it proves its own inconsistency.
Friedman
H
H
Department of Mathematics, State University of New York at Buffalo, 4246 Ridge Lea Road, Amherst, N.Y. 14226.