On the Distinction Between Sets and Classes: A Categorical Perspective

Abstract

According to Kreisel, category theory provides a powerful tool to organize mathematics. An example of this descriptive power is the categorical analysis of the practice of presenting classes as shorthands in ZF set theory. In this case, category theory provides a natural way to describe the relation between mathematics and metamathematics. If metamathematics can be described by using categories (in particular syntactic categories), the mathematical level can be represented by internal categories. Through this two-level interpretation, we can clarify the relation between classes and sets in ZF; in particular, we can describe two equivalent categorical notions of definable sets. Some common sayings about set theory are interpreted on the basis of this representation, emphasizing the distinction between naïve and rigorous sentences about sets and classes.

These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

1 Introduction

1.1 The Thorny Relation Between Categories and Sets

The relation between sets and categories is a thorny and intriguing topic (see, e.g., Blass 1984). The set-theoretical foundations of category theory were discussed by some mathematicians, e.g., by Feferman (1977), Engler (1969), and Lolli (1977). On the contrary, the categorical foundation of set theory is not yet a completely clear matter. Categorical logic allows us to talk about the categorical models of mathematical theories; in particular, it makes possible to talk about the categorical models of set theories, for example, IZF, CZF, and ZF. In 1995, Joyal and Moerdijk in their algebraic set theory (Joyal and Moerdijk 1995) proposed a technique to ensure the existence of internal models of ZF and IZF in a category. Before this, mathematicians had proposed categorical models of set theory within categories. However, these categories were still built using a model of set theory. Joyal and Moerdijk’s approach has thus two main advantages:

• 1. It allows to prove the existence of a model of IZF inside a category by simply checking some purely categorical properties of a family of arrows.

• 2. It works for a relatively large family of categories.

Their book led to the large spread of several works (see, e.g., Awodey et al. (2007) or Simpson (1999)). Algebraic set theory was expected to be not only a useful tool for mathematics but also something interesting for foundational studies.

Category theory provides a foundation for mathematics: this is maybe one of the most striking and imprecise sentences (see, e.g., Marquis 1995; Landry and Marquis 2005). In fact this is not necessarily wrong, but it is indispensable to clearly explain the meaning of the words foundation for mathematics. Kreisel observed (see e.g., Kreisel 1971) that category theory provides a powerful tool to organize mathematics; this is also what many mathematicians interested in category theory think, considering it as a foundation.

However, there are also some proposals to use category theory to build a theory of sets based on functions. On such a theory, it is possible to found the whole mathematical building: the typical examples are the axiomatic systems proposed by Lawvere (2005) and philosophically analyzed by McLarty, for example, in McLarty (2004).

This paper is in accordance with the first vision of category theory as a foundation: we think that category theory describes mathematics in a very effective way. In the following pages, this descriptive power will be shown by using category theory to explain the role of classes in the practice of ZF set theory. Category theory—both in its usual and in its internal version—will be used to represent the relation between mathematics and metamathematics.

1.2 A Nontrivial Question

The original title of this paper was What is the real category of sets?. Since it was a little pretentious and too vague, we changed it into the present one. However, the question What is the real category of sets? is strongly connected with the content of the paper and has been the motivation for the work. In fact, in the practice of mathematics, we often refer to the category of sets, even if we use a category of sets. Actually we typically use categories of sets which are built starting from a given model of ZF set theory. So the question should be rephrased as follows: Is there anything that is uniquely determined and that can be called the real category of sets? If such a category exists, then it must be the common core of all the different categories of sets. This is why we chose to propose an answer considering the syntactic category of definable classes of ZF and its internal category of sets (which are in fact mere syntactical constructions). This is motivated by a fundamental correspondence between functors defined on the syntactic category of a theory with values in a category equipped with appropriate structures and models of the same theory in it. This particularly applies to ZF.

1.3 Classes and ZF

Set theory is mainly ZF (or—in other words—most set theorists study ZF). ZF is a classical first-order theory with equality, and its language has (countably many) individual variables, no functional symbols, and a binary relational symbol ∈ ; its specific axioms are the following ones:

• 1. $\forall x\forall y(\forall t(t \in x \leftrightarrow t \in y) \rightarrow x = y)$;

• 2. For every formula P with free variables $p_{1},\ldots,p_{k},t$,

  $$\displaystyle{\forall p_{1}\ldots \forall p_{k}\forall x\exists y\forall t(t \in y \leftrightarrow (t \in x \wedge P));}$$

• 3. $\forall x\forall y\exists z\forall t(t \in z \leftrightarrow (t = x \vee t = y))$;

• 4. $\forall x\exists z\forall t(t \in z \leftrightarrow \exists y(t \in y \wedge y \in x))$;

• 5. $\forall y\exists z\forall x(x \in z \leftrightarrow x \subseteq y)$;

• 6. For every formula F with free variables p ₁, . . , p _k , x, y,

  $$\displaystyle{\forall p_{1}\ldots \forall p_{k}\forall z(\forall x(x \in z \rightarrow \exists !yF) \rightarrow \exists z'\forall x(x \in z \rightarrow \exists y(y \in z' \wedge F)));}$$

