Quantifier complexity of definition of compactness

Question

This question is inspired by the post on quantifier complexity of continuity. We work with metric spaces M considered as two-sorted first-order structures (M,$\mathbb R$,d,+,⋅,<) where $d:M^2→\mathbb R$ is the metric, and +,⋅,< the usual operations and relations on $\mathbb R$.

As is well known, the classical definition of continuity in $\in$-language involves two quantifier alternations. On the other hand, the st-$\in$-language enables a definition of continuity of lower quantifier complexity as follows. Let $\forall^{in},\exists^{in}$ denote quantification over infinitesimals. A standard function $f$ is continuous at a standard point $c$ iff $(\forall^{in} \epsilon) (\exists^{in} \delta) f(c+\epsilon)=f(c)+\delta$. This has only one quantifier alternation.

For compactness, the difference seems to be more far-reaching. Let's stick with separable metric spaces $(M,d)$ for simplicity (this may not be necessary). Then $M$ is compact iff $(\forall x\in M) (\exists^{st} y\in M)(\exists^{in}\epsilon\in\mathbb R) d(x,y)=\epsilon$ (in words: "every point is infinitely close to a standard one"), where $\exists^{st}$ denotes quantification over standard elements. But there is apparently no definition of compactness in the $\in$-language that involves quantification over elements only (the classical definitions involve quantification over sequences or open covers, etc.). Can this be formally proved?

I should have mentioned also that, if the Heine-Borel theorem is satisfied for an ambient complete space including $M$, then such a definition of compactness does exist since one can formulate both closedness and boundedness while quantifying only over elements (even in this case, one can ask how complex the formula would have to be). This item requires more precise formalisation in terms of an appropriate structure.

Note. This question is formulated in a foundational framework referred to as "nonstandard axiomatic approach" in Joel David Hamkins' useful answer here. Such an approach is the only one that enables a study of the role of the axiom of choice in infinitesimal analysis in the spirit (though not the letter) of reverse mathematics, as outlined in this answer to the same question. This approach suggests that the real numbers possess resources undreamt of by Dedekind, which is usually a source of celebration in mathematics.

Answer 1

Often the way you prove that something isn't formalizable in first-order logic is (ironically enough) with a compactness proof. This is how you show, for instance, that there isn't a first-order theory in the language of equality whose class of models is precisely the finite sets.

For your question though, you have this extra stipulation that the structure has $\mathbb{R}$ as a second sort that is always the standard $\mathbb{R}$. This makes applying compactness arguments directly difficult, since they can't guarantee that the example produced will have the reals sort be the standard $\mathbb{R}$. (That said, a related question is whether compactness is formalizable in continuous logic and it turns out there that the answer is also no precisely by this kind of compactness argument.)

However, there's a second tool that is relevant here, which is Ehrenfeucht–Fraïssé games. In some sense Ehrenfeucht–Fraïssé games are just a particular semantic way of talking about formulas, but they're often in practice a little bit easier to think about.

---

Let $D$ be the class of structures in your language with standard $\mathbb{R}$ satisfying that for any $x,y \in M$, $d(x,y) \in \{0,1\}$. Clearly a metric space in $D$ is compact if and only if its $M$-sort is finite. Furthermore, a structure in $D$ is determined up to isomorphism by the cardinality of its $M$ sort. For each cardinal $\kappa$, let $\Delta_\kappa$ be some fixed structure in $D$ satisfying $|M^{\Delta_\kappa}| =\kappa$.

Proposition. For sentence $\varphi$, there is a finite $n$ such that for any cardinals $\kappa$ and $\lambda$ with $\kappa,\lambda > n$, $\Delta_\kappa\models \varphi$ if and only if $\Delta_\lambda\models \varphi$.

Proof. By standard facts about Ehrenfeucht–Fraïssé games, it is enough to show that for any $m$ (corresponding roughly to the quantifier complexity of $\varphi$), there is an $n$ such that for any $\kappa,\lambda > n$, duplicator has a winning strategy in the Ehrenfeucht–Fraïssé game on $\Delta_\kappa$ and $\Delta_\lambda$ of length $m$, but this is fairly immediate. We can actually just let $n$ be $m$. Duplicator's winning strategy is this: If spoiler chooses an element of $\mathbb{R}$, duplicator chooses the same element of $\mathbb{R}$. If spoiler chooses an element of $M$ that has not been chosen before, duplicator chooses some element of $M$ (in the other structure) that has also not been chosen before. Since $\kappa, \lambda > n$, this will always be possible. Finally, if spoiler chooses an element of $M$ that has been chosen before (which really spoiler shouldn't be doing anyway since it can't possibly help to win), then duplicator picks the element of the other structure chosen the last time spoiler played that element. It's straightforward to check that plays resulting from this strategy are always wins for duplicator. $\square$

Corollary. There is no sentence $\varphi$ such that $X \models \varphi$ if and only if $M^X$ is compact.

Proof. If there were such a sentence, then we'd have that for any $\kappa$, $\Delta_\kappa \models \varphi$ if and only if $M^{\Delta_\kappa}$ is finite, but this contradicts the proposition. $\square$