This question requires me to write quite a bit of background, so I apologize.
Suppose our domain of discourse is the set of open subsets of a topological space. This means that, by $\forall A$ I mean "for all open sets $A$" and by $\exists A$ I mean "there exists an open set $A$".
Consider the following property: \begin{align} \forall A_1,A_2,\color{red}{[(\exists Y_1:Y_1\subseteq A_1}&\color{red}{{}\land\lnot(Y_1=A_1))\land(\exists Y_2:Y_2\subseteq A_2\land\lnot(Y_2=A_2))]\implies}\\ [\exists X_1,X_2:X_1\ne X_2\land{}( &(A_1\subseteq X_1\land A_1\subseteq X_2\land A_2\subseteq X_1\land A_2\subseteq X_2)\lor{}\\ &(X_1\subseteq A_1\land X_2\subseteq A_1\land X_1\subseteq A_2\land X_2\subseteq A_2))]\\ \end{align} In words: for any two $\color{red}{\text{nonempty}}$ open sets $A_1$ and $A_2$, there are two distinct open sets either containing both or contained in both. For what topological spaces is this valid? Take a moment to consider. Spoiler: It turns out that a topological space satisfies this condition iff the space is connected.
(EDIT: Originally I had forgotten to add in a requirement forcing $A_1$ and $A_2$ to be nonempty. The formula is much less elegant now.)
This is a formula in the first-order theory of posets, applied to the open set poset of a topological space. The first-order theory of posets has only one relation, namely the order (which I denote by $\subseteq$), and has no constants or functions. Every topological space has an associated poset of open sets, ordered by inclusion. I am interested in which properties of topological spaces are first-order expressible in this language.
Here are some other first-order expressible properties:
- $X={\rm all}\quad$ iff $\quad\forall A,X\subseteq A\implies X=A$
- $X=\emptyset\quad$ iff $\quad\forall A,A\subseteq X\implies X=A$
- $X={\rm all}\setminus\overline{\{p\}}$ for some $p\quad$ iff $\quad X\ne{\rm all}\land\forall A,X\subseteq A\implies X=A\lor A={\rm all}$
(Note that for T1 spaces, $\overline{\{p\}}=\{p\}$.) - $X=A\cap B\quad$ iff $\quad X\subseteq A\land X\subseteq B\land(\forall Y,Y\subseteq A\land Y\subseteq B\implies Y\subseteq X)$
- $X=A\cup B\quad$ iff $\quad A\subseteq X\land A\subseteq Y\land(\forall Y,A\subseteq Y\land B\subseteq Y\implies X\subseteq Y)$
- $X$ is connected$\quad$ iff $\quad\lnot\exists A_1,A_2:A_1\ne\emptyset\land A_2\ne\emptyset\land A_1\cap A_2=\emptyset\land A_1\cup A_2=X$
(If you fully expand that out for the special case $X={\rm all}$, then you get the example I led with.)
We cannot talk about points, arbitrary subsets, functions, or families of open sets in this language.
Consider, finally, this property: $$\exists A_1,A_2:A_1,A_2\text{ are connected}\land(A_1\cup A_2={\rm all}\setminus\overline{\{p\}}\text{ for some }p)\land{}\\\lnot(A_1\cap A_2\text{ is connected})$$ In words, there are two connected open sets whose union is everything but a point and whose intersection is disconnected. This is a first-order property because of the formulas I wrote out above. (Technically I am not allowed to quantify over points $p$, but this is OK because it is really shorthand for one of the formulas above.)
I will not prove it, but this property is true of $\Bbb R^2$ and false of $\Bbb R^3$! Take a moment to convince yourself of this. In fact, I believe this should be true of $\Bbb R^2$ but false of $\Bbb R^m$, $m\ne2$. Out of all Euclidean spaces, this formula picks out the plane. I believe I can generalize this to pick out $\Bbb R^n$ for all $n$; that is, for any $n$, I can give you a formula that's true of $\Bbb R^n$ but false of $\Bbb R^m$, $m\ne n$. The only issue is, as far as I can tell, $n$ grows, so does the quantifier rank. The quantifier rank of a formula is the depth of nesting quantifiers. (That very first formula I wrote, about a space being connected, has quantifier rank 4, since the deepest part has the form $\forall\forall\exists\exists$.)
To finally arrive at my question: What's the most efficient way to do this? Specifically: For each $n$, what's the minimal quantifier rank of a first-order formula that's true of $\Bbb R^n$ but false of $\Bbb R^m$, $m\ne n$?
I would also be interested in answers involving other ways to measure simplicity than quantifier rank.