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. These include the disjunction property (DP), the existence property (EP), and three additional properties:

These properties can only be directly expressed for theories that have the ability to quantify over natural numbers and, for CR₁, quantify over functions from ${\displaystyle \mathbb {N} }$ to ${\displaystyle \mathbb {N} }$. In practice, one may say that a theory has one of these properties if a definitional extension of the theory has the property stated above (Rathjen 2005).

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).

Heyting arithmetic is well known for having the disjunction property and the (numerical) existence property.

While the earliest results were for constructive theories of arithmetic, many results are also known for constructive set theories (Rathjen 2005). John Myhill (1973) showed that IZF with the axiom of replacement eliminated in favor of the axiom of collection has the disjunction property, the numerical existence property, and the existence property. Michael Rathjen (2005) proved that CZF has the disjunction property and the numerical existence property.

Freyd and Scedrov (1990) observed that the disjunction property holds in free Heyting algebras and free topoi. In categorical terms, in the free topos, that corresponds to the fact that the terminal object, ${\displaystyle \mathbf {1} }$, is not the join of two proper subobjects. Together with the existence property it translates to the assertion that ${\displaystyle \mathbf {1} }$ is an indecomposable projective object—the functor it represents (the global-section functor) preserves epimorphisms and coproducts.

There are several relationship between the five properties discussed above.