The disjunction property implies the numerical existence property
Harvey Friedman · Proceedings of the National Academy of Sciences · 1975
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.