Inproof theory andconstructive mathematics, the principle ofindependence of premise (IP) states that if φ and ∃x θ are sentences in a formal theory andφ → ∃x θ is provable, then∃x (φ → θ) is provable. Herex cannot be afree variable of φ, while θ can be a predicate depending on it.

The main application of the principle is in the study ofintuitionistic logic, where the principle is not generally valid. Its crucial equivalent special case is discussed below.The principle is valid inclassical logic.

As is common, thedomain of discourse is assumed to be inhabited. That is, part of the theory is at least some term. For the discussion we distinguish one such term asa. In the theory of the natural numbers, this role may be played by the number7. Below,φ andψ denote propositions not depending onx, whileθ is a predicate that can depend on in.

The following is easily established:

• Firstly, if φ is established to be true, then if one assumesφ → ∃x θ to be provable, there is anx satisfyingφ → θ.
• Secondly, if φ is established to be false, then, by theexplosion, any proposition of the formφ → ψ holds. Then,anyx formally satisfiesφ → θ (and indeed any predicate of this form.)

In the first scenario,somex bound in the premise is reused in the conclusion, and it is generally not the a prioria that validates it. In the second scenario, the valuea in particular validates the conclusion of the principle. So in both of these two cases,somex validates the conclusion.

Thirdly, now in contrast to the two points above, consider the case in which it is not known how to prove or reject φ. A core case is when φ is the formula∃z θ(z), in which case the antecedentφ → ∃x θ becomes trivial: "If θ is satisfiable then θ is satisfiable." For illustration purposes, let it be granted that θ is a decidable predicate in arithmetic, meaning for any given numberb the proposition θ(b) can easily be inspected for its truth value. More specifically, θ shall express thatx is the index of a formal proof of some mathematical conjecture whose provability is not known. Certainly here, one way to establish∃x (φ → θ) would be to provide a particular indexx for which it can be shown (then aided by the assumption thatsome valuez satisfies θ) thatit genuinely satisfies θ. However, explicating a suchx is not possible (not yet and possibly never), as suchx exactly encodes the proof of a conjecture not yet proven or rejected.

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

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

The issue can also be approached using theBHK 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 anx. A proof of∃x (φ → θ) must then demonstrate aparticularx, together with a function that converts a proof of φ into a proof of θ in whichx has that value. In the proof calculus - like in the weak counterexample - a suitablex 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 established that if¬η → ∃x θ has a proof inarithmetic, then∃x (¬η → θ) has a proof as well.

It is not known whether this also applies to familiarset theories.^[1]

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

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 thelaw 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 numberx, such that if an index of a proof of the Goldbach conjecture exists, then the numberx 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 validx 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 thatx=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 anx such that one can demonstrate (then aided by φ assumed valid and so also ∃y θ for somey) that θ holds for thatx. Classically, it suffices to draw the same conclusion of interest when starting from two hypotheticals about φ. In the latter framework,somex is asserted to exist either which way, and the logic does not demand for it to be explicated.

IP and the shorter∃x ((∃y θ) → θ) have analogs in propositional logic. In the intuitionistic calculus, the finite form

${\displaystyle (\eta \to (\alpha \vee \beta ))\to ((\eta \to \alpha )\vee (\eta \to \beta ))}$

may be understood as expressing that information in the premise${\displaystyle \eta }$ is not required to establishwhich proposition in a pair of conjuncts it implies. For${\displaystyle \eta =\alpha \vee \beta }$, this reduces to the shorter but indeed equivalent so called Dirk Gently’s principle${\displaystyle (\alpha \to \beta )\vee (\beta \to \alpha )}$. The schema implies the strictly weaker excluded middle for negated propositions (WLEM) through the intuitionistic form ofconsequentia mirabilis.

Kreisel–Putnam logic, obtained by adopting this schema for negated propositions, i.e. with${\displaystyle \eta =\mathrm{\neg }\delta }$, still has thedisjunction property. The corresponding rule is anadmissible rule.

• 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.

• Predicate logic

• Articles with short description
• Short description matches Wikidata