Independence of premise

In proof theory and constructive mathematics, the principle of independence of premise (IP) 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 φ, while θ can be a predicate depending on it.

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

Discussion

As is common, the domain 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 as a. In the theory of the natural numbers, this role may be played by the number 7. Below, φ and ψ denote propositions not depending on x, 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 an x satisfying φ → θ.
• Secondly, if φ is established to be false, then, by the explosion, any proposition of the form φ → ψ holds. Then, any x formally satisfies φ → θ (and indeed any predicate of this form.)

In the first scenario, some x bound in the premise is reused in the conclusion, and it is generally not the a priori a that validates it. In the second scenario, the value a in particular validates the conclusion of the principle. So in both of these two cases, some x 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 number b the proposition θ(b) can easily be inspected for its truth value. More specifically, θ shall express that x 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 index x for which it can be shown (then aided by the assumption that some value z satisfies θ) that it genuinely satisfies θ. However, explicating a such x is not possible (not yet and possibly never), as such x exactly encodes the proof of a conjecture not yet proven or rejected.

In intuitionistic logic

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

Rules

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 in arithmetic, then ∃x (¬η → θ) has a proof as well.

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

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

In classical logic

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.

Propositional logic

Kreisel–Putnam logic

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

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

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

Kreisel–Putnam logic, obtained by adopting this schema for negated propositions, i.e. with $\eta =\neg \delta$, still has the disjunction property. The corresponding rule is an admissible rule.

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.