Trimble on ETCS II (changes) in nLab

Showing changes from revision #14 to #15: Added | Removed | Changed

This is Part II of an exposition by Todd Trimble on ETCS.

See also

• Part I, ZFC and ETCS

• Part III, ETCS: Building joins and coproducts

---

ETCS : Internalizing the logic

This post is a continuation of the discussion of “the elementary theory of the category of sets” [ETCS] which we had begun last time, here and in the comments which followed. My thanks go to all who commented, for some useful feedback and thought-provoking questions.

Today I’ll describe some of the set-theoretic operations and “internal logic” of ETCS. I have a feeling that some people are going to love this, and some are going to hate it. My main worry is that it will leave some readers bewildered or exasperated, thinking that category theory has an amazing ability to make easy things difficult.

• An aside: has anyone out there seen the book Mathematics Made Difficult? It’s probably out of print by now, but I recommend checking it out if you ever run into it — it’s a kind of extended in-joke which pokes fun at category theory and abstract methods generally. Some category theorists I know take a dim view of this book; I for my part found certain passages hilarious, in some cases making me laugh out loud for five minutes straight. There are category-theory-based books and articles out there which cry out for parody!

In an attempt to nip my concerns in the bud, let me remind my readers that there are major differences between the way that standard set theories like ZFC treat membership and the way ETCS treats membership, and that differences at such a fundamental level are bound to propagate throughout the theoretical development, and impart a somewhat different character or feel between the theories. The differences may be summarized as follows:

• Membership in ZFC is a global relation between objects of the same type (sets).

• Membership in ETCS is a local relation between objects of different types (“generalized” elements or functions, and sets).

Part of what we meant by “local” is that an element per se is always considered relative to a particular set to which it belongs; strictly speaking, as per the discussion last time, the same element is never considered as belonging to two different sets. That is, in ETCS, an (ordinary) element of a set AA is defined to be a morphism x:1→Ax : 1 \to A; since the codomain is fixed, the same morphism cannot be an element 1→B1 \to B of a different set BB. This implies in particular that in ETCS, there is no meaningful global intersection operation on sets, which in ZFC is defined by:

A∩B={x:(x∈A)∧(x∈B)}A \cap B = \{ x : (x \in A) \:\wedge\: (x \in B) \}

Instead, in ETCS, what we have is a local intersection operation on subsets A↪X,B↪XA \hookrightarrow X, B \hookrightarrow X of a set. But even the word “subset” requires care, because of how we are now treating membership. So let’s back up, and lay out some simple but fundamental definitions of terms as we are now using them.

Given two monomorphisms i:A→X,j:B→Xi : A \to X, j : B \to X, we write i⊆ji \subseteq j (A⊆BA \subseteq B if the monos are understood, or A⊆ XBA \subseteq_X B if we wish to emphasize this is local to XX) if there is a morphism k:A→Bk : A \to B such that i=jki = j k. Since jj is monic, there can be at most one such morphism kk; since ii is monic, such kk must be monic as well. We say i,ji, j define the same subset if this kk is an isomorphism. So: subsets of XX are defined to be isomorphism classes of monomorphisms into XX. As a simple exercise, one may show that monos i,ji, j into XX define the same subset if and only if i⊆ji \subseteq j and j⊆ij \subseteq i. The (reflexive, transitive) relation ⊆ X\subseteq_X on monomorphisms thus induces a reflexive, transitive, antisymmetric relation, i.e., a partial order on subsets of XX.

Taking some notational liberties, we write A⊆XA \subseteq X to indicate a subset of XX (as isomorphism class of monos). If x:U→Xx : U \to X is a generalized element, let us say xx is in a subset A⊆XA \subseteq X if it factors (evidently uniquely) through any representative mono i:A→Xi : A \to X, i.e., if there exists x′:U→Ax' : U \to A such that x=ix′x = i x'. Now the intersection of two subsets A⊆XA \subseteq X and B⊆XB \subseteq X is defined to be the subset A∩B⊆XA \cap B \subseteq X defined by the pullback of any two representative monos i:A→X,j:B→Xi : A \to X, j : B \to X. Following the “Yoneda principle”, it may equivalently be defined up to isomorphism by specifying its generalized elements:

A∩B≔ i{x∈X:(xis inA)∧(xis inB)}.A \:\cap\: B {\coloneqq}_i \{ x \in X : (x \:\text{is in}\: A) \:\wedge\: (x \:\text{is in}\: B) \}.

