Independence of premise
Encyclopedia
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.
, 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 θ(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 . 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.
Proof theory
Proof theory is a branch of mathematical logic that represents proofs as formal mathematical objects, facilitating their analysis by mathematical techniques. Proofs are typically presented as inductively-defined data structures such as plain lists, boxed lists, or trees, which are constructed...
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 (Avigad and Feferman 1999). This can illustrated the BHK interpretationBHK interpretation
In mathematical logic, the Brouwer–Heyting–Kolmogorov interpretation, or BHK interpretation, of intuitionistic logic was proposed by L. E. J. Brouwer, Arend Heyting and independently by Andrey Kolmogorov...
, 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 θ(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 . 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.