Todd Trimble classical well-foundedness

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

(P:Ω X)(x:X)P(x)(x 0:X)P(x 0)¬(y:X)P(y)(y Xx 0)\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 E\mathbf{E}.


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


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

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

J J×J j×j X X×X\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 RR of JJ may be regarded as an inhabited subobject jRj R of XX, and any X\prec_X-minimal (generalized) element of jRj R can be viewed as a J\prec_J-minimal element of RR.

The subobject AA of XX defined by the formula

(x 1:X)(y:X)y Xx 1(x_1: X) \exists (y: X) y \prec_X x_1

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

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

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

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

true=(x 0:I)P(x 0)¬(y:I)P(y)(y Ix 0).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 1I = I_0 + I_1, this proposition is equivalent to a join of two propositions

(1)(x 0:I 0)P(x 0)¬(y:I)P(y)(y Ix 0) \exists (x_0: I_0)\; P(x_0) \wedge \neg \exists (y: I) P(y) \wedge (y \prec_I x_0)


(2)(x 1:I 1)P(x 1)¬(y:I)P(y)(y Ix 1). \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

(x 0:I 0)P(x 0)¬(y:I)P(y)(y Ix 0)=Q\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 (x 0:I 0)P(x 0)\exists (x_0: I_0) P(x_0) (since ¬(y:I)P(y)(y Ix 0)\neg \exists (y: I) P(y) \wedge (y \prec_I x_0) is truetrue over the context (x 0:I 0)(x_0: I_0) of minimal elements), and (x 0:I 0)P(x 0)=Q\exists (x_0: I_0) P(x_0) = Q since PP restricted to I 0I_0 is Q!:I 0ΩQ !: I_0 \to \Omega.

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

(x 1:I 1)¬(y:I)P(y)(y Ix 1) (x 1:I 1)¬(y:I)P(y)yI 0 = (x 1:I 1)¬Q = ¬Q\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 }


true=(x 0:I)P(x 0)¬(y:I)P(y)(y Ix 0)Q¬Qtrue \;\; = \;\; \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