• 7. $\exists x(0 \in x \wedge \forall t(t \in x \rightarrow \sigma (t) \in x))$;

• 8. $\forall x(x\neq 0 \rightarrow \exists z(z \in x \wedge \forall t(t \in x \rightarrow t\notin z)))$;

where, as usual, x ⊆ y is a shorthand for $\forall t(t \in x \rightarrow t \in y)$, σ(t) stays for $t \cup \left \{t\right \}$, and 0 is a shorthand for the empty set. In detail, for every formula P = P(x),

$$\displaystyle\begin{array}{rcl} & & P(\sigma (t))\ \mbox{ means}\ \forall x(\forall s(s \in x \leftrightarrow ((s = t) \vee (s \in t))) \rightarrow P(x))\ \mbox{ and} {}\\ & & \qquad \qquad \qquad P(0)\ \mbox{ means}\ \forall x(\forall t(t\notin x) \rightarrow P(x)). {}\\ \end{array}$$

Set theorists work with sets, but they also talk about classes. However, classes do not exist in ZF. In practice, set theorists consider classes as shorthands or formal writings. If P is a formula with a distinguished variable x, then a class is a formal writing $\left \{x\vert P(x)\right \}$, and the expression

$$\displaystyle{t \in \left \{x\vert P(x)\right \}}$$

is simply a shorthand for P[t∕x]. For example, set theorists write $t \in \mathcal{V}$, as a shorthand for $t \in \left \{x\vert x = x\right \}$, which is a shorthand for t = t. They also write $t \in \mathcal{O}\mathcal{N}$ as a shorthand for $t \in \left \{x\vert ON(x)\right \}$, which is a shorthand for ON(t), where ON(x) is the formula expressing that x is an ordinal:

$$\displaystyle\begin{array}{rcl} & & \qquad \forall s\forall s'\forall s''((s \in t \wedge s' \in t \wedge s'' \in t \wedge s \in s' \wedge s' \in s'') \rightarrow s \in s'') \wedge {}\\ & &\wedge \forall s\forall s'((s \in t \wedge s' \in t \wedge s\neq s') \rightarrow (s \in s' \vee s' \in s)) \wedge \forall s(s \in t \rightarrow s \subseteq t). {}\\ \end{array}$$

It is clear that classes are not mathematical, but metamathematical objects. However, these shorthands share some properties with sets. For instance, the notion of intersection of classes or the notion of subclass can be given a meaning. This accidental fact leads of course to some confusion! As a matter of fact, the metamathematical level is often mixed up with the mathematical one. As a consequence, impressive (but at the same time highly incorrect) assertions are not uncommon. This is a typical example:

$$\displaystyle{\mbox{ Sets are exactly those classes for which the comprehension axiom is true.}({\ast})}$$

Sentences like this can be used as a sort of convincing arguments to give students a hint of the notion of set. Nonetheless, in the context of ZF, these statements sound quite dangerous rather than useful.

Set theorists easily use classes, which are formal objects, as quasi-sets, for two reasons. Firstly, we have already seen that their syntactical structure (and in particular the use of connectives and quantifiers) makes this legitimate for many operations. Secondly, set theorists know that the theory of classes NBG is a conservative extension of ZFC. Nevertheless, in this context, classes are nothing more than syntactical objects.

In the following sections, we will see how the use of category theory can help to describe the relation between metamathematics and mathematics. Furthermore, category theory makes easier the distinction between real sentences about sets and external (naïve) ones.

2 The Syntactic Category of ZF

In this section, we will study the category of ZF definable classes and its relevant subcategories. First of all, we want to define the syntactic category of ZF (see Johnstone (2002) for the general construction). We will indicate it with $\mathbf{Z}\mathbf{F}$. Its objects are formulas in context, i.e., the following formal writings:

$$\displaystyle{\left \{x_{1},\ldots,x_{n}\vert P\right \},}$$

where $x_{1},\ldots,x_{n}$ is a (possibly empty) list of distinct variables and P is a formula which has free variables among $x_{1},\ldots,x_{n}$. An arrow from a formula in context $\left \{\mathbf{x}\vert P\right \}$ to another formula in context $\left \{\mathbf{y}\vert Q\right \}$ is an equivalence class of formulas in context

$$\displaystyle{[\left \{\mathbf{x}',\mathbf{y}'\vert F\right \}]_{\equiv },}$$

where x′ is a list of variables having the same length as x and y′ is a list of variables having the same length as y, which satisfies the following requirements:

• 1. $F \vdash _{ZF}P[\mathbf{x}'/\mathbf{x}] \wedge Q[\mathbf{y}'/\mathbf{y}]$.

