Todd Trimble 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}$ .

Proposition

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

Proof

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