Is there a succinct way to axiomatize the theory of a single elementary topos?

Is there a succinct way to axiomatize the theory of a single elementary topos?

I'm trying to get a definition of an elementary topos that uses basic notions from logic as a way of understanding topoi better and understanding where certain non-topoi like the set theory NFU fail to meet the criteria for toposhood.

I'm curious if there's a way to axiomatize the theory of a single elementary topos that's reasonably straightforward, but still uses a logic in the background that's general purpose.

What follows is my attempt to produce an axiomatization of the theory of a single elementary topos. It is not succinct.

Here is my attempt to axiomatize the theory of a single elementary topos using first-order logic with multiple sorts. My attempt is very brute-force. It also does a lot of things that are weird and not idiomatic from a category theory perspective, like using objects directly rather than objects up to unique isomorphism all over the place.

Following this paper, I am defining an elementary topos as a category that:

• is cartesian-closed.
• has finite limits.
• has a subobject classifier.

As for having finite limits, I am following this article and saying that a category has finite limits if and only if it has a terminal object and admits all binary pullbacks.

Now for the first-order axiomatization.

Let $O$ be my sort of objects. Let $A$ be my sort of arrows. Let $S$ be the sort of ordered pairs of arrows with the same source, e.g. $(f, g) \in S \;\; \text{if} \;\; f : X \to Z \;\text{and}\; g : X \to W $. Let $D$ be the sort of ordered pairs of arrows with the same dest.

I will now define the following predicates and functions.

$C$ is a predicate of type $A \times A \times A \to 2$. $ C(a, b, c) $ holds if and only if $a \circ b$ = c.

Let $R$ be reverse composition. $C(f, g, h)$ holds if and only if $R(g, f, h)$ holds.

$\text{id}$ is a function of type $O \to A$. It sends each object to its identity arrow.

$\text{src} : A \to O$ sends an arrow to its source object.

$\text{dst} : A \to O$ sends an arrow to its destination object.

$\pi_1 : S \to A$ and $\pi_1 : D \to A$ selects the first element of a pair of arrows.

$\pi_2 : S \to A$ and $\pi_2 : D \to A$ selects the second element of a pair of arrows.

$ Q : S \times D \to 2$ is a predicate that holds if and only if the $S$ arrow-pair and the $D$ arrow-pair make a commutative diagram.

$ p : D \to S $ is a pullback. It takes a group of arrows with the same destination and sends to them to a group of arrows with the same source.

$ 1 $ is a constant in the sort $O$. It is the terminal object.

$ \Omega $ is a constant in the sort $O$. It is the subobject classifier.

$ \tau $ is a constant in the sort $A$. It is the $\mathsf{true}$ morphism.

$ M : A \to 2 $ is a predicate that is true if and only if its argument is a monomorphism.

Let $t : S \times S $ be a product. It sends a pair of morphisms with the same source to another pair of morphisms (the projections) with the same source (the product).

Let $w : O \times O \to O$ be the product of two objects.

Let $I : O \times O \to 2$ be uniqueness up to unique isomorphism.

Let $e : O \times O \to O$ be an exponential object.

Let $v : O \times O \to A$ be an evaluation map.

Let $J : A \times A \to 2$ hold of $(a, \chi_a)$ if and only if $\chi_a$ is the classifying morphism for the subobject represented by $j$.

Here is my attempt to axiomatize the theory of a single elementary topos.

Axiomatization of a category

Composition is associative.

$$ (\exists a \mathop. C(x, y, a) \land C(a, z, b)) \iff (\exists d \mathop. C(x, d, b) \land C(y, z, d)) $$

The composition is unique but need not exist.

$$ C(x, y, a) \land C(x, y, b) \to a = b $$

The composition of two arrows exists whenever the destination of the second is the source of the first.

$$ (\exists u \mathop. C(f, g, u)) \leftrightarrow \mathrm{dst}(g) = \mathrm{src}(f) $$

The source of the identity arrow on $o$ is $o$.

$$ \mathrm{src}(\mathrm{id}(o)) = o $$

The destination of the identity arrow on $o$ is $o$.

$$ \mathrm{dst}(\mathrm{id}(o)) = o $$

Composition produces an arrow with the expected source and destination.