Thus, intersection works essentially the same way as in ZFC, only it’s local to subsets of a given set.

While we’re at it, let’s reformulate the power set axiom in this language: it says simply that for each set BB there is a set P(B)P(B) and a subset ∈ B⊆B×P(B)\in_B \subseteq B \times P(B), such that for any relation R⊆B×AR \subseteq B \times A, there is a unique “classifying map” χ R:A→P(B)\chi_R : A \to P(B) whereby, under 1 B×χ R:B×A→B×P(B)1_B \times \chi_R : B \times A \to B \times P(B), we have

R=(1 B×χ R) −1(∈ B).R = (1_B \times \chi_R)^{-1} (\in_B).

The equality is an equality between subsets, and the inverse image on the right is defined by a pullback. In categorical set theory notation,

R={⟨b,a⟩∈B×A:b∈ Bχ R(a)}.R = \{ \langle b, a \rangle \in B \times A : b \in_B \chi_R(a) \}.

Hence, there are natural bijections

R⊆B×AA→P(B)R⊆B×AB→P(A)\displaystyle \frac{R \subseteq B \times A}{A \to P(B)} \qquad \frac{R \subseteq B \times A}{B \to P(A)}

between subsets and classifying maps. The subset corresponding to ϕ:A→P(B)\phi : A \to P(B) is denoted [ϕ]⊆B×A\left[\phi\right] \subseteq B \times A or [ϕ]⊆A×B\left[\phi\right] \subseteq A \times B, and is called the extension of ϕ\phi.

The set P(1)P(1) plays a particularly important role; it is called the “subset classifier” because subsets A⊆XA \subseteq X are in natural bijection with functions χ:X→P(1)\chi : X \to P(1). [Cf. classifying spaces in the theory of fiber bundles.]

In ordinary set theory, the role of P(1)P(1) is played by the 2-element set {f,t}\{ f, t \}. Here subsets A⊆XA \subseteq X are classified by their characteristic functions χ A:X→{f,t}\chi_A : X \to \{ f, t \}, defined by χ A(x)≔t\chi_A(x) \coloneqq t iff x∈Ax \in A. We thus have A=χ A −1(t)A = \chi_A^{-1}(t); the elementhood relation ∈ 1↪1×P(1)\in_1 \hookrightarrow 1 \times P(1) boils down to t:1→P(1)t : 1 \to P(1). Something similar happens in ETCS set theory:

Lemma 1. The domain of elementhood ∈ 1→1×P(1)≅P(1)\in_1 \to 1 \times P(1) \cong P(1) is terminal.

Proof. A map X→∈ 1X \to \in_1, that is, a map χ:X→P(1)\chi : X \to P(1) which is in ∈ 1⊆P(1)\in_1 \subseteq P(1), corresponds exactly to a subset χ −1(∈ 1)⊆X\chi^{-1}(\in_1) \subseteq X which contains all of XX (_i.e._, the subobject 1 X:X⊆X1_X : X \subseteq X). Since the only such subset is 1 X1_X, there is exactly one map X→∈ 1X \to \in_1. □\Box

Hence elementhood ∈ 1⊆1×P(1)\in_1 \subseteq 1 \times P(1) is given by an element t:1→P(1)t : 1 \to P(1). The power set axiom says that a subset A⊆XA \subseteq X is retrieved from its classifying map χ A:X→P(1)\chi_A : X \to P(1) as the pullback χ A −1(t)⊆X\chi^{-1}_A (t) \subseteq X.

Part of the power of, well, power sets is in a certain dialectic between external operations on subsets and internal operations on P(1)P(1); one can do some rather amazing things with this. The intuitive (and pre-axiomatic) point is that if CC has finite products, equalizers, and power objects, then P(1)P(1) is a representing object for the functor

Sub:C op→SetSub : C^{op} \to Set

which maps an object XX to the collection of subobjects of XX, and which maps a morphism (“function”) f:X→Yf : X \to Y to the “inverse image” function f −1:Sub(Y)→Sub(X)f^{-1} : Sub(Y) \to Sub(X), that sends a subset j:B⊆Yj : B \subseteq Y to the subset f −1(B)⊆Xf^{-1}(B) \subseteq X given by the pullback of the arrows f:X→Yf : X \to Y, j:B⊆Y j : B \subseteq Y. By the Yoneda lemma, this representability means that external natural operations on the Sub(X)Sub(X) correspond to internal operations on the object P(1)P(1). As we will see, one can play off the external and internal points of view against each other to build up a considerable amount of logical structure, enough for just about any mathematical purpose.

