Do topological semantics of SOL satisfy the compactness theorem? 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?

 A: Unless I'm misunderstanding this, this is in fact as complicated as standard second-order logic.

First, as a warm-up let's look at the not-necessarily-connected version.
Consider the sentence $$(*):\quad \forall x\exists U\forall y(y\in U\leftrightarrow y=x).$$ The topological models of $(*)$ are precisely the topological structures whose topology is discrete. The map sending a standard structure $\mathcal{M}$ to the topological structure gotten by slapping the discrete topology onto $\mathcal{M}$ then appropriately embeds standard second-order logic into not-necessarily-connected topological second-order logic.
This embedding in turn means that all the usual pathologies of second-order logic - the failures of compactness, Lowenheim-Skolem, computable enumerability for validity, and set-theoretic absoluteness - carry over to this topological second-order logic.

OK, now what about the connectedness requirement?
Well, the "slap on the discrete topology" idea no longer works, but the broader intuition is still valuable. We'll find a way to associate to each standard structure $\mathcal{M}$ a connected topological structure $\hat{\mathcal{M}}$ in some "information-preserving" way, and then argue that this gives rise to the desired embedding. One step of this will be to show that the set of topological structures associated to classical structures in the manner above is actually definable; in the not-necessarily-connected version, this was accomplished by $(*)$.
Here's a sketch of one approach which works. Suppose for simplicity our language consists of a single binary function symbol. Given a structure $\mathcal{M}=(M, f)$, consider the "$\mathcal{M}$-octopus:"

*

*First, we consider the following function on $M\times[0,1]$: $$\hat{f}((m,i),(n,j))=(f(m,n), \min\{i,j\}).$$


*Next, consider the equivalence relation $\sim$ on $M\times[0,1]$ given by $(a,i)\sim (b,j)$ iff $(a,i)=(b,j)$ or $i=j=0$. Note that $\hat{f}$ respects $\sim$, so we get an induced $\underline{f}:(M\times[0,1]/\sim)^2\rightarrow(M\times[0,1]/\sim)$.


*Finally, equip $M$ with the discrete topology and $[0,1]$ with the usual topology, and $M\times[0,1]/\sim$ with the induced topology. Let $\hat{\mathcal{M}}$ be the topological structure in the same language as $\mathcal{M}$ with underlying space $M\times[0,1]/\sim$  and the binary function symbol interpreted as $\underline{f}$.
The set of topological structures isomorphic in the appropriate sense to some $\hat{\mathcal{M}}$ is indeed definable via a topological second-order sentence, although this is a bit tedious. Meanwhile, we can locate $\mathcal{M}$ inside $\hat{\mathcal{M}}$ in a precise way: consider the non-cut points of $\hat{\mathcal{M}}$. So the resulting translation is to send $\varphi$ to "the structure is an octopus and $\varphi$ holds with all element-quantifiers relativized to the non-cut-points."
So again, we wind up with the full terribleness of standard second-order logic.

Actually, I think the really valuable idea along these lines is to look at a specific topological space. E.g. what happens when we demand that our structure be built on $\mathbb{R}$ with the usual topology?
It turns out that even for equational first-order logic things get quite complicated; see e.g. this paper by Taylor. To be honest, I think that no reasonably rich space will yield a second-order logic which is compact or has a good deductive system, and Lowenheim-Skolem is of course dead on arrival. A certain amount of set-theoretic absoluteness, however, will hold for some spaces under appropriate set-theoretic assumptions like large cardinals - specifically, for spaces like $\mathbb{R}$, large cardinals will ensure that the corresponding logic is forcing-invariant.
