Independence of premise

The arithmetical example above provides what is called a weak counterexample. The existence claim ∃x (φ → θ) cannot be provable by intuitionistic means: Being able to inspect an x validating φ → θ would resolve the conjecture.

For example, consider the following classical argument: Either the Goldbach conjecture has a proof or it does not. If it does not have a proof, then to assume is has a proof is absurd and anything follows - in particular, it follows that it has a proof. Hence, there is some natural number index x such that if one assumes the Goldbach conjecture has a proof, that x is an index of such a proof.

The issue can also be approached using the BHK interpretation for intuitionistic proofs, which should be compared against the classical proof calculus. BHK says that a proof of φ → ∃x θ comprises a function that takes a proof of φ and returns a proof of ∃x θ. Here proofs themselves can act as input to functions and, when possible, may be used to construct an x. A proof of ∃x (φ → θ) must then demonstrate a particular x, together with a function that converts a proof of φ into a proof of θ in which x has that value. In the proof calculus - like in the weak counterexample - a suitable x can only be given using more input tied to amenable φ.

Indeed, using violating models, it has been established that the premise φ → ∃x θ does not suffice for a generic proof of existence as granted by the principle.

An implication is strengthened when the antecedent can be weakened. Of interest here are premises in the form of a negated statements, φ := ¬η.

It has been meta-theoretically that if ¬η → ∃x θ has a proof in arithmetic, then ∃x (¬η → θ) has a proof as well.

It is not known whether this also applies to familiar set theories.[1]

For existential-quantifier-free φ, theories over intuitionistic logic tend to be well behaved in regard to rules of this nature.

The Intuitionistic propositional calculus still has the disjunction property when the following related principle is adopted as an axiom:

${\displaystyle {\big (}\neg \eta \to (\alpha \lor \beta ){\big )}\to {\big (}(\neg \eta \to \alpha )\lor (\neg \eta \to \beta ){\big )}}$

The corresponding rule is an admissible rule.

As noted, the independence of premise principle for fixed φ and any θ follows both from a proof of φ as well as from a rejection of it. Hence, assuming the law of the excluded middle disjunction axiomatically, the principle is valid.

For example, here ∃x ((∃y θ) → θ) always holds. More concretely, consider the proposition:

"There exists a natural number x, such that if an index of a proof of the Goldbach conjecture exists, then the number x is the index of a proof of the Goldbach conjecture."

This is classically provable, as follows: Either an index for a proof of the Goldbach conjecture exists, or no such index exists. On the one hand, if one does exist, then whatever that index is also functions as a valid x in the above proposition. On the other hand, if no such index exists, then for such an index to also exist is contradictory, and then by explosion anything follows - and in particular it follows that x=7 is an index of a proof of the Goldbach conjecture. In both cases, some index exists that validates the proposition.

Constructively, one needs to provide an x such that one can demonstrate (then aided by φ assumed valid and so also ∃y θ for some y) that θ holds for that x. Classically, it suffices to draw the same conclusion of interest when starting from two hypotheticals about φ. In the latter framework, some x is asserted to exist either which way, and the logic does not demand for it to be explicated.