Syntactic category of a geometric theory has finite limits.

Question

Let $T$ be a geometric theory. Consider the syntactic category $C_T$. I want to show that $C_T$ has all finite limits. To show this, it is enough to show that it has finite products and equalizers. There is a proof for this statement in “Sketches of an Elephant”, D1.4, Lemma 1.4.3, p. 842, but I can not understand it well. I need to see more details to understand it.

Answer 1

I will do here the proof of $[[]:\top]$ being the terminal object in $\mathcal{C}_{\mathbb{T}}$ to exemplify what kind of techniques one uses to prove such statements in syntactic categories and at the end I will link a couple of places where you can consult the proofs (or at least part of them) for the case of binary products and equalizers.

Throughout, I'm going to use the same notation as Johnstone does in Sketches of an Elephant (Elephant for short), and whenever I mention some page it will be a reference to this book. Moreover, I will write $\mathbb{T}, \phi \vdash_{\overline{x}} \psi$ to denote that the sequent-in-context $\phi \vdash_{\overline{x}} \psi$ is provable modulo $\mathbb{T}$.

Before starting the proof I also want to recall the important definition of a $\mathbb{T}$-provably functional formula; the properties that characterize such formula are given at the end of page 841 in Elephant, yet Johnstone gives the definition as such in the second paragraph of page 842. Note that the (equivalence classes of) $\mathbb{T}$-provably functional formulas $\gamma$ are precisely the arrows in $\mathcal{C}_{\mathbb{T}}$, and they express at the syntactic level that $\gamma$ is the graph of a function.

Definition: An arrow $[\overline{x} : \phi] \rightarrow [\overline{y} : \psi]$ in $\mathcal{C}_{\mathbb{T}}$ is given by the equivalence class of a $\mathbb{T}$-provably functional formula $\gamma(\overline{x}, \overline{y})$, i.e. a formula such that:

1. $\mathbb{T}, \gamma(\overline{x}, \overline{y}) \vdash_{\overline{x}, \overline{y}} \phi(\overline{x}) \wedge \psi(\overline{y})$.
2. $\mathbb{T}, \phi(\overline{x}) \vdash_{\overline{x}} \exists\overline{y}(\gamma(\overline{x}, \overline{y}))$.
3. $\mathbb{T}, \gamma(\overline{x}, \overline{y_1}) \wedge \gamma(\overline{x}, \overline{y_2}) \vdash_{\overline{x}, \overline{y_1}, \overline{y_2}} \overline{y_1 }= \overline{y_2}$.

Note that to show that $\mathcal{C}_{\mathbb{T}}$ has finite products it suffices to show that it has $0$-ary products and binary products; note that a $0$-ary (or empty) product is just the terminal object in a category. This latter fact is shown here, for example.

The terminal object is $[[]:\top]$.

Proof: Let $[ \overline{x}: \phi]$ be any object in $\mathcal{C}_{\mathbb{T}}$. Note that we have indeed an arrow $[ \overline{x}: \phi] \rightarrow [[] : \top ]$, namely $[(\overline{x}, \emptyset) : \phi(\overline{x}) ]$. Of course one needs to check that $[(\overline{x}, \emptyset) : \phi(\overline{x}) ]$ is in $\mathcal{C}_{\mathbb{T}}$ (i.e that $\phi(\overline{x})$ is a $\mathbb{T}$-provably functional formula), but this is straightforward using the fact that $[ \overline{x}: \phi]$ is an object in $\mathcal{C}_{\mathbb{T}}$.

Let now $[ \gamma], [ \gamma' ] : [ \overline{x} : \phi ] \rightrightarrows [ [] : \top]$ be two arrows in $\mathcal{C}_{\mathbb{T}}$. As $\gamma$ and $\gamma'$ are provably functional, we have that $\mathbb{T}, \gamma(\overline{x}) \vdash_{\overline{x}} \phi(\overline{x})$ (by property $1$ of $\gamma$) and $\mathbb{T}, \phi(\overline{x}) \vdash_{\overline{x}} \exists \emptyset \gamma'(\overline{x})$ (by property $2$ of $\gamma'$). Note that existential quantification over an empty set of variables is a vacuous statement, so the latter gives us $\mathbb{T}, \phi(\overline{x}) \vdash_{\overline{x}} \gamma'(\overline{x})$, and by the Cut Rule (see page 830) we thus have $\mathbb{T}, \gamma(\overline{x}) \vdash_{\overline{x}} \gamma'(\overline{x})$.

A similar argument shows that $\mathbb{T}, \gamma'(\overline{x}) \vdash_{\overline{x}} \gamma(\overline{x})$, so $\gamma$ and $\gamma'$ are provably equivalent over $\mathbb{T}$ and therefore for any object $[ \overline{x}: \phi]$ there exists a unique arrow $[ \overline{x}: \phi] \rightarrow [[] : \top ]$; hence $[[] : \top ]$ is the terminal object in $\mathcal{C}_{\mathbb{T}}$.

---

You can consult these lecture notes (page 26) for the almost complete proof of binary products; in there $\mathcal{R}(T)$ is our $\mathcal{C}_{\mathbb{T}}$, but $T$ is a regular theory instead of geometric. This is not a problem beacuse any regular theory is by definition also geometric, so the proof presented there also works for our case.

You can consult Mark Kamsma's personal webpage (Lemma 5.2.1 of his Master thesis: Classifying Topoi and Model Theory) for the proof of equalizers; in there, Syn$^g_{\kappa}(T)$ is our $\mathcal{C}_{\mathbb{T}}$, but we works in the more general case, since his theory $T$ is a $\kappa$-geometric theory, for $\kappa$ a regular cardinal. This is not a problem again since Syn$^g_{\aleph_0}(T)$ is precisely $\mathcal{C}_{\mathbb{T}}$. In fact, he shows that Syn$^g_{\kappa}(T)$ has finite limits and more, but the proof for binary products is not as detailed as in the lecture notes linked above.

In conclusion, the main idea to prove such statements in syntactic categories is to use the properties of $\mathbb{T}$-provably functional formulas and the axioms and inference rules of your proof system. As Johnstone said in the end of proof of Lemma 1.4.2, this work is tedious as it requires manipulations within your deductive system, and not too many people are trained to be proficient at this (compared, say, to the usual diagram chasing arguments).