Articles by others on the same topic (1)

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.