$$ C(a, b, x) \to (\mathrm{dst}(a) = \mathrm{dst}(x) \land \mathrm{src}(b) = \mathrm{src}(x)) $$

The identity arrow is a left identity.

$$ C(\mathrm{id}(o), x, x) \leftrightarrow o = \mathrm{dst}(x) $$

The identity arrow is a right identity.

$$ C(x, \mathrm{id}(o), x) \leftrightarrow o = \mathrm{src}(x) $$

Here is the definition of uniqueness up to unique isomorphism.

$$ I(a, b) \iff (\exists! f \mathop. \mathrm{src}(f) = a \land \mathrm{dst}(f) = b \land (\exists g \mathop. C(f, g, \mathrm{id}(b)) \land C(g, f, \mathrm{id}(a)))) $$

A monomorphism is a left-cancellative morphism.

$$ M(f) \iff \forall m \mathop. C(f, g, m) \land C(f, h, m) \to f = g $$

Pairs of arrows

If $m$ and $q$ are both of sort $S$ or both of sort $D$, then if they have the same first and second arrow they are the same pair.

$$ \pi_1(m) = \pi_1(q) \land \pi_2(m) = \pi_2(q) \to m = q $$

A diagram consisting of a same-source pair and a same-destination pair commutes if and only if both paths through the diagram are the same.