• 2. $F \wedge F[\mathbf{y}''/\mathbf{y}'] \vdash _{ZF}\mathbf{y}' = \mathbf{y}''$.

• 3. $P[\mathbf{x}'/\mathbf{x}] \vdash _{ZF}\exists \mathbf{y}'F$.

The equivalence relation is given by

$$\displaystyle{\left \{\mathbf{x}',\mathbf{y}'\vert F\right \} \equiv \left \{\mathbf{x}'',\mathbf{y}''\vert F'\right \}\mbox{ iff } \vdash _{ZF}F \leftrightarrow F'[\mathbf{x}'/\mathbf{x}'',\mathbf{y}'/\mathbf{y}''].}$$

For the composition, it is enough to consider the composable arrows $[\left \{\mathbf{x}',\mathbf{y}'\vert F\right \}]_{\equiv }$ and $[\left \{\mathbf{y}',\mathbf{z}'\vert F'\right \}]_{\equiv }$ with all distinct variables (this doesn’t determine a loss of generality). In this case, the composition is given by

$$\displaystyle{[\left \{\mathbf{x}',\mathbf{z}'\vert \exists \mathbf{y}'(F \wedge F')\right \}]_{\equiv }.}$$

For very general reasons, the category we obtain is regular and Boolean (see Johnstone (2002) for a proof). In particular we recall the fact that the product of two objects $\left \{\mathbf{x}\vert P\right \}$ and $\left \{\mathbf{y}\vert Q\right \}$ is given by

$$\displaystyle{\left \{\mathbf{x},\mathbf{y}\vert P \wedge Q\right \},}$$

where we have supposed (without loss of generality) that all variables involved are distinct. Moreover, terminal objects are given for example by

$$\displaystyle{\left \{\;\vert \forall x(x = x)\right \},\mbox{ either }\left \{x\vert \forall t(t\notin x)\right \}.}$$

We can also easily prove that $\mathbf{Z}\mathbf{F}$ is extensive, thanks to the fact that

$$\displaystyle{\vdash _{ZF}0\neq 1,}$$

where 1 stays for σ(0).

Initial objects are given, for example, by

$$\displaystyle{\left \{\;\vert \exists x(x\neq x)\right \},\mbox{ either }\left \{x\vert x\neq x\right \}.}$$

$\mathbf{Z}\mathbf{F}$ is also an exact category; the proof of it is based on Scott’s trick (see Rosolini 2011; Maschio 2012). Finally, $\mathbf{Z}\mathbf{F}$ has also a subobject classifier that is given by

$$\displaystyle{[\left \{x,x'\vert x = 0 \wedge x' = 1\right \}]_{\equiv }: \left \{x\vert x = 0\right \} \rightarrow \left \{x\vert x = 0 \vee x = 1\right \}.}$$

2.1 Definable Classes

The category of definable classes of ZF, which we denote with $\mathbb{D}\mathbb{C}\mathbb{L}[ZF]$, is the full subcategory of $\mathbf{Z}\mathbf{F}$ which is determined by all those objects having a list of variables with length 1. This is clearly conceived of as the category of classes, in the context of the practice of ZF.

Although $\mathbb{D}\mathbb{C}\mathbb{L}[ZF]$ is a subcategory of $\mathbf{Z}\mathbf{F}$, it is provable to be equivalent to it. This results from the possibility to represent ordered pairs in ZF:

$$\displaystyle{x =< x_{1},x_{2} >\equiv ^{def}x = \left \{\left \{x_{ 1}\right \},\left \{x_{1},x_{2}\right \}\right \}.}$$

An arbitrary object of $\mathbf{Z}\mathbf{F}$, $\left \{x_{1},..,x_{n}\vert P\right \}$, is isomorphic to

$$\displaystyle{\left \{x\vert \exists x_{1}\ldots \exists x_{n}(x =<<\ldots < x_{1},x_{2} >,\ldots >,x_{n} > \wedge P)\right \},}$$

where x is a variable not included in $x_{1},\ldots,x_{n}$.

2.2 The Categorical Side of Class Operations

At this point, we would like to give an example of the categorical interpretation of the practical operations between classes. Our aim is to prove how adequate $\mathbb{D}\mathbb{C}\mathbb{L}[ZF]$ is for the description of the category of formal classes. On this purpose, we will focus on intersection. We consider two definable classes $\left \{x\vert P\right \}$ and $\left \{y\vert Q\right \}$ (we can assume that x and y are distinct without loss of generality); we usually consider their intersection as $\left \{x\vert P \wedge Q[x/y]\right \}$. However, this operation can be expressed in mere categorical terms. In fact $\left \{x\vert P \wedge Q[x/y]\right \}$ is isomorphic in $\mathbb{D}\mathbb{C}\mathbb{L}[ZF]$ to the object we obtain by considering the following pullback.

2.3 Definable Sets

Now we will consider the full subcategory $\mathbf{D}\mathbf{S}\mathbf{T}[ZF]$ of $\mathbb{D}\mathbb{C}\mathbb{L}[ZF]$ determined by the objects $\left \{x\vert P\right \}$ for which

$$\displaystyle{\vdash _{ZF}\exists z\forall x(x \in z \leftrightarrow P).}$$

This is the category of sets we have in mind, when we think sentence (∗) is true.

We obtain the following result:

Theorem 10.2.1.

$\mathbf{D}\mathbf{S}\mathbf{T}[ZF]$ is a Boolean topos.

Proof.

Finite limits exactly correspond to finite limits in $\mathbf{Z}\mathbf{F}$: a terminal object is given by $\left \{x\vert x = 0\right \}$, equalizers are exactly equalizers in $\mathbf{Z}\mathbf{F}$, while the product of two definable sets $\left \{x\vert P\right \}$, $\left \{y\vert Q\right \}$ is given by

$$\displaystyle{\left \{z\vert \exists x\exists y(z =< x,y > \wedge P \wedge Q)\right \}}$$

with the obvious projections (we are assuming x and y to be distinct without loss of generality). The subobject classifier is exactly the subobject classifier of $\mathbf{Z}\mathbf{F}$, while exponentials $\left \{y\vert Q\right \}^{\left \{x\vert P\right \}}$ are given by

$$\displaystyle{\left \{f\vert \mathrm{Fun}(f) \wedge \forall s(s \in \mathrm{ dom}(f) \leftrightarrow P(s)) \wedge \forall s'(s' \in \mathrm{ ran}(f) \rightarrow Q(s'))\right \},}$$

with the evaluation arrow given by

$$\displaystyle\begin{array}{rcl} [\{F,y\vert \exists f\exists x(F =< f,x > \wedge \ \mathrm{Fun}(f)& \wedge & \forall s(s \in \mathrm{ dom}(f) \leftrightarrow P(s)) \wedge {}\\ \wedge \forall s'(s' \in \mathrm{ ran}(f)& \rightarrow & Q(s'))\wedge < x,y >\in f)\}]_{\equiv }. {}\\ \end{array}$$

 □ 

3 Algebraic Set Theory in the Syntactic Category of ZF

In order to better understand the relation between formal classes, definable sets, and sets, we are now going to talk a little about algebraic set theory and the syntactic category of ZF following Rosolini’s example in Rosolini (2011); in fact the notion of definable sets is strictly connected with a specific notion of small maps in $\mathbf{Z}\mathbf{F}$.

3.1 Simpson’s Axioms for Algebraic Set Theory

In this section, we will introduce a list of axioms for algebraic set theory proposed by Simpson (see Simpson 1999). Every axiomatization of algebraic set theory is based on a pair $(\mathbf{C},\mathcal{S})$ in which $\mathbf{C}$ is a category and $\mathcal{S}$ is a family of arrows of $\mathbf{C}$ (called family of small maps). The axioms are the following ones:

• 1. $\mathbf{C}$ is a regular category.

• 2. The composition of two arrows in $\mathcal{S}$ is in $\mathcal{S}$.

• 3. Every mono is in $\mathcal{S}$.

• 4. (Stability) If $f \in \mathcal{S}$ and f′ is a pullback of f, then $f' \in \mathcal{S}$.

• 5. (Representability) For every X, there exists an object $\mathcal{P}_{\mathcal{S}}(X)$ and an arrow $e_{X}:\in _{X} \rightarrow X \times \mathcal{P}_{\mathcal{S}}(X)$ with $\pi _{2} \circ e_{X} \in \mathcal{S}$ so that, for every $\psi: R \rightarrow X \times Z$ with $\pi _{2}\circ \psi \in \mathcal{S}$, there exists a unique arrow $\rho: Z \rightarrow \mathcal{P}_{\mathcal{S}}(X)$ that fits in a pullback as follows:

  

• 6. (Power Set) $\sqsubseteq _{X}:\subseteq _{X} \rightarrow \mathcal{P}_{\mathcal{S}}(X) \times \mathcal{P}_{\mathcal{S}}(X)$ satisfies $\pi _{2}\circ \sqsubseteq _{X} \in \mathcal{S}$,

  where $\sqsubseteq _{X}$ is determined by the following property:

  An arrow $f =< f_{1},f_{2} >: Z \rightarrow \mathcal{P}_{\mathcal{S}}(X) \times \mathcal{P}_{\mathcal{S}}(X)$ factorizes through $\sqsubseteq _{X}$ if and only if considering the following pullbacks

  

  the arrow $\pi$ factorizes through $\pi '$.

We also want to recall some definitions:

Definition 10.3.1.

An object U in a category $\mathbf{C}$ is universal, if for every object X in $\mathbf{C}$, there exists a mono $j: X \rightarrow U$.

Definition 10.3.2.

An object U in a regular category $\mathbf{C}$ with a class of small maps $\mathcal{S}$ is a universe if there exists a mono $j: \mathcal{P}_{\mathcal{S}}(U) \rightarrow U$.

Definition 10.3.3.

A ZF-algebra for a regular category $\mathbf{C}$ with a class of small maps $\mathcal{S}$ is an internal sup-semilattice $(U,\subseteq )$ together with an arrow $\sigma: U \rightarrow U$, so that for every $\lambda: B \rightarrow U$ and for every $j: B \rightarrow A \in \mathcal{S}$, there exists $\mathrm{sup}_{j}(\lambda ): A \rightarrow U$ so that for any $j': B' \rightarrow A$ and $\lambda ': B' \rightarrow U$, once we consider the following pullback

we have that

$$\displaystyle{\mathrm{sup}_{j}(\lambda ) \circ j' \subseteq \lambda '\mbox{ if and only if }\lambda \circ \pi _{2} \subseteq \lambda '\circ \pi _{1}.}$$

The morphisms of ZF-algebras are the morphisms between internal sup-semilattices that preserve $\mathrm{sup}_{j}(\lambda )$ along $j \in \mathcal{S}$ and commute with the arrows σ. An initial Z F-algebra is an initial object in the category of ZF-algebras and morphisms between them.

3.2 Small Maps in$\mathbf{Z}\mathbf{F}$

We now want to define a class $\mathcal{S}_{ZF}$ of small maps in $\mathbb{D}\mathbb{C}\mathbb{L}[ZF]$. An arrow

is in $\mathcal{S}_{ZF}$ if and only if

$$\displaystyle{\vdash _{ZF}\forall y\exists z\forall x(F(x,y) \leftrightarrow x \in z).}$$

The class $\mathcal{S}_{ZF}$ is a class of small maps, as Simpson means (Simpson 1999):

Lemma 10.3.4.

Every mono is in $\mathcal{S}_{ZF}$ .

Proof.

This is obtained by using axiom 2 to obtain the existence of an empty set and axiom 3 to prove the existence of singletons, once we notice that an arrow

$$\displaystyle{[\left \{x,y\vert F\right \}]_{\equiv }}$$

is mono if and only if

$$\displaystyle{F \wedge F[x'/x] \vdash _{ZF}x = x'}$$

 □ 

Lemma 10.3.5.

Every composition of arrows in $\mathcal{S}_{ZF}$ is in $\mathcal{S}_{ZF}$ .

Proof.

This is obtained by using axioms 6 and 4 □ 

Lemma 10.3.6.

The stability axiom is satisfied by $\mathcal{S}_{ZF}$ .

Proof.

This is obtained by using axiom 6. □ 

Lemma 10.3.7.

The representability axiom is satisfied by $\mathcal{S}_{ZF}$ .

Proof.

A definable class $X = \left \{x\vert P\right \}$ is fixed. Then, the definable class $\mathcal{P}_{\mathcal{S}_{ZF}}(X)$ is given by

$$\displaystyle{\left \{y\vert \forall x(x \in y \rightarrow P)\right \},}$$

while the definable class ∈  _X is given by

$$\displaystyle{\left \{z\vert \exists x\exists y(z =< x,y > \wedge \forall t(t \in y \rightarrow P(t)) \wedge x \in y)\right \},}$$

and the arrow e _X : $\in _{X} \rightarrow X \times \mathcal{P}_{\mathcal{S}_{ZF}}(X)$ is given by

$$\displaystyle{[\left \{z,z'\vert \exists x\exists y(z =< x,y > \wedge \forall t(t \in y \rightarrow P(t)) \wedge x \in y) \wedge z = z'\right \}]_{\equiv }.}$$

Now if the following arrow

satisfies $R(x,y) \vdash _{ZF}P(x) \wedge Q(y)$ and $\vdash _{ZF}\forall y\exists y'\forall x(R(x,y) \leftrightarrow x \in y')$, which means that it represents (without loss of generality) a relation with the second component in $\mathcal{S}_{ZF}$, then its representing arrow from $\left \{y\vert Q\right \}$ to $\mathcal{P}_{\mathcal{S}_{ZF}}(X)$ is given by

$$\displaystyle{[\left \{y,y'\vert Q \wedge \forall x(R(x,y) \leftrightarrow x \in y')\right \}]_{\equiv }.}$$

 □ 

Lemma 10.3.8.

The power set axiom is satisfied by $\mathcal{S}_{ZF}$ .

Proof.

The subset relation for $\left \{x\vert P\right \}$ is given by the following arrow:

$$\displaystyle{[\left \{z,z'\vert \exists y\exists y'(z =< y,y' > \wedge y \subseteq y' \wedge \forall x(x \in y' \rightarrow P(x))) \wedge z = z'\right \}]_{\equiv }}$$

from $\left \{z\vert \exists y\exists y'(z =< y,y' > \wedge y \subseteq y' \wedge \forall x(x \in y' \rightarrow P(x)))\right \}$ to $\mathcal{P}_{\mathcal{S}_{ZF}}(X) \times \mathcal{P}_{\mathcal{S}_{ZF}}(X)$.

This relation is in $\mathcal{S}_{ZF}$ by virtue of axiom 5. □ 

3.3 An Algebraic Set-Theoretical Light on Definable Sets

First of all, the small definable classes are exactly those classes $\left \{x\vert P\right \}$ for which the unique arrow to 1, which is $[\left \{x,y\vert P \wedge y = 0\right \}]$, is small. This means that

$$\displaystyle{\vdash _{ZF}\forall y\exists z\forall x(x \in z \leftrightarrow (P(x) \wedge y = 0)).}$$

Now we know that

$$\displaystyle{\vdash _{ZF}\exists y(y = 0)}$$

and so the previous condition is equivalent to

$$\displaystyle{\vdash _{ZF}\exists z\forall x(x \in z \leftrightarrow P(x)).}$$

This means that the small definable classes are exactly the definable sets. Furthermore, $\left \{x\vert N(x)\right \}$ is a small definable class, where N(x) is the formula saying that x is a finite ordinal: this follows from axioms 7 and 2.

Finally, $\left \{x\vert x = x\right \}$ is a universal definable class (and so also a universe), because, for every definable class $\left \{x\vert P\right \}$, the arrow $[\left \{x,x'\vert P \wedge x = x'\right \}]_{\equiv }$ is a mono from $\left \{x\vert P\right \}$ to $\left \{x\vert x = x\right \}$.

Last but not least, there exists an explicit (and obvious) representation for an initial ZF-algebra: this is given by

$$\displaystyle{(\left \{x\vert x = x\right \},\sqsubseteq _{\left \{x\vert x=x\right \}},[\left \{x,z\vert z = \left \{x\right \}\right \}]_{\equiv }).}$$

If

$$\displaystyle{[\left \{z,z'\vert F(z,z')\right \}]_{\equiv }: \left \{z\vert P\right \} \rightarrow \left \{z'\vert Q\right \}}$$

is small in $\mathbb{D}\mathbb{C}\mathbb{L}[ZF]$, and $[\left \{z,x\vert \lambda (z,x)\right \}]_{\equiv }$ is an arrow from $\left \{z\vert P\right \}$ to $\left \{x\vert x = x\right \}$, then

$$\displaystyle{\mathrm{sup}_{[\left \{z,z'\vert F(z,z')\right \}]}([\left \{z,x\vert \lambda (z,x)\right \}]_{\equiv })}$$

is given by the arrow

$$\displaystyle{[\left \{z',x\vert Q \wedge \forall t(t \in x \leftrightarrow \exists z(F(z,z') \wedge \lambda (z,t)))\right \}]_{\equiv }.}$$

4 The Internal Category of Sets

In this section, we will introduce internal category theory to build an internal category of sets in $\mathbf{Z}\mathbf{F}$. This will be the internal topos induced by the initial ZF-algebra for $\mathcal{S}_{ZF}$.

4.1 Internal Category Theory

First of all, we need to recall the notion of internal category, which is the generalization of the notion of small category. Although we can define an internal category in an arbitrary category (requiring the existence of certain pullbacks), we prefer considering the case of a category $\mathbf{C}$ with all finite limits.

Definition 10.4.1.

An internal category of $\mathbf{C}$ is a 6-ple

$$\displaystyle{(C_{0},C_{1},\delta _{0},\delta _{1},ID,\square )}$$

in which C ₀, C ₁ are objects of $\mathbf{C}$ and $\delta _{0},\delta _{1}: C_{1} \rightarrow C_{0}$, $ID: C_{0} \rightarrow C_{1}$,

$$\displaystyle{\square: C_{1} \times _{\square }C_{1} \rightarrow C_{1}}$$

are arrows of $\mathbf{C}$, where $C_{1} \times _{\square }C_{1}$ fits in the following pullback.

The 6-ple $\mathbf{C}$ must satisfy the following requirements:

• 1. $\delta _{1} \circ ID =\delta _{0} \circ ID = id_{C_{0}}$.

• 2. $\delta _{0} \circ \square =\delta _{0} \circ p_{0}$ and $\delta _{1} \circ \square =\delta _{1} \circ p_{1}$.

• 3. $\square \circ \lceil ID \circ \delta _{0},id_{C_{1}}\rceil = \square \circ \lceil id_{C_{1}},ID \circ \delta _{1}\rceil = id_{C_{1}}$.

• 4. $\square \circ \lceil \square \circ p_{0},p_{1}\rceil = \square \circ \lceil p_{0},\square \circ p_{1}\rceil \circ \lceil p_{0}\circ p_{0},\lceil p_{1}\circ p_{0},p_{1}\rceil \rceil: (C_{1}\times _{\square }C_{1})\times _{\square }C_{1} \rightarrow C_{0}$.

Here we denote with $\lceil f,f'\rceil$ the unique arrow that exists for the definition of pullback, and $(C_{1} \times _{\square }C_{1}) \times _{\square }C_{1}$ is the pullback of $\delta _{1} \circ \square$ and δ ₀.

Before going to the next section, we show a way to externalize internal categories. This is done in a very natural way by means of global elements.

Proposition 10.4.2.

If $\mathcal{C} = (C_{0},C_{1},\delta _{0},\delta _{1},ID,\square )$ is an internal category of $\mathbf{C}$ and I is an object of $\mathbf{C}$ , then

$$\displaystyle{\mathrm{Hom}(I,\mathcal{C})\!:=\! (\mathrm{Hom}(I,C_{0}),\mathrm{Hom}(I,C_{1}),\delta _{0}\circ (-),\delta _{1}\circ (-),\mathit{ID}\circ (-),\square \circ \lceil (-)_{1},(-)_{2}\rceil )}$$

is a category.

Proof.

Every point of the definition of category follows immediately because of the relative point in the definition of internal category. This is possible as the functor $\mathrm{Hom}(I,\bullet )$ preserves all finite limits. □ 

We will denote by $\Gamma (\mathcal{C})$ the category $\mathrm{Hom}(1,\mathcal{C})$, where 1 is a (selected) terminal object of $\mathbf{C}$.

Remark 10.4.3.

We should notice that an internal category in a category $\mathbf{C}$ with all finite limits is nothing more than a model of the first-order theory of categories (see Johnstone 2002) in $\mathbf{C}$.

4.2 The Real Category of Sets:$\mathcal{S}\mathcal{E}\mathcal{T}$

We will now define an internal category of $\mathbf{Z}\mathbf{F}$ (or equivalently of $\mathbb{D}\mathbb{C}\mathbb{L}(ZF)$), called $\mathcal{S}\mathcal{E}\mathcal{T}$, which is built on the initial ZF-algebra for $\mathcal{S}_{ZF}$. This category is given by the following assignments:

• 1. $\mathcal{S}\mathcal{E}\mathcal{T}_{0}:= \left \{x\vert x = x\right \}$.

• 2. $\mathcal{S}\mathcal{E}\mathcal{T}_{1}:= \left \{F\vert \exists f\exists z(F =< f,z > \wedge \mathrm{Fun}(f) \wedge \mathrm{ ran}(f) \subseteq z)\right \}$.

• 3. $\delta _{0}:= [\left \{F,x\vert \exists f\exists z(F =< f,z > \wedge \mathrm{Fun}(f) \wedge \mathrm{ ran}(f) \subseteq z \wedge \mathrm{ dom}(f) = x)\right \}]_{\equiv }$.

• 4. $\delta _{1}:= [\left \{F,z\vert \exists f(F =< f,z > \wedge \mathrm{Fun}(f) \wedge \mathrm{ ran}(f) \subseteq z)\right \}]_{\equiv }$.

• 5. $ID:= [\left \{x,F\vert \exists f(F =< f,x > \wedge \forall t(t \in f \leftrightarrow \exists s(s \in x \wedge t =< s,s >)))\right \}]_{\equiv }$.

• 6.
  $$\displaystyle\begin{array}{rcl} & & \qquad \square:= [\{J,G\vert \exists f\exists f'\exists z\exists f''(J =< f,< f',z >> \wedge \mathrm{Fun}(f) \wedge \mathrm{ Fun}(f') {}\\ & & \qquad \qquad \quad \wedge \mathrm{ ran}(f) \subseteq \mathit{dom}(f') \wedge \mathit{ran}(f') \subseteq z \wedge G =< f'',z > \wedge {}\\ &&\wedge \forall t(t\! \in \! f'' \leftrightarrow (\exists s\exists s'\exists s''(< s,s' >\in \! f\wedge < s',s'' >\in \! f' \wedge t\! =\!< s,s'' >))))\}]_{\equiv }, {}\\ \end{array}$$

  once we easily realized that the object of composable arrows is given by

  $$\displaystyle\begin{array}{rcl} & & \ \{J\vert \exists f\exists f'\exists z(J =< f,< f',z >> \wedge \mathrm{Fun}(f) \wedge {}\\ &&\wedge \mathrm{Fun}(f') \wedge \mathrm{ ran}(f) \subseteq \mathrm{ dom}(f') \wedge \mathrm{ ran}(f') \subseteq z)\}. {}\\ \end{array}$$

We obtain that

Theorem 10.4.4.

$\mathcal{S}\mathcal{E}\mathcal{T}$ is an internal category.

Proof.

See Johnstone (1977). □ 

We also derive that this is an internal topos, as every construction for a topos can be done in $\mathbf{Z}\mathbf{F}$. This follows from a well-written proof of the fact that sets and functions form a topos formalized in ZF.

Moreover, we should notice that this internal category exactly corresponds to the canonical interpretation (according to model theory) of the first-order theory of categories in ZF set theory.

5 Definable Sets and Global Elements

We have just well explained what we mean by the internal category $\mathcal{S}\mathcal{E}\mathcal{T}$; we now would like to study the category $\Gamma (\mathcal{S}\mathcal{E}\mathcal{T} )$. Following in detail the definition, the objects of $\Gamma (\mathcal{S}\mathcal{E}\mathcal{T} )$ are the equivalence classes $[\left \{x\vert P(x)\right \}]_{\equiv }$ of definable classes with the property that $\vdash _{ZF}\exists !xP(x)$. The arrows of $\Gamma (\mathcal{S}\mathcal{E}\mathcal{T} )$ are the classes of equivalence $[\left \{f\vert P(f)\right \}]_{\equiv }$ which satisfy ⊢  _ZF ∃! fP(f), and

$$\displaystyle{P(f) \vdash _{ZF}\exists f'\exists z(f =< f',z > \wedge \mathrm{Fun}(f') \wedge \mathrm{ ran}(f') \subseteq z).}$$

As a consequence, we have the following theorem:

Theorem 10.5.1.

$\mathbf{D}\mathbf{S}\mathbf{T}(ZF)$ and $\Gamma (\mathcal{S}\mathcal{E}\mathcal{T} )$ are equivalent.

Proof.

We need to consider the following functors:

• 1. $\mathbf{P}: \mathbf{D}\mathbf{S}\mathbf{T}(ZF) \rightarrow \Gamma (\mathcal{S}\mathcal{E}\mathcal{T} )$ is given by

  $\mathbf{P}(\left \{x\vert P(x)\right \}):= [\left \{z\vert \forall x(x \in z \leftrightarrow P(x))\right \}]_{\equiv }$

  $\mathbf{P}([\left \{x,y\vert F(x,y)\right \}]_{\equiv }):=$

  $:= [\{f'\vert \exists f\exists z(f' =< f,z > \wedge \forall t(t \in f \leftrightarrow \exists x\exists y(t =< x,y > \wedge F(x,y)))\wedge$

  $\wedge \forall y(y \in z \leftrightarrow Q(y)))\}]_{\equiv }$

• 2. $\mathbf{P'}: \Gamma (\mathcal{S}\mathcal{E}\mathcal{T} ) \rightarrow \mathbf{D}\mathbf{S}\mathbf{T}[ZF]$ is given by

  $\mathbf{P'}([\left \{z\vert P(z)\right \}]_{\equiv }):= \left \{x_{0}\vert \exists z(P(z) \wedge x_{0} \in z)\right \}$

  $\mathbf{P'}([\left \{f'\vert Q(f')\right \}]_{\equiv }):= [\left \{x,x'\vert \exists f'(Q(f') \wedge \exists z\exists f(f' =< f,z > \wedge < x,x' >\right.$ $\left.\in f))\right \}]_{\equiv }$

where x ₀ is a fixed variable. (We can think of it as the first variable. The condition for this is that the variables of the language of ZF are presented in a countable list.)

We can then immediately see that $\mathbf{P} \circ \mathbf{P'}$ is the identity functor for $\Gamma (\mathcal{S}\mathcal{E}\mathcal{T} )$, while there is a natural isomorphism from the identity functor of $\mathbb{D}\mathbb{C}\mathbb{L}[ZF]$ to $\mathbf{P'} \circ \mathbf{P}$, which is given by the arrows

$$\displaystyle{[\left \{x,x'\vert P(x) \wedge x = x'\right \}]_{\equiv }: \left \{x\vert P(x)\right \} \rightarrow \left \{x_{0}\vert \exists z(x_{0} \in z \wedge \forall x(x \in z \leftrightarrow P(x)))\right \}}$$

 □ 

We can think about objects of $\Gamma (\mathcal{S}\mathcal{E}\mathcal{T} )$ as sets with a name, because they are exactly determined by a class of formulas [P] with one free variable; the name of the object of $\Gamma (\mathcal{S}\mathcal{E}\mathcal{T} )$ determined by [P] could be, for example, [[P]].

6 Final Remarks

In our attempt to clarify the relation between (formal) classes and sets and between metamathematics and mathematics, by means of a unique mathematical structure, we started by introducing the syntactic category $\mathbf{Z}\mathbf{F}$ (that we proved to be equivalent to the category of definable classes of ZF). This category shapes the metamathematical level: its objects are classes as are usually (see, e.g., Jech 2003) introduced in the set theorists’ practice. Moreover, this category has an important full subcategory: the category of definable sets, whose objects are those definable classes $\left \{x\vert P\right \}$ for which

$$\displaystyle{\vdash _{ZF}\exists z\forall x(x \in z \leftrightarrow P).}$$

This corresponds to the naïve category of sets. Obviously, this is not the real category of sets. In this context, the real category of sets is $\mathcal{S}\mathcal{E}\mathcal{T}$. However, this is not a category: it is an internal category in $\mathbf{Z}\mathbf{F}$. The relation between metamathematics and mathematics in this context exactly corresponds to the relation between categories and internal categories. Mathematical concepts are represented through internal categories, and external (or metamathematical) concepts are expressed on the categorical level. In our opinion, the most interesting result described in the previous sections is the equivalence of the two most (at least in our opinion) natural ways to give an external account of the notion of set. We proved that the category of definable sets is equivalent to the category obtained by global sections on $\mathcal{S}\mathcal{E}\mathcal{T}$: the classes that satisfy the comprehension axiom are exactly those classes that can be named.