What is a possible language for the Theory of Topological Spaces? 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!
 A: 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:


*

*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$.

*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.

*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.
