disjunction and existence properties

The disjunction and existence properties are characteristic properties of constructive logics.

disjunction property

Whenever is a theorem, either or is a theorem.

existence property

Whenever is a theorem, then there is some term such that is a theorem.