This question is inspired by this Mathoverflow question.
Ignoring size issues, there is a natural way to view a category as a first-order structure in a finite language. In light of this we can ask about the computational complexity of the first-order theory of a given category. Note that a lot of important structure is lost when passing to the first-order level; nevertheless, it still seems interesting to me.
Plenty of categories are easily checked to have very complicated first-order theories – for example, assuming the axiom of choice in the background we can identify the finite sets as those for which every self-injection is a surjection, and since Cartesian products and disjoint unions give the usual arithmetic we have that the first-order theory of the category Sets is not computable.
Incidentally, choice isn't needed here, but the non-choice argument is a bit more tedious.
My question is:
Is the first-order theory of the category Top of topological spaces (with morphisms being continuous maps) computable?
My suspicion is that the answer is no. An obvious way to prove this would be to show that the finite discrete spaces are first-order characterizable here, since then we could run the same argument as for Sets; however, I don't see how to do this. (In particular, the notion of "compact objcet" of a category is not obviously first-order expressible, so that characterization of finite discrete spaces doesn't seem to help.)
There are weaker versions of this question which could be asked:
-
We could focus on the theory of the categorial equivalence class of Top – that is, the set of sentences true in every category which is categorially equivalent to Top. In general categorial equivalence does not imply elementary equivalence (since a two-element category can be categorially equivalent to a one-element category), so this is a nontrivial weakening.
-
We could also restrict attention to a subcollection of categories – that is, pin down some non-first-order categorial property $P$ of Top, and then ask for a first-order theory which distinguishes the theory of Top (or the theory of the categorial equivalence class of Top) within this class. For example, Lawvere's ETCS characterizes Sets up to categorial equivalence amongst the locally small complete categories.
I am also interested in comments along these lines; however, my main question is specifically about the first-order theory of Top.
EDIT: David Roberts brought to my attention Schlomiuk's paper An elementary theory of the category of topological spaces; among other things, this gives a computable (indeed, finite) theory characterizing Top up to categorial equivalence amongst complete categories, as well as in a more subtle sense (any such category is equivalent to Top$^\mathfrak{S}$ for some model $\mathfrak{S}$ of ETCS).
Best Answer
Let me assume choice. It is possible to distinguish discrete spaces from other spaces: those are precisely the spaces $X$ such that for any epimorphism $f:Y\to X$ admits a section $g:X\to Y$ (i.e. $g\circ f=\mathrm{id}_Y$). To see this, recall first that epimorphisms in Top are just the surjective continuous maps.
If $X$ is discrete, then for any epimorphism $Y\to X$ there is a set-theoretical section by AC, which is automatically continuous.
Conversely, suppose every epimorphism into $X$ splits. Let $Y$ have the same underlying space as $X$, but discrete topology. Then the identity on points is a continuous map from $Y\to X$, and since it's an epimorphism, it admits a section, which shows that $X$ is discrete too.
The subcategory of discrete topological spaces is equivalent to the category of sets, and you already know it's uncomputable. It follows the first-order theory of Top is undecidable.
It's not clear to me if this proof can be modified so as to avoid the use of AC.
Edit: a proof without the use of AC: we will again distinguish the subcategory of discrete spaces. Let $1$ be a one-point space (a terminal object) and $2$ a two-point discrete space (a space with exactly two maps from $1$ to it, and with $4$ maps from it to itself) and $i:1\to 2$ any map. Then $X$ is discrete iff for any map $f:1\to X$ there is a map $g:X\to 2$ such that $g\circ f=i$, and for any $f':1\to X,f'\neq f$, we have $g\circ f'\neq i$.
This expresses that for any point $x\in X$, there is a map $X\to 2$ which takes $x$ to one point, and all other points to a different one. Since $2$ was discrete, this implies $\{x\}$ is open, so $X$ is discrete.
Since you say you know Set has uncomputable theory even without AC, we deduce the same for Top.