Fix a relational language $\mathcal{L}$. (I don't think relational really matters that much but I don't want to worry about it.) A topological $\mathcal{L}$-structure is an $\mathcal{L}$-structure $M$ together with a topology $\tau$ on $M$ such that for every relation symbol $R \in \mathcal{L}$ (including equality), $R^{M}$ is closed as a subset of $M^n$ (where $n$ is the arity of $R$). Note that since the diagonal is closed in $M^2$, a topological $\mathcal{L}$-structure is automatically Hausdorff. For any topological property $P$ (such as compact or second countable), a topological $\mathcal{L}$-structure is $P$ if the underlying topological space is $P$.
For any $\mathcal{L}$-structure $M$ and any $\mathcal{L}$-formula $\varphi(\bar{x})$ with a designated tuple of variables $\bar{x}$ such that the free variables of $\varphi$ are contained in $\bar{x}$, let $\varphi(M)$ be the subset of $M^n$ of tuples $\bar{a}$ such that $M \models \varphi(\bar{a})$, where $n = |\bar{x}|$.
Let $T$ be the set of $\mathcal{L}$-sentences true in every compact $\mathcal{L}$-structure. $T$ is certainly non-trivial (for non-trivial $\mathcal{L}$). For instance, if $\mathcal{L}$ contains a binary relational symbol $\leq$, then $T$ contains a sentence that says that if $\leq$ is a linear order then there is a greatest element.
For lack of a better term, call an $\mathcal{L}$-formula $\varphi(\bar{x})$ closed if for every compact $\mathcal{L}$-structure $M$, $\varphi(M)$ is a closed subset of $M^n$. Broadly my question is about syntactic characterization of closed formulas, but before we can even talk about that there's a deeper issue.
Question 1. For a fixed language $\mathcal{L}$, are $T$ and the collection of closed $\mathcal{L}$-formulas set theoretically absolute? What if we change the definition of $T$ and closed formula to restrict attention to second countable compact $\mathcal{L}$-structures?
If they aren't then I'm not very hopeful for a syntactic characterization. There are a few easy facts about the collection of closed $\mathcal{L}$-formulas:
- Any $\mathcal{L}$-sentence is closed.
- Any positive atomic formula is closed.
- Any positive Boolean combination of closed formulas is closed.
- Any variable substitution of a closed formula is closed (i.e. if $\varphi(x,y)$ is closed, then $\varphi(x,x)$ is closed).
- If $\varphi$ is closed, then $\exists x \varphi(x)$ is closed (this uses the fact that the structures are compact, so the projection maps are closed).
- If $\varphi$ is closed, then $\forall x \varphi(x)$ is closed (this uses the fact that the projection maps are open).
Another subtler operation under which closed formulas are closed is special relative universal quantification.
- If $\varphi$ is closed and $\psi$ is arbitrary, but has $x$ as its only free variable, then $\forall x (\psi \rightarrow \varphi)$ is closed. (EDIT: I realized you don't even need $\psi$ to be closed for this.)
This last operation is part of the definition of generalized positive formulas, which are relevant to positive set theory. A hopeful guess as to a syntactic characterization is the following.
Question 2. Is every closed $\mathcal{L}$-formula logically equivalent over $T$ to one of the form $\bigvee_{i<n} \varphi_i \wedge \psi_i$, where each $\varphi_i$ is a sentence and each $\psi_i$ is a generalized positive formula? Again, what if we restrict attention to second countable structures?
Where the generalized positive formulas are the smallest class of formulas containing $\bot$, $\top$, and the positive atomic formulas and closed under positive Boolean combination, existential quantification, and the formation of formulas of the form $\forall x (\psi \rightarrow \varphi)$, where $\psi$ is arbitrary and has at most $x$ free and $\varphi$ is generalized positive.
