nLab double-negation shift

Double-negation shift

Double-negation shift


In logic, the principle of double-negation shift (DNS), also known as the Kuroda Principle, is the statement that for any predicate PP, the following holds:

(x,¬¬P(x))¬¬x,P(x). (\forall x, \neg\neg P(x)) \to \neg\neg\forall x, P(x).

Of course, this is a tautology in classical logic where double negation ¬¬\neg\neg is the identity, but in constructive mathematics this is not provable (although its converse? is).

It is provable even constructively, though, if the domain of quantification of the variable xx is finite. In general, the principle of double-negation shift can be considered a property of this domain, which holds automatically for finite sets, and might hold for some other sets but not for others. Sometimes by “double-negation shift” is meant specifically the version for the domain \mathbb{N} of natural numbers.

Equivalence to double-negated PEM

The principle of double-negation shift (over arbitrary domains) is equivalent to the double-negation of the universally-quantified principle of excluded middle:

¬¬Q:Ω,(Q¬Q).\neg\neg \forall Q:\Omega, (Q \vee \neg Q).

Since Q,¬¬(Q¬Q)\forall Q, \neg\neg(Q \vee \neg Q) is a constructive tautology, the above double-negated PEM follows from DNS with domain PropProp and P(Q)=(Q¬Q)P(Q) = (Q\vee\neg Q). Conversely, if double-negated PEM holds, then to prove any negated goal like ¬¬x,P(x)\neg\neg\forall x, P(x) we may assume full PEM, i.e. classical logic, in which case DNS holds.

Validity in toposes

The interpretation of the predicate (Q:Ω|Q¬Q)(Q : \Omega | Q\vee\neg Q) in an elementary topos \mathcal{E} is the subobject [t,f]:1+1=2Ω[t,f] : 1+1=2\to\Omega. Thus, ¬¬Q:Ω,Q¬Q\neg\neg \forall Q:\Omega, Q \vee \neg Q holds in \mathcal{E} precisely if there exists a subterminal U1U\to 1 such that ¬¬Uid 1\neg\neg U \cong\id_1 and

(*)(Ω×UΩ)(2Ω).(*) \qquad\quad (\Omega\times U\to\Omega)\subseteq(2\to\Omega).

If \mathcal{E} is the topos of sheaves on a locale XX, the subterminals correspond to the opens of the locale, and (*)(*) holds for an open UO(X)U\in O(X) precisely if UV¬VU\subseteq V\vee\neg V for all VO(X)V\in O(X) with VUV\subseteq U. This means precisely that UU is boolean as an open sublocale, so double negation shift holds in Sh(X){Sh}(X) precisely if XX has a dense boolean open sublocale. If XX is (the set of opens in) a T 0T_0-space, the booleanness condition is equivalent to discreteness, so double negation shift holds in the sheaf topos precisely if XX has a dense discrete open subspace. A non-trivial example satisfying T 2T_2 is the 1-point compactification of an infinite set, and the real line is a counterexample (since a dense discrete open would be non-empty, and each of its element would be an isolated point, contradicting connectedness of R\mathrm{R}).

In the case of a presheaf topos, say on a small category C\mathrm{C}, truth values are precisely sieves in C\mathrm{C}, i.e. sets of objects UU such that for every morphism f:ABf: A\to B, BUB\in U implies AUA\in U. In this situation, (*)(*) is equivalent to C/A1\mathrm{C}/A\simeq 1 for all AUA\in U. From this it can be deduced that double negation shift holds in presheaves over C\mathrm{C} if and only if for every ACA\in\mathrm{C} there exists an f:BAf:B\to A with C/B1\mathrm{C}/B\simeq 1.

DNS holds in every Kripke model with finite frame; see here.

Last revised on April 27, 2020 at 13:16:31. See the history of this page for a list of all contributions to it.