What is a possible language for the Theory of Topological Spaces?

Question

An example of “first-order” language for Group Theory consists in a binary function, a unary function and a costant; a language for Ring Theory has two binary functions, one unary function and two constants. I can continue making examples of languages for Fields, Vector Spaces and so on but I didn’t come up with one for Topological Spaces. Any advice?

Thanks in advance!

Answer 1

Topology is a third-order theory over your space $X$. Specifically because you need to assert not just about sets which are open (that's a second-order statement), but that any union of open sets is open.

You can think about this also as a three-sorted logic: $X$ is the space, $\mathcal T$ is the subsets of $X$ which are relevant, and $\mathcal P$ is the power set of $\mathcal T$. In addition you have a membership relation $\in$, and a partial-operator (which can be thought of as a binary relation when there is an axiom stating that it is functional on its domain) for $\bigcup$.

Now you write basic rudimentary axioms:

1. Cement your types: the three sorts are disjoint, and every object in $\cal T$ is essentially a subset of $X$, and every object of $\mathcal P$ is a subset of $\mathcal T$.

2. Basic set theoretic axioms, like extensionality, and definitions of the unary union is an operator on $\mathcal P$ which returns an object in $\mathcal T$ which is the union of the sets.

3. The axioms of topology!

Of course, this won't truly give you topology, since this is a first-order assertion. And, for example, most interesting topological spaces have uncountable topologies. So having a countable elementary submodel sort of undermines this. You can sort-of get away with second-countable topologies by replacing the topology with a countable basis which is always "enough for most things" when it comes to topological arguments; but you still need to cut out a lot of the space and so on.

Besides, many topological properties are not first-order properties. Simply because they rely on the real numbers (e.g. path connected), and these are not first-order characterizable. So it shouldn't be very surprising that higher-order logic is needed.