Independence of premise

In proof theory and constructive mathematics, the principle of independence of premise states that if φ and ∃ x θ are sentences in a formal theory and φ → ∃ x θ is provable, then ∃ x (φ → θ) is provable. Here x cannot be a free variable of φ.

The principle is valid in classical logic. Its main application is in the study of intuitionistic logic, where the principle is not always valid.

In classical logic

The principle of independence of premise is valid in classical logic because of the law of the excluded middle. Assume that φ → ∃ x θ is provable. Then, if φ holds, there is an x satisfying φ → θ but if φ does not hold then any x satisfies φ → θ. In either case, there is some x such that φ→θ. Thus ∃ x (φ → θ) is provable.

In intuitionistic logic

The principle of independence of premise is not generally valid in intuitionistic logic (Avigad and Feferman 1999). This can be illustrated by the BHK interpretation, which says that in order to prove φ → ∃ x θ intuitionistically, one must create a function that takes a proof of φ and returns a proof of ∃ x θ. Here the proof itself is an input to the function and may be used to construct x. On the other hand, a proof of ∃ x (φ → θ) must first demonstrate a particular x, and then provide a function that converts a proof of φ into a proof of θ in which x has that particular value.

As a weak counterexample, suppose θ(x) is some decidable predicate of a natural number such that it is not known whether any x satisfies θ. For example, θ may say that x is a formal proof of some mathematical conjecture whose provability is not known. Let φ the formula ∃ z θ(z). Then φ → ∃ x θ is trivially provable. However, to prove ∃ x (φ → θ), one must demonstrate a particular value of x such that, if any value of x satisfies θ, then the one that was chosen satisfies θ. This cannot be done without already knowing whether ∃ x θ holds, and thus ∃ x (φ → θ) is not intuitionistically provable in this situation.

References

• Jeremy Avigad and Solomon Feferman (1999). Gödel's functional ("Dialectica") interpretation (PDF). in S. Buss ed., The Handbook of Proof Theory, North-Holland. pp. 337–405.