Disjunction and existence properties
= Disjunction and existence properties
{wiki}
A theory has the disjunction property when provability of a closed disjunction implies provability of one disjunct. It has the existence property when a provable existential sentence has a witness whose substitution is provably valid. These are distinct constructive properties; <disjunction property of intuitionistic propositional logic> is one instance of the former.