Disjunction property

In mathematical logic, the disjunction and existence properties are the "hallmarks" of constructive theories such as Heyting arithmetic and constructive set theories (Rathjen 2005).

The disjunction property is satisfied by a theory if, whenever a sentence A ∨ B is a theorem, then either A is a theorem, or B is a theorem.

The existence property or witness property is satisfied by a theory if, whenever a sentence (∃x)A(x) is a theorem, where A(x) has no other free variables, then there is some term t such that the theory proves A(t).

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

...
Wikipedia