$$ Q(s, d) \iff (\exists u \mathop. R(\pi_1(s), \pi_1(d), u) \land R(\pi_2(s), \pi_2(d), u) $$

Every two arrows with the same source has a pair.

$$ \mathrm{src}(a) = \mathrm{src}(b) \implies \exists s: S \mathop. \pi_1(s) = a \land \pi_2(s) = b $$

Every two arrows with the same destination has a pair.

$$ \mathrm{dst}(a) = \mathrm{dst}(b) \implies \exists d : D \mathop. \pi_1(d) = a \land \pi_2(d) = b $$

Cartesian closure (Products)

The product is only defined up to unique isomorphism, but the function symbol $t$ picks out a specific product in an arbitrary fashion. Here is a source with rules for products.

The product of a pair of arrows has the same destinations as the original pair of arrows.

$$ \mathrm{dst}(\pi_1(t(s))) = \mathrm{dst}(\pi_1(s) \land \mathrm{dst}(\pi_2(t(s)) = \mathrm{dst}(\pi_2(s)) $$

The product has a unique arrow making the diagram commute.

$$ \exists! f \mathop. R(f, \pi_1(t(s)), \pi_1(s)) \land R(f, \pi_2(t(s)), \pi_2(s)) $$

Define the product of two objects $w$.

$$ (\exists s' : S \mathop. s = t(s')) \to w(\mathrm{src}(\pi_1(s)), \mathrm{src}(\pi_2(s))) = \mathrm{src}(\pi_1(s)) $$

The product always exists.

$$ w(a, b) = z \to (\exists s : S \mathop. \mathrm{src}(\pi_1(s)) = z) $$

Cartesian closure (terminal object)

An object has a unique arrow from every other object to itself if and only if it is equivalent to the designated terminal object up to unique isomorphism. $1$ is a constant symbol, so it picks out a specific object.

$$ (\forall x \mathop. \exists! f \mathop. \mathrm{src}(f) = x \land \mathrm{dst}(f) = a) \iff I(1, a) $$

Cartesian closure (exponential objects)

An exponential object, according to Wikipedia consists of an object and an arrow. Let $e(y, z)$ correspond to $Z^Y$ in the traditional notation. Let $v(z, y)$ be the corresponding evaluation map.

Fix the destination of the evaluation map.

$$ \mathrm{dst}(v(y, z)) = z $$

Fix the source of the evaluation map.

$$ \mathrm{src}(v(y, z)) = w(e(z, y), y) $$

For any arrow $g : x \times y \to z$, there's a unique arrow that makes the diagram commute.

$$ \mathrm{src}(g) = w(x, y) \land \mathrm{dst}(g) = z \implies (\exists! u \mathop. R(u, v(y, z), g)) $$

Finite Limits (existence of pullbacks)

A pullback produces a commutative diagram. Here is a source for pullbacks.

$$ Q(p(d), d) $$

This is an encoding of the universal property of a pullback.

$$ Q(s, d) \implies (\exists! u \mathop. R(u, \pi_1(s), \pi_1(p(d))) \land R(u, \pi_2(s), \pi_2(p(d)))) $$

Subobject classifier

The left arguments of $J$ are exactly the monomorphisms.

$$ M(a) \iff \exists b \mathop. J(a, b) $$

The right argument of $J$ exists and is uniquely determined by the left argument.

$$ \forall x \mathop. M(x) \to \exists! y \mathop. J(x, y) $$

I'm following this article for the definition of a subobject classifier because it makes the order of quantification clear.

The $\mathsf{true}$ is a monomorphism.

$$M(\tau)$$

The source of $\tau$ is the terminal object.

$$ \mathrm{src}(\tau) = 1 $$

The destination of $\tau$ is $\Omega$.

$$ \mathrm{dst}(\tau) = \Omega $$

$J$ gives us a unique morphism giving us a pullback.

$$ \forall a : A \mathop. M(a) \to \exists! u : A \mathop. \mathrm{dst}(u) = \Omega \land (\exists b \mathop. R(a, u, b)) \land (\exists s \exists d \mathop. \pi_1(d) = u \land \pi_2(d) = \tau \land s = p(d) \land \pi_1(s) = a) \land J(\pi_1(s), \pi_1(d)) $$

Solution 1:

Consider the following logic:

There is a sort $Obj$.

For each $a, b : Obj$, there is a sort $Hom(a, b)$ (also written $a \to b$).

Terms consist of:

1. Variables (each of which has a sort)
2. Given terms $f : Hom(a, b)$ and $g : Hom(b, c)$, there is a term $g \circ f : Hom(a, c)$.
3. For each $a : Obj$, there is a term $1_A : Hom(a, a)$.

The only atomic formulas are $f = g$ where $f, g : Hom(a, b)$.

Formulas are closed under the usual propositional operators (eg $\land$, $\lor$, etc) and also under universal/existential quantification over a given sort (eg $\forall f : Hom(a, b), \phi(f)$). When we universally quantify over multiple variables of the same type, we often shorten $\forall f : T \forall g : T (\phi(f, g))$ to $\forall f, g : T (\phi(f, g))$ (and the same for existential quantifiers).

The axioms for a category are as follows:

1. $\forall x, y \in Obj \forall f : Hom(x, y) (f = f \circ 1_x)$
2. $\forall x, y \in Obj \forall f : Hom(x, y) (f = 1_y \circ f)$
3. $\forall w, x, y, z \in Obj \forall f : Hom(w, x) \forall g : Hom(x, y) \forall h : Hom(y, z) (f \circ (g \circ h) = (f \circ g) \circ h)$

Note that $\exists! x : Hom(k, \ell) \phi(x)$ is shorthand for $\exists x (\phi(x) \land \forall y : Hom(k, \ell) (\phi(y) \implies y = x)$.

Given an object $x$, we define $isTerminal(x)$ to be shorthand for $\forall y \in Obj \exists! f : Hom(y, x) (f = f)$.

Given objects $p, x, y, z$ and arrows $p_0 : Hom(p, x)$, $p_1 : Hom(p, y)$, $f : Hom(x, z)$, $g: Hom(y, z)$, we define $isPullback(p, x, y, z, p_0, p_1, f, g)$ as shorthand for the statement $f \circ p_0 = g \circ p_1 \land \forall k \in Obj \forall k_0 : Hom(k, x) \forall k_1 : Hom(k, y) (f \circ k_0 = g \circ k_1 \implies \exists! h : Hom(k, p) (p_0 \circ h = k_0 \land p_1 \circ h = k_1)$.

The axioms for finite limits are as follows:

4. $\exists x \in Obj (isTerminal(x))$ [terminal object]
5. $\forall x, y, z \in Obj \forall f : Hom(x, z) \forall g : Hom(y, z) \exists p : Obj \exists p_0 : Hom(p, x) \exists p_1 : Hom(p, y) (isPullback(p, x, y, z, p_0, p_1, f, g))$ [pullbacks]

Given a term $f : Hom(x, y)$, we define $monic(f)$ to be shorthand for $\forall w : Obj \forall g, h : Hom(w, x) (f \circ g = f \circ h \implies g = h)$. The axiom for subobject classifiers is

6. $\exists x, \Omega : Obj (isTerminal(x) \land \exists \top : Hom(x, \Omega) \forall y : Obj \forall z : Obj \forall f : Hom(z, y) (isMonic(f) \implies \exists! \chi : Hom(y, \Omega) \exists u : Hom(z, x) (isPullback(z, x, y, \Omega, u, f, \top, \chi)))$

Finally, Cartesian closure. Given objects $p, x, y$ and maps $p_0 : Hom(p, x)$, $p_1 : Hom(p, y)$, we define $isProduct(p, x, y, p_0, p_1)$ in the obvious way (left to the reader). Then the axiom for Cartesian Closure is

7. $\forall x, y : Obj \exists E : Obj \exists p_{E, y} : Obj \exists p_0 : Hom(p_{E, y}, E) \exists p_1 : Hom(p_{E, y}, y) (isProduct(p_{E, y}, E, y, p_0, p_1) \land \exists eval : Hom(P_{E, y}, x) \forall z : Obj \exists P_{z, y} \exists \pi_0 : Hom(P_{z, y}, z) \exists \pi_1 : Hom(P_{z, y}, y) (isProduct(P_{z, y}, z, y, \pi_0, \pi_1) \land \forall f : Hom(P_{z, y}, x) \exists! g : Hom(z, E) \exists m : Hom(P_{z, y}, P_{E, y}) (p_0 \circ m = g \circ \pi_0 \land p_1 \circ m = \pi_1 \land eval \circ m = f)))$

There you have it.

There are some nice theorems about this axiomatization of a topos. First, it captures exactly the properties about categories which are isomorphism- and equivalence-invariant (equivalence in the sense of a fully faithful essentially surjective functor). Second, it has some level of "type-checking" inherent in the theory - there's no need to have propositions involving the domains and codomains of arrows lining up, for example.

Solution 2:

My approach tends to use more explicit names for operations and objects as opposed to asserting existence of objects which then must be made suitably unique based on axioms. This aligns better in my opinion with usual mathematical practice.

Category

We start with a sort $\operatorname{Obj}$ -- or, if the topos is called $\mathcal{E}$, we might accept a minor abuse of notation in using $\mathcal{E}$ instead of $\operatorname{Obj}$. Then, for each $X, Y \in \operatorname{Obj}$, we also have a sort $\operatorname{Hom}(X, Y)$. We also have a composition operator $\circ$ which for each $X, Y, Z \in \operatorname{Obj}$ gives a map $\operatorname{Hom}(Y, Z) \times \operatorname{Hom}(X, Y) \to \operatorname{Hom}(X, Z)$; along with an identity operator which for each $X \in \operatorname{Obj}$ gives an element of $\operatorname{Hom}(X, X)$. The axioms are then the usual ones.

Finite limits

First, for products, we define a product operation $\times : \operatorname{Obj} \times \operatorname{Obj} \to \operatorname{Obj}$. We also define projection operators $(\pi_1)_{X,Y} \in \operatorname{Hom}(X \times Y, X)$ and $(\pi_2)_{X,Y} \in \operatorname{Hom}(X \times Y, Y)$ (or if it's clear, simply $\pi_1$ and $\pi_2$), along with a pair map operator $(-, -) : \operatorname{Hom}(U, X) \times \operatorname{Hom}(U, Y) \to \operatorname{Hom}(U, X \times Y)$. The axioms would be:

• $\pi_1 \circ (f, g) = f$.
• $\pi_2 \circ (f, g) = g$.
• $f = (\pi_1 \circ f, \pi_2 \circ f)$ for all $f \in \operatorname{Hom}(U, X \times Y)$.

Similarly, for the final object, we define an object (or nullary operation) $1 \in \operatorname{Obj}$, along with a morphism $()_U \in \operatorname{Hom}(U, 1)$ for each $U \in \operatorname{Obj}$. The axiom here would simply be that for all $f \in \operatorname{Hom}(U, 1)$, we have $f = ()_U$.

Finally, for equalizers, we define an operation $\operatorname{eq} : (\operatorname{Hom}(X, Y))^2 \to \operatorname{Obj}$ for each $X, Y \in \operatorname{Obj}$. We also have a morphism $\operatorname{eqinc}_{f,g} \in \operatorname{Hom}(\operatorname{eq}(f, g), X)$, along with an operator $\operatorname{eqfactor}_{f,g} : \{ x \in \operatorname{Hom}(U, X) \mid f \circ x = g \circ x \} \to \operatorname{Hom}(U, \operatorname{eq}(f, g))$. The axioms here would be:

• $f \circ \operatorname{eqinc}_{f,g} = g \circ \operatorname{eqinc}_{f,g}$.
• Whenever $f \circ x = g \circ x$, then $x = \operatorname{eqinc}_{f,g} \circ \operatorname{eqfactor}_{f,g}(x)$.
• For any morphism $x \in \operatorname{Hom}(U, \operatorname{eq}(f, g))$, we have $\operatorname{eqfactor}_{f,g}(\operatorname{eqinc}_{f,g} \circ x) = x$.

Cartesian closed

Similarly, we will define an operator ${\multimap} : \operatorname{Obj}^2 \to \operatorname{Obj}$. We will also have morphisms $\operatorname{ev}_{X,Y} \in \operatorname{Hom}((X \multimap Y) \times X, Y)$ and an "abstraction" operator $\operatorname{abs}_{U,X,Y} : \operatorname{Hom}(U \times X, Y) \to \operatorname{Hom}(U, X \multimap Y)$. The axioms would include:

• For $f \in \operatorname{Hom}(U, X)$ and $g \in \operatorname{Hom}(U \times X, Y)$, $\operatorname{ev} \circ (\operatorname{abs}(g), f) = g \circ (\operatorname{id}, f)$.
• $\operatorname{abs}(\operatorname{ev}_{X,Y}) = \operatorname{id}_{X \multimap Y}$.
• For $\varphi \in \operatorname{Hom}(V, U)$, $f \in \operatorname{Hom}(U \times X, Y)$, we have $\operatorname{abs}(f \circ (\varphi \circ \pi_1, \pi_2)) = \operatorname{abs}(f) \circ \varphi$.

Subobject classifier

We finally suppose we have a given object $\Omega \in \operatorname{Obj}$. To use this, we define an operation such that whenever $f \in \operatorname{Hom}(X', X)$ is monic, we have a corresponding "characteristic function" morphism $\chi_f \in \operatorname{Hom}(X, \Omega)$. (Or, as usual, if $X'$ is viewed as a subobject with $f$ being a canonical inclusion, we can also write $\chi_{X'}$.) The inverse would be a "comprehension subset object" operation $\Sigma : \operatorname{Hom}(X, \Omega) \to \operatorname{Obj}$ along with a canonical inclusion map $\operatorname{inc}_{\Sigma} \in \operatorname{Hom}(\Sigma(\varphi), X)$; and we also give a pair of inverse isomorphisms between $\Sigma(\chi_f)$ and $X'$ for each monomorphism $f \in \operatorname{Hom}(X', X)$. (More loosely, in place of $\Sigma(\varphi)$ we can write $\{ x \in X \mid \varphi(x) \}$ understanding this to be purely notational.) Similarly, letting $\operatorname{true} \in \operatorname{Hom}(1, \Omega)$ be shorthand for $\chi_{\operatorname{id}_1}$, we need an operator such that whenever $x \in \operatorname{Hom}(U, X)$ satisfies $\chi_f \circ x = \operatorname{true} \circ ()_U$, we get a factorization of $x$ through $f$. Axioms would include the requirement that $\chi_{\Sigma(\varphi)} = \varphi$; functoriality of $\chi$ with respect to subobject pullbacks; the statement that $\operatorname{inc}_{\Sigma}(\varphi)$ is a monomorphism; the statement that the isomorphisms mentioned above are inverses and form commutative diagrams with $f$; and the statement that the distinguished factorization map mentioned above does indeed function as a factorization.

(Note that the description of equalizers given above could be considered mostly redundant if we're expecting to be working in a topos anyway. Instead, we could define equality morphism ${=}_X \in \operatorname{Hom}(X \times X, \Omega)$ as the characteristic morphism of the diagonal subobject $(\operatorname{id}, \operatorname{id}) \in \operatorname{Hom}(X, X \times X)$; and then we have $\operatorname{eq}(f, g)$ canonically isomorphic to $\Sigma({=}_Y \circ (f, g))$.)