classical well-foundedness

Recall that an object $X$ of a topos $\mathbf{E}$ is *inhabited* if the unique map $!: X \to 1$ is an epimorphism. Recall also one of the formulations of “well-foundedness” in set theory: given a binary relation $\prec_X \hookrightarrow X \times X$, we say that $\prec_X$ is *classically well-founded* if every subset $P$ of $X$ with an element possesses a $\prec_X$-minimal element. Formally, this is the assertion

$\forall (P: \Omega^X) \;\; \exists (x: X)\; P(x) \Rightarrow \exists (x_0: X) \; P(x_0) \wedge \neg \exists (y: X)\; P(y) \wedge (y \prec_X x_0)$

which can be interpreted in an arbitrary topos $\mathbf{E}$.

Suppose that in a topos $\mathbf{E}$, there is an object $X$ that carries an inhabited classically well-founded binary relation $\prec_X$. Then the law of excluded middle holds in $E$.

We must show that for any proposition $Q: 1 \to \Omega$, we have $Q \vee \neg Q = true: 1 \to \Omega$.

First observe that if $j: J \hookrightarrow X$ is any subobject, then the induced relation $\prec_J$ defined by the pullback

$\array{
\prec_J & \hookrightarrow & J \times J \\
\downarrow & & \downarrow _\mathrlap{j \times j} \\
\prec_X & \hookrightarrow & X \times X
}$

is also classically well-founded, as any inhabited subobject $R$ of $J$ may be regarded as an inhabited subobject $j R$ of $X$, and any $\prec_X$-minimal (generalized) element of $j R$ can be viewed as a $\prec_J$-minimal element of $R$.

The subobject $A$ of $X$ defined by the formula

$(x_1: X) \exists (y: X) y \prec_X x_1$

is inhabited since $\prec_X$ is. By classical well-foundedness, the object $I_0$ of $\prec_X$-minimal elements of $X$ is inhabited; notice this is precisely $\neg A$. As $A$ itself is inhabited, classical well-foundedness implies that the object $I_1$ consisting of $\prec_X$- (or $\prec_A$-)minimal elements of $A$ is also inhabited. Obviously $I_0$ and $I_1$ are disjoint subobjects of $X$, and so their coproduct is their union in $X$, a subobject $I = I_0 + I_1 \hookrightarrow X$. As we already observed, the induced relation $\prec_I$ on $I$ is classically well-founded.

Let $P: I \to \Omega$ be the predicate

$I_0 + I_1 \stackrel{! + !}{\to} 1 + 1 \stackrel{(Q, true)}{\to} \Omega.$

As $P$ is $true$ on $I_1$ and $I_1$ is an inhabited object, we see $\exists (x: I) P(x)$ is $true$. It follows from classical well-foundedness that

$true \;\; = \;\; \exists (x_0: I) P(x_0) \wedge \neg \exists (y: I) P(y) \wedge (y \prec_I x_0).$

But as $I = I_0 + I_1$, this proposition is equivalent to a join of two propositions

(1)$\exists (x_0: I_0)\; P(x_0) \wedge \neg \exists (y: I) P(y) \wedge (y \prec_I x_0)$

and

(2)$\exists (x_1: I_1)\; P(x_1) \wedge \neg \exists (y: I) P(y) \wedge (y \prec_I x_1).$

For the first (1), we have

$\exists (x_0: I_0)\; P(x_0) \wedge \neg \exists (y: I) P(y) \wedge (y \prec_I x_0) \;\; = \;\; Q$

as the left side reduces to $\exists (x_0: I_0) P(x_0)$ (since $\neg \exists (y: I) P(y) \wedge (y \prec_I x_0)$ is $true$ over the context $(x_0: I_0)$ of minimal elements), and $\exists (x_0: I_0) P(x_0) = Q$ since $P$ restricted to $I_0$ is $Q !: I_0 \to \Omega$.

For the second (2), this reduces to $\exists (x_1: I_1) \neg \exists (y: I) P(y) \wedge (y \prec_I x_1)$ because $P(x_1) = true$ over the context $(x_1: I_1)$ (i.e., $P$ restricted to $I_1$ is $true !: I_1 \to \Omega$). Furthermore, over the context $(x_1: I_1)$ we have $y \prec_I x_1 \vdash y \in I_0$, and so

$\array{
\exists (x_1: I_1)\; \neg \exists (y: I) P(y) \wedge (y \prec_I x_1) & \vdash & \exists (x_1: I_1)\; \neg \exists (y: I) P(y) \wedge y \in I_0 \\
& = & \exists (x_1: I_1)\; \neg Q \\
& = & \neg Q
}$

Thus

$true \;\; = \;\; \exists (x_0: I)\; P(x_0) \vee \neg \exists (y: I) P(y) \wedge (y \prec_I x_0) \;\; \vdash \;\; Q \vee \neg Q$

as was to be shown.

Revised on May 31, 2014 at 08:58:58
by
Todd Trimble