• Remark. A category satisfying just the first three axioms of ETCS, namely existence of finite products, equalizers, and power objects, is called an (elementary) topos. Most or perhaps all of this post will use just those axioms, so we are really doing some elementary topos theory. As I was just saying, we can build up a tremendous amount of logic internally within a topos, but there’s a catch: this logic will be in general intuitionistic. One gets classical logic (including law of the excluded middle) if one assumes strong extensionality [where we get the definition of a well-pointed topos]. Topos theory has a somewhat fearsome reputation, unfortunately; I’m hoping these notes will help alleviate some of the sting.

To continue this train of thought: by the Yoneda lemma, the representing isomorphism

θ:hom(−,P(1))→∼Sub(−)\displaystyle \theta : \hom(-, P(1)) \stackrel{\sim}{\to} Sub(-)

is determined by a universal element θ P(1)(1 P(1))\theta_{P(1)}(1_{P(1)}), i.e., a subset of P(1)P(1), namely the mono t:1→P(1)t : 1 \to P(1). In that sense, t:1→P(1)t : 1 \to P(1) plays the role of a universal subset. The Yoneda lemma implies that external natural operations on general posets Sub(X)Sub(X) are completely determined by how they work on the universal subset.

Internal Meets

To illustrate these ideas, let us consider intersection. Externally, the intersection operation is a natural transformation

∩ X:Sub(X)×Sub(X)→Sub(X).\cap_X : Sub(X) \times Sub(X) \to Sub(X).

This corresponds to a natural transformation

hom(X,P(1))×hom(X,P(1))→hom(X,P(1))\hom(X, P(1)) \times \hom(X, P(1)) \to \hom(X, P(1))

which (by Yoneda) is given by a function ∧:P(1)×P(1)→P(1)\wedge : P(1) \times P(1) \to P(1). Working through the details, this function is obtained by putting X=P(1)×P(1)X = P(1) \times P(1) and chasing

⟨π 1,π 2⟩∈hom(P(1)×P(1),P(1))×hom(P(1)×P(1),P(1))\langle \pi_1, \pi_2 \rangle \in \hom(P(1) \times P(1), P(1)) \times \hom(P(1) \times P(1), P(1))

through the composite

hom(X,P(1))×hom(X,P(1))→∼Sub(X)×Sub(X)→∩Sub(X)→∼hom(X,P(1)).\hom(X, P(1)) \times \hom(X, P(1)) \stackrel{\sim}{\to} Sub(X) \times Sub(X) \stackrel{\cap}{\to} Sub(X) \stackrel{\sim}{\to} \hom(X, P(1)).

Let’s analyze this bit by bit. The subset [π 1]=π 1 −1(t)⊆P(1)×P(1)\left[\pi_1\right] = \pi_{1}^{-1}(t) \subseteq P(1) \times P(1) is given by

t×id:1×P(1)→P(1)×P(1),t \times id : 1 \times P(1) \to P(1) \times P(1),

and the subset [π 2]=π 2 −1(t)⊆P(1)×P(1)\left[\pi_2\right] = \pi_{2}^{-1}(t) \subseteq P(1) \times P(1) is given by

id×t:P(1)×1→P(1)×P(1).id \times t : P(1) \times 1 \to P(1) \times P(1).

Hence [π 1]∩[π 2]⊆P(1)×P(1)\left[\pi_1\right] \cap \left[\pi_2\right] \subseteq P(1) \times P(1) is given by the pullback of the functions t×idt \times id and id×tid \times t, which is just

t×t:1×1→P(1)×P(1).t \times t : 1 \times 1 \to P(1) \times P(1).

The map ∧:P(1)×P(1)→P(1)\wedge : P(1) \times P(1) \to P(1) is thus defined to be the classifying map of t×t:1×1⊆P(1)×P(1)t \times t : 1 \times 1 \subseteq P(1) \times P(1).

