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 is provable, then 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 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 is provable.

In intuitionistic logic

The principle of independence of premise is not generally valid in intuitionistic logic. This can be illustrated by the BHK interpretation, which says that in order to prove intuitionistically, one must create a function that takes a proof of φ and returns a proof of. Here the proof itself is an input to the function and may be used to construct x. On the other hand, a proof of 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 θ 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. Then is trivially provable. However, to prove , 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 holds, and thus is not intuitionistically provable in this situation.