For a language $\tau$, let a topological $\tau$-model be a connected Hausdorff topological space $X$ equipped with a $\tau$-structure $\mathcal{M}$ on the set of points of $X$ such that:
- For any $n$-ary relation symbol $R$, $R^\mathcal{M}$ is a closed subset of $X^n$
- For any $n$-ary function symbol $f$, $f^\mathcal{M}$ : $X^n\rightarrow X$ is continuous
Note that, by the Hausdorff condition, equality (the diagonal) is a closed subset of $X^2$ and so we may add it to our topological theories as we like. Also note that this is a generalization of topological algebras.
This question is about the semantics for second-order logic arising when predicate symbols are interpreted as open subsets. For example, consider the following axiom:
"For any nonequal points $x$ and $y$ there exist open sets $U$, $V$, $U'$, and $V'$, such that $x$ is in $U$, $y$ is in $V$, no point in $U$ is in $U'$, no point in $V$ is in $V'$, and no point is in both $U$ and $V$."
A topological model satisfies the above axiom if and only if it is Urysohn.
To be more precise:
- The sentences of the logic are precisely the second-order sentences.
- If $\varphi$ is $P(x)$ for a predicate $P$, then for a topological model $X$, you have $X\models\varphi[U, x]$ iff $U$ is an open set and $x\in U$
- $\land$, $\neg$, and first order quantifiers behave exactly as they do in first-order logic, via the underlying structure $\mathcal{M}$
- If $\varphi$ is $\exists P(\psi(P, x_1...x_n))$ then $X\models\varphi(x_1...x_n)$ iff there is some open set $U$ such that $X\models\psi[U, x_1...x_n]$.
Does this logic satisfy the compactness theorem?
The above logic is a lot tamer than full second-order logic; in fact, you can think of any theory in the logic as being a theory in Henkin semantics with 2 more axioms in first-order logic (stating that the empty set is an open set and that the intersection of open sets is again open), as well as a third-order axiom stating that the union of any collection of open sets is again open. Due to this third-order axiom though, it's not immediately clear whether or not this logic is compact.
The main problem with this interpretation is that I'm not sure there's any way to state that a relation is closed in $X^n$, or that a function from $X^n$ to $X$ is continuous, when $n>1$. These reasons only serve to obfuscate this logic even more.
A friend proposed to me that a modified form of the ultraproduct argument could be applied here, where "$\{i : x_i = y_i\}$ is in the filter" was replaced with "For every basic open $U$ in $X$ containing $[x_i]$, $\{i : b_i\in U_i\}$ is in the filter" but we found an issue in this argument that made it unusable.
We both are under the impression that this logic may be compact, but are unable to prove it. How should we go about doing this?
Bonus questions!
- Does this logic satisfy any analogues to the Lowenheim-Skolem theorem?
- What model-theoretic properties does this logic have?
- Can you find a complete, effective deductive system for this logic?