To go from the internal meet ∧:P(1)×P(1)→P(1)\wedge : P(1) \times P(1) \to P(1) back to the external intersection operation, let A⊆X,B⊆XA \subseteq X, B \subseteq X be two subsets, with classifying maps χ A,χ B:X→P(1)\chi_A, \chi_B : X \to P(1). By the definition of ∧\wedge, we have that for all generalized elements x∈Xx \in X

χ A(x)∧χ B(x)=tif and only if⟨χ A(x),χ B(x)⟩=⟨t,t⟩\chi_A(x) \:\wedge\: \chi_B(x) = t \;\text{if and only if}\; \langle \chi_A(x), \chi_B(x) \rangle = \langle t, t \rangle

(where the equality signs are interpreted with the help of equalizers). This holds true iff xx is in the subset A⊆XA \subseteq X and is in the subset B⊆XB \subseteq X, i.e., if and only if xx is in the subset A∩B⊆XA \cap B \subseteq X. Thus χ A∧χ B\chi_A \wedge \chi_B is indeed the classifying map of A∩B⊆XA \cap B \subseteq X. In other words, χ A∩B=χ A∧χ B\chi_{A \cap B} = \chi_A \wedge \chi_B.

A by-product of the interplay between the internal and external is that the internal intersection operator

∧:P(1)×P(1)→P(1)\wedge : P(1) \times P(1) \to P(1)

is the meet operator of an internal meet-semilattice structure on P(1)P(1): it is commutative, associative, and idempotent (because that is true of external intersection). The identity element for ∧\wedge is the element t:1→P(1)t : 1 \to P(1). In particular, P(1)P(1) carries an internal poset structure: given generalized elements u,v:A→P(1)u, v : A \to P(1), we may define

u≤vif and only ifu=u∧vu \leq v \;\text{if and only if}\; u = u \wedge v

and this defines a reflexive, symmetric, antisymmetric relation [≤]⊆P(1)×P(1)\left[\leq\right] \subseteq P(1) \times P(1):

[≤]≔ i{⟨u,v⟩∈P(1)×P(1):u=u∧v},\left[\leq\right] {\coloneqq}_i \{ \langle u, v \rangle \in P(1) \times P(1) : u = u \wedge v\},

equivalently described as the equalizer

[≤]→P(1)×P(1)→→P(1)\left[\leq\right] \to P(1) \times P(1) \stackrel{\to}{\to} P(1)

of the maps π 1:P(1)×P(1)→P(1)\pi_1 : P(1) \times P(1) \to P(1) and ∧:P(1)×P(1)→P(1)\wedge : P(1) \times P(1) \to P(1). We have that u≤vu \leq v if and only if [u]⊆[v]\left[u\right] \subseteq \left[v\right].

Internal Implication

Here we begin to see some of the amazing power of the interplay between internal and external logical operations. We will prove that P(1)P(1) carries an internal Heyting algebra structure (ignoring joins for the time being).

Let’s recall the notion of Heyting algebra in ordinary naive set-theoretic terms: it’s a lattice PP that has a material implication operator “⇒\Rightarrow” such that, for all x,y,z∈Px, y, z \in P,

x∧y≤zif and only ifx≤y⇒z.x \wedge y \leq z \;\text{if and only if}\; x \leq y \Rightarrow z.

Now: by the universal property of P(1)P(1), a putative implication operation ⇒:P(1)×P(1)→P(1)\Rightarrow : P(1) \times P(1) \to P(1) is uniquely determined as the classifying map of its inverse image (⇒) −1(t)⊆P(1)×P(1)(\Rightarrow)^{-1}(t) \subseteq P(1) \times P(1), whose collection of generalized elements is

{⟨u,v⟩∈P(1)×P(1):(u⇒v)=t}\{ \langle u, v \rangle \in P(1) \times P(1) : (u \Rightarrow v) = t\}

Given ⟨u,v⟩:A→P(1)×P(1)\langle u, v \rangle : A \to P(1) \times P(1), the equality here is equivalent to

t≤u⇒vt \leq u \Rightarrow v

(because t:1→P(1)t : 1 \to P(1) is maximal), which in turn is equivalent to

t∧u=u≤vt \wedge u = u \leq v

This means we should define ⇒:P(1)×P(1)→P(1)\Rightarrow : P(1) \times P(1) \to P(1) to be the classifying map of the subset

[≤]⊆P(1)×P(1).\left[\leq\right] \subseteq P(1) \times P(1).

Theorem 1. P(1)P(1) admits internal implication.

