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
x. The following is easily established: •
Firstly, if φ is established to be true, then if one assumes 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 , in which case the antecedent 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 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 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 comprises a function that takes a proof of φ and returns a proof of . Here proofs themselves can act as input to functions and, when possible, may be used to construct an
x. A proof of 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 does not suffice for a generic proof of existence as granted by the principle.
Rules An implication is strengthened when the antecedent is weakened. Of interest here are premises in the form of a negated statement, φ := ¬η. It has been meta-theoretically established that if has a proof in
arithmetic, then 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 axiomatically, the principle is valid. For example, here 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 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 from intuitionistic logic 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 in intuitionistic logic. == References ==