A metatheoretical property of a deductive system stating that whenever the system proves a disjunction A ∨ B (typically a closed formula) it proves A or it proves B individually; commonly required of constructive systems.

Principle

Constructive proofs of a disjunction must contain information selecting which disjunct holds: proving A ∨ B must effectively yield a proof of A or a proof of B rather than merely excluding their joint falsity.

Demonstration

In intuitionistic propositional logic or in certain constructive type theories, a derivation of A ∨ B arises from a proof term that is either an injection into the left or right disjoint sum, so the term itself witnesses which disjunct is provable and the system therefore proves that disjunct.

Misapplication

Assuming the disjunction property holds in classical systems or for arbitrary metatheoretic encodings; or interpreting a derivable meta-level disjunction (provable 'either A or B') as immediate provability of one disjunct without an internal constructive witness.

Consequence

When a system has the disjunction property one can extract definite algorithmic information from disjunctive proofs, improve program extraction, and ensure that proofs of alternatives are not merely non-constructive eliminations by contradiction.

Reversal

A system lacking the disjunction property can prove A ∨ B while proving neither A nor B, typically by resorting to non-constructive principles such as excluded middle or classical reasoning.

Boundary

Concerns provability in the object theory and often only for closed or arithmetical formulas; it does not assert that every meta-theoretic disjunction lifts to an internal witness in every formalization and can fail in extensions that add classical axioms.

Semantic Tension

Tension with the law of excluded middle: excluded middle allows proving A ∨ ¬A without supplying which side holds, directly opposing the constructive content required by the disjunction property.

Synthesis

The disjunction property captures the constructive demand that proofs of alternatives be informative: if the system proves A ∨ B then it must—within the system—prove one of the disjuncts, ensuring disjunctive proofs carry a concrete selection rather than mere non-contradiction.