Proof. We must check that for any three generalized elements u,v,w:A→P(1)u, v, w : A \to P(1), we have

w≤u⇒vif and only ifw∧u≤v.w \leq u \Rightarrow v \;\text{if and only if}\; w \wedge u \leq v.

Passing to the external picture, let [u],[v],[w]\left[u\right], \left[v\right], \left[w\right] be the corresponding subsets of AA. Now: according to how we defined ⇒,\Rightarrow, a generalized element e∈Ae \in A is in [u⇒v]\left[u \Rightarrow v\right] if and only if u(e)≤v(e)u(e) \leq v(e). This applies in particular to any monomorphism e:[w]→Ae: \left[w\right] \to A that represents the subset [w]⊆A \left[w\right] \subseteq A.

Lemma 2. The composite

u(e)=([w]→eA→uP(1))\displaystyle u(e) = (\left[w\right] \stackrel{e}{\to} A \stackrel{u}{\to} P(1))

is the classifying map of the subset [w]∩[u]⊆[w]\left[w\right] \cap \left[u\right] \subseteq \left[w\right].

Proof. As subsets of [w]\left[w\right],

(ue) −1(t)=e −1u −1(t)=e −1([u])=[w]∩[u](u e)^{-1}(t) = e^{-1} u^{-1}(t) = e^{-1}(\left[u\right]) = \left[w\right] \cap \left[u\right]

where the last equation holds because both sides are the subsets defined as the pullback of two representative monos e:[w]→Ae : \left[w\right] \to A, i:[u]→Ai : \left[u\right] \to A. □\Box

Continuing the proof of Theorem 1, we see by Lemma 2 that the condition u(e)≤v(e)u(e) \leq v(e) corresponds externally to the condition

[w]∩[u]⊆[w]∩[v]\left[w\right] \cap \left[u\right] \subseteq \left[w\right] \cap \left[v\right]

and this condition is equivalent to [w]∩[u]⊆[v]\left[w\right] \cap \left[u\right] \subseteq \left[v\right].

Passing back to the internal picture, this is equivalent to w∧u≤vw \wedge u \leq v, and the proof of Theorem 1 is complete. □\Box

Cartesian Closed Structure

Next we address a comment made by “James”, that a category satisfying the ETCS axioms is cartesian closed. As everything else in this article, this uses only the fact that such a category is a topos: has finite products, equalizers, and “power sets”.

Proposition 1. If A,BA, B are “sets”, then P(A×B)P(A \times B) represents an exponential P(B) A.P(B)^A.

Proof. By the power set axiom, there is a bijection between maps into the power set and relations:

ϕ:X→P(A×B)R⊆X×(A×B)\displaystyle \frac{\phi : X \to P(A \times B)}{R \subseteq X \times (A \times B)}

which is natural in XX. By the same token, there is a natural bijection

