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.

gollark: <@293066066605768714> Please grant me access to the newly created private subforum.

gollark: > As well as actually working, maybe

gollark: Yes, this is planned.

gollark: As well as actually working, maybe, and not allowing historical data to accumulate forever, it could monitor APIONET for functionality, and, using proven osmarksDNS™ technologies, offer a domain which returns a random IP selected from all operational APIONET servers.

gollark: I have a useful* idea: onstat™++™. The current status.osmarks.net is down. However, via "oracle cloud" I can get a free bad VPS (1/4 of a core allocated and 1GB of RAM, or something) which should be sufficient to run a shinier version.

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.

This article is issued from Wikipedia. The text is licensed under Creative Commons - Attribution - Sharealike. Additional terms may apply for the media files.