In mathematical logic, the disjunction property is satisfied by a logic if whenever

is a theorem, then either φ is a theorem, or ψ is a theorem.

The existence property is satisfied by a logic if whenever

is a theorem, then there is some term t for which φ(t) is a theorem.

The disjunction and existence properties are validated by intuitionistic logic and invalid for classical logic; they are key criteria used in assessing whether a logic is constructive. In particular the existence property is fundamental to understanding in what sense proofs can be considered to have content: the essence of the discussion of existence theorems. The disjunction property is a finitary analogue, in an evident sense. Namely given two or finitely many propositions φ_i, whose disjunction is true, we want to have an explicit value of the index i such that we have a proof of that particular φ_i. There are quite concrete examples in number theory where this has a major effect.