R⊆(X×A)×Bϕ′:X×A→P(B).\displaystyle \frac{R \subseteq (X \times A) \times B}{\phi' : X \times A \to P(B)}.

Putting these together, we have a natural isomorphism hom(−,P(A×B))≅hom(−×A,P(B))\hom(-, P(A \times B)) \cong \hom(- \times A, P(B))

and this representability means precisely that P(A×B)P(A \times B) plays the role of an exponential P(B) AP(B)^A. □\Box

Corollary 1. P(A)≅P(1) AP(A) \cong P(1)^A. □\Box

The universal element of this representation is an evaluation map A×P(A)→P(1)A \times P(A) \to P(1), which is just the classifying map of the subset ∈ A⊆A×P(A)\in_A \subseteq A \times P(A).

Thus, P(B) A≅P(A×B)P(B)^A \cong P(A \times B) represents the set of all functions ϕ:A→P(B)\phi : A \to P(B) (that is, relations from AA to B B). This is all we need to continue the discussion of internal logic in this post, but let’s also sketch how we get full cartesian closure. [Warning: for those who are not comfortable with categorical reasoning, this sketch could be rough going in places.]

As per our discussion, we want to internalize the set of such relations which are graphs of functions, i.e., maps ϕ\phi where each ϕ(a)⊆B\phi(a) \subseteq B is a singleton, in other words which factor as

A→B→σP(B)\displaystyle A \to B \stackrel{\sigma}{\to} P(B)

where σ:B→P(B)\sigma : B \to P(B) is the singleton mapping:

b↦{b}={c∈B:b=c}.b \mapsto \{ b \} = \{ c \in B: b = c \}.

We see from this set-theoretic description that σ:B→P(B)\sigma : B \to P(B) classifies the equality relation

{⟨b,c⟩∈B×B:b=c}⊆B×B\{ \langle b, c \rangle \in B \times B: b = c \} \subseteq B \times B

which we can think of as either the equalizer of the pair of maps π 1,π 2:B×B→B\pi_1, \pi_2 : B \times B \to B or, what is the same, the diagonal map δ B=⟨1 B,1 B⟩:B→B×B\delta_B = \langle 1_B, 1_B \rangle : B \to B \times B.

Thus, we put σ=χ δ:B→P(B)\sigma = \chi_{\delta} : B \to P(B), and it is not too hard to show that the singleton mapping σ\sigma is a monomorphism. As usual, we get this monomorphism as the pullback χ σ −1(t)\chi_{\sigma}^{-1}(t) of t:1→P(1)t : 1 \to P(1) along its classifying map χ σ:P(B)→P(1)\chi_{\sigma} : P(B) \to P(1).

Now: a right adjoint such as (−) A (-)^A preserves all limits, and in particular pullbacks, so we ought then to have a pullback

B A ⟶ 1 A σ A↓ ↓t A P(B) A ⟶χ σ A P(1) A \begin{matrix} B^{\mathrlap{A}} & \longrightarrow & 1^{\mathrlap{A}} \\ \mathllap{\scriptsize{\sigma^A}}\downarrow & & \downarrow\mathrlap{\scriptsize{t^\A}} \\ P(B)^{\mathrlap{A}} & \underset{\chi_\sigma^A}{\longrightarrow} & P(1)^{\mathrlap{A}} \end{matrix}

Of course, we don’t even have B AB^A yet, but this should give us an idea: define σ A\sigma^A, and in particular its domain B AB^A, by taking the pullback of the right-hand map along the bottom map. In case there is doubt, the map on the bottom is defined Yoneda-wise, applying the isomorphism

hom(P(B) A×A,P(1))≅hom(P(B) A,P(1) A)\hom(P(B)^A \times A, P(1)) \cong \hom(P(B)^A, P(1)^A)

to the element in the hom-set (on the left) given by the composite

P(B) A×A→evP(B)→χ σP(1).\displaystyle P(B)^A \times A \stackrel{ev}{\to} P(B) \stackrel{\chi_\sigma}{\to} P(1).

The map on the right of the pullback is defined similarly. That this recipe really gives a construction of B AB^A will be left as an exercise for the reader.

Universal Quantification

As further evidence of the power of the internal-external dialectic, we show how to internalize universal quantification.

As we are dealing here now with predicate logic, let’s begin by defining some terms as to be used in ETCS and topos theory:

• An ordinary predicate of type AA is a function ϕ:A→P(1)\phi : A \to P(1). Alternatively, it is an ordinary element ϕ′:1→P(1) A≅P(A)\phi' : 1 \to P(1)^A \cong P(A). It corresponds (naturally and bijectively) to a subset [ϕ]:S⊆A\left[\phi\right]: S \subseteq A.

• A generalized predicate of type AA is a function ϕ′:X→P(A)≅P(1) A\phi' : X \to P(A) \cong P(1)^A. It may be identified with (corresponds naturally and bijectively to) a function ϕ:X×A→P(1)\phi : X \times A \to P(1), or to a subset [ϕ]:S⊆X×A\left[\phi\right] : S \subseteq X \times A.

We are trying to define an operator ∀ A\forall_A which will take a predicate of the form ϕ:X×A→P(1)\phi : X \times A \to P(1) [conventionally written ] to a predicate ∀ Aϕ:X→P(1)\forall_A \phi : X \to P(1) [conventionally written ]. Externally, this corresponds to a natural operation which takes subsets of X×AX \times A to subsets of XX. Internally, it corresponds to an operation of the form:

∀ A:P(A)≅P(1) A→P(1).\forall_A : P(A) \cong P(1)^A \to P(1).

This function is determined by the subset (∀ A) −1(t)⊆P(1) A(\forall_A)^{-1}(t) \subseteq P(1)^A, defined elementwise by

{ϕ∈P(1) A:∀ Aϕ=t}.\{ \phi \in P(1)^A : \forall_A \phi = t\}.

Now, in ordinary logic, ∀ a∈Aϕ(a)\forall_{a \in A} \phi(a) is true if and only if ϕ(a)\phi(a) is true for all a∈Aa \in A, or, in slightly different words, if ϕ:A→P(1)\phi : A \to P(1) is constantly true over all of AA:

ϕ=(A→!1→tP(1)).\displaystyle \phi = (A \stackrel{!}{\to} 1 \stackrel{t}{\to} P(1)).

The expression on the right (global truth over AA) corresponds to a function t A:1→P(1) At_A : 1 \to P(1)^A, indeed a monomorphism since any function with domain 11 is monic. Thus we are led to define the desired quantification operator ∀ A:P(1) A→P(1)\forall_A : P(1)^A \to P(1) as the classifying map of t A:1⊆P(1) At_A : 1 \subseteq P(1)^A.

Let’s check how this works externally. Let ϕ:X→P(1) A\phi : X \to P(1)^A be a generalized predicate of type AA. Then according to how ∀ A\forall_A has just been defined, ∀ Aϕ:X→P(1)\forall_A \phi : X \to P(1) classifies the subset

{x∈X:ϕ(x,−)=t A:A→P(1))}⊆X\displaystyle \{ x \in X: \phi(x, -) = t_A : A \to P(1)) \} \subseteq X

