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 \to 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. R(g, f, m) \land R(h, f, m) \to g = h $$
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)) $$
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:
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:
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:
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
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
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.