In mathematical logic, the disjunction and existence properties are the "hallmarks" of constructive theories such as Heyting arithmetic and constructive set theories (Rathjen 2005).
Rathjen (2005) lists five properties that a theory may possess.
Almost by definition, a theory that accepts excluded middle while having independent statements does not have the disjunction property.
So all classical theories expressing Robinson arithmetic do not have it.
Most classical theories, such as Peano arithmetic and ZFC in turn do not validate the existence property either, e.g. because they validate the least number principle existence claim.
But some classical theories, such as ZFC plus the axiom of constructibility, do have a weaker form of the existence property (Rathjen 2005).
In categorical terms, in the free topos, that corresponds to the fact that the terminal object,
The proof uses the fact that a disjunction can be rewritten as an existential formula quantifying over natural numbers: Therefore, if Thus, assuming the numerical existence property, there exists some
Harvey Friedman (1974) proved that in any recursively enumerable extension of intuitionistic arithmetic, the disjunction property implies the numerical existence property.
The bounded formula may then be written as a finite disjunction A(1)∨A(2)∨...∨A(n).
Kurt Gödel (1932) stated without proof that intuitionistic propositional logic (with no additional axioms) has the disjunction property; this result was proven and extended to intuitionistic predicate logic by Gerhard Gentzen (1934, 1935).