There is an interesting adjoint relationship between universal quantification and substitution (aka “pulling back”). By “substitution”, we mean that given any predicate ψ:X→P(1)\psi : X \to P(1) on XX, we can always pull back to a predicate on X×AX \times A (substituting in a dummy variable aa of type AA, forming e.g. ψ(x)∧[a=a]\psi(x) \wedge \left[a=a\right]) by composing with the projection π:X×A→X\pi : X \times A \to X. In terms of subsets, substitution along AA is the natural external operation

([ψ]⊆X)↦([ψ]×A⊆X×A).(\left[\psi\right] \subseteq X) \mapsto (\left[\psi\right]\times A \subseteq X \times A).

Then, for any predicate ϕ:X×A→P(1)\phi : X \times A \to P(1), we have the adjoint relationship

[ψ]×A⊆ϕif and only if[ψ]⊆∀ Aϕ\left[\psi\right] \times A \subseteq \phi \;\text{if and only if}\; \left[\psi\right] \subseteq \forall_A \phi

so that substitution along AA is left adjoint to universal quantification along AA. This is easy to check; I’ll leave that to the reader.

Internal Intersection Operators

Now we put all of the above together, to define an internal intersection operator

⋂:PPX→PX\bigcap : PPX \to PX

which intuitively takes an element 1→PPX1 \to PPX (a family FF of subsets of XX) to its intersection 1→PX1 \to PX, as a subset ⋂F⊆X\bigcap F \subseteq X.

Let’s first write out a logical formula which expresses intersection:

x∈⋂Fif and only if∀ S∈PX(S∈F)⇒(x∈S).x \in \bigcap F \;\text{if and only if}\; \forall_{S \in PX} (S \in F) \Rightarrow (x \in S).

Jon AwbreyWe have all the ingredients to deal with the logical formula on the right: we have an implication operator “: There seemed to be an orphan right bracket in the above line, also on your blog.⇒\Rightarrow” as part of the internal Heyting algebra structure on P(1)P(1), and we have the quantification operator “∀ PX\forall_{PX}”. The atomic expressions (S∈F)(S \in F) and (x∈S)(x \in S) refer to internal elementhood: (x∈S)(x \in S) means ⟨x,S⟩∈X×PX\langle x, S \rangle \in X \times PX is in ∈ X⊆X×PX\in_{X} \subseteq X \times PX, and (S∈F)(S \in F) means ⟨S,F⟩∈PX×PPX\langle S, F \rangle \in PX \times PPX is in ∈ PX⊆PX×PPX\in_{PX} \subseteq PX \times PPX.

