topologic view on FO
Is there a topology related or that even captures FO, s.t. properties of FO corresponds to properties of that topology?
In first-order logic there are the set of variables (that is considered as countable for whatever reason), terms, formulas, structures etc. Although that is said in metalanguage, is it possible to define naturally over these "sets" topologic structures? This is related to algebraic stuctures over metaconcepts in FO.
There are a few topological spaces which play a crucial role in the study of first-order logic. A couple key phrases include "logic topology" and "type spaces."
Most obviously, suppose we have a language $\Sigma$ and a collection $\mathfrak{S}$ of $\Sigma$-structures. Then there is a natural logic topology $\tau_{log}^\mathfrak{S}$ on $\mathfrak{S}$, namely that generated by sets of the form $\{\mathcal{A}\in\mathfrak{S}:\mathcal{A}\models\varphi\}$ for $\varphi$ a sentence in the language $\Sigma$. Facts about first-order logic often translate to topological facts about spaces of the form $(\mathfrak{S},\tau_{log}^\mathfrak{S})$. For example:
-
In general $\tau_{log}^\mathfrak{S}$ is not $T_0$, even if $\mathfrak{S}$ contains at most one structure of each isomorphism type, since we can have non-isomorphic structures which are elementarily equivalent.
-
On the other hand, the $T_0$ification of $\tau_{log}^\mathfrak{S}$ (really, a space of complete theories) is Hausdorff (since first-order logic is closed under negation).
-
The compactness theorem says that each $\tau_{log}^\mathfrak{S}$ is compact.
-
The downwards Lowenheim-Skolem theorem says that we can essentially restrict attention to countable structures (when $\Sigma$ is countable; structures of cardinality $\le\vert\Sigma\vert+\aleph_0$ more generally); in particular, while the collection of all $\Sigma$-structures is a proper class, this means that we can see all the topological data (up to $T_0$ification) by looking at a set of structures.
-
Lindstrom's theorem meanwhile can be phrased as a statement about how the various topological spaces interact. We restrict attention here to finite languages, and for each finite language $\Sigma$ let $X_\Sigma$ be the set of $\Sigma$-structures with domain $\subseteq\mathbb{N}$, and $\tau_{log}^{X_\Sigma}$ the logic topology on $X_\Sigma$ as above. There is a family $\mathbb{M}$ of maps between the $\mathcal{X}_\Sigma$s, corresponding to reduction and relativization, and these maps are continuous (this is a condition of being a regular logic). Lindstrom's theorem then says there is no family $\{\sigma_\Sigma:\Sigma$ a finite language$\}$ with $\sigma_\Sigma$ a topology on $X_\Sigma$ at least as fine as $\tau_{log}^{X_\Sigma}$, at least one of which is strictly finer than $\tau_{log}^{X_\Sigma}$, and with respect to which all the maps in $\mathbb{M}$ remain continuous. As far as I know this rephrasing isn't useful for proving Lindstrom's theorem, but it's neat to note that it has a purely topological meaning.
- EDIT: see Xavier Caicedo's Lindstrom's theorem for positive logics, a topological view for more on this theme. (The link in my comment below is broken now.)
-
Interestingly, motivated by this we can interpret the classical fact "No proper refinement of a compact Hausdorff topology is compact" as a kind of Lindstrom theorem for propositional logic.
And the logic topology is also interesting outside of the "pure" study of FOL - e.g. it plays an important role in descriptive set theory.
We can also assign topological spaces to theories; these are closely related to the spaces described above.
For a (complete, for niceness) theory $T$ and an $n\in\mathbb{N}$, an $n$-type over $T$ is a set $p$ of formulas in free variables $x_1,...,x_n$ such that $p\cup T$ is consistent and $p$ is maximal such. The set of all $n$-types over $T$, denoted "$S_n(T)$," has a natural topology generated by sets of the form $$\{p\in S_n(T): \varphi\in p\}$$ for $\varphi$ a formula. Note the close similarity with the logic topology above.
The type space of a theory is compact, per the compactness theorem, and winds up being an important tool for studying $T$ itself. For example, isolated points in $S_n(T)$ are just principle types.
These spaces are called type spaces.
And this is just a taste of the topic; there is a lot of interaction between topology and logic.