We There have is all a slight catch, in that the ingredients predicates to deal with the logical formula on the right: we have an implication operator “ ⇒ (S∈ PXF) \Rightarrow (S \in_{PX} F) ” as and part “ of the internal Heyting algebra structure onP(1x∈ XS) P(1) (x \in_X S) , ” and (as we generalized have predicates the over quantification operator “∀ PXPX \forall_{PX} PX ”. , The where atomic expressions(S∈F) (S S \in F) and lives) are taken over different domains. The first is of the formϕ 1:PPX→P(x1∈) PXS) (x \phi_1 \in : S) PPX \to P(1)^{PX} , refer and to the internal second elementhood: is of the formϕ 2:X→P(x1∈) PXS) (x \phi_2 \in : S) X \to P(1)^{PX} . means No matter: we just substitute in some dummy variables. That is, we just pull these maps back to a common domain⟨PPXx,S⟩∈X× PX X \langle PPX x, S \rangle \in X \times PX X , is forming in the composites∈ X⊆X×PX\in_{X} \subseteq X \times PX, and (S∈F)(S \in F) means ⟨S,F⟩∈PX×PPX\langle S, F \rangle \in PX \times PPX is in ∈ PX⊆PX×PPX\in_{PX} \subseteq PX \times PPX.

Jon Awbrey: I didn’t know what to do with the extra slashes in the above paragraph that weren’t parsing, so I deleted them.

ψ 1=(PPX×X→π 1PPX→ϕ 1P(1) PX)\displaystyle \psi_1 = (PPX \times X \stackrel{\pi_1}{\to} PPX \stackrel{\phi_1}{\to} P(1)^{PX})

There is a slight catch, in that the predicates “(S∈ PXF)(S \in_{PX} F)” and “(x∈ XS)(x \in_X S)” (as generalized predicates over PXPX, where SS lives) are taken over different domains. The first is of the form ϕ 1:PPX→P(1) PX\phi_1 : PPX \to P(1)^{PX}, and the second is of the form ϕ 2:X→P(1) PX\phi_2 : X \to P(1)^{PX}. No matter: we just substitute in some dummy variables. That is, we just pull these maps back to a common domain PPX×XPPX \times X, forming the composites

ψ 1=(PPX×X→π 1PPX→ϕ 1P(1) PX)\displaystyle \psi_1 = (PPX \times X \stackrel{\pi_1}{\to} PPX \stackrel{\phi_1}{\to} P(1)^{PX})

and

ψ 2=(PPX×X→π 2X→ϕ 2P(1) PX).\displaystyle \psi_2 = (PPX \times X \stackrel{\pi_2}{\to} X \stackrel{\phi_2}{\to} P(1)^{PX}).

Putting all this together, we form the composite

PPX×X→⟨ψ 1,ψ 2⟩P(1) PX×P(1) PX\displaystyle PPX \times X \stackrel{\langle \psi_1, \psi_2 \rangle}{\to} P(1)^{PX} \times P(1)^{PX}

≅(P(1)×P(1)) PX→(⇒) PXP(1) PX→∀ PXP(1)\displaystyle \cong (P(1) \times P(1))^{PX} \stackrel{(\Rightarrow)^{PX}}{\to} P(1)^{PX} \stackrel{\forall_{PX}}{\to} P(1)

This composite directly expresses the definition of the internal predicate (x∈⋂F)(x \in \bigcap F) given above. By cartesian closure, this map PPX×X→P(1)PPX \times X \to P(1) induces the desired internal intersection operator, ⋂:PPX→PX\bigcap : PPX \to PX.

This construction provides an important bridge to getting the rest of the internal logic of ETCS. Since we can can construct the intersection of arbitrary definable families of subsets, the power sets PXPX are internal inf-lattices. But inf-lattices are sup-lattices as well; on this basis we will be able to construct the colimits ( e.g., finite sums, coequalizers) that we need. Similarly, the intersection operators easily allow us to construct image factorizations: any function f:X→Yf : X \to Y can be factored (in an essentially unique way) as an epi or surjection X→IX \to I to the image, followed by a mono or injection I→YI \to Y. The trick is to define the image as the smallest subset of YY through which ff factors, by taking the intersection of all such subsets. Image factorization leads in turn to the construction of existential quantification.

As remarked above, the internal logic of a topos is generally intuitionistic (the law of excluded middle is not satisfied). But, if we add in the axiom of strong extensionality of ETCS, then we’re back to ordinary classical logic, where the law of excluded middle is satisfied, and where we just have the two truth values “true” and “false”. This means we will be able to reason in ETCS set theory just as we do in ordinary mathematics, taking just a bit of care with how we treat membership. The foregoing discussion gives indication that logical operations in categorical set theory work in ways familiar from naive set theory, and that basic set-theoretic constructions like intersection are well-grounded in ETCS.