$\def\f#1{\text{#1}}$Does $\f{ACA}$ prove that any two internally complete ordered fields are isomorphic?

Here internal completeness is expressed roughly as "every sequence of reals with an upper bound has a least upper bound", where the sequences and reals are coded appropriately.

This is an attempt to express the categoricity of the reals in the context of subsystems of 2nd-order arithmetic, where $\f{ACA}_0$ is already equivalent to the internal completeness of the (coded) reals over $\f{RCA}_0$ (SoSOA).

To be precise, let $T$ be the 2-sorted FOL theory $\f{ACA}_0$ with sorts $N,S$ where $N$ is for the naturals and $S$ is for the subsets of $N$, plus the following:

  • Predicate-symbol $R$ on $S$ (intended to represent the subsort of reals).
  • Constant-symbols $0_R,1_R$ of sort $S$.
  • Function-symbols $+_R,·_R$ from $S^2$ to $S$.
  • Predicate-symbol $<_R$ on $S^2$.
  • Axioms stating that $(R,0_R,1_R,+_R,·_R,<_R)$ is an ordered field.
  • The internal completeness axiom, namely $∀f{∈}N{→}R\ ( \ ∃m{∈}R\ ( \ f ≤ m \ ) ⇒ ∃m{∈}R\ ( \ f ≤ m ∧ ∀x{∈}R\ ( \ f ≤ x ⇒ m ≤ x \ ) \ ) \ )$ where "$f ≤ t$" is short-hand for "$∀k{∈}N\ ( \ f(k) ≤_R t \ )$". (Here each member of $N{→}R$ is of course coded as a member of $S$.)

$T$ is what I mean by "theory of internally complete ordered field". Now $T$ is actually conservative over $\f{ACA}_0$, by the equivalence of $\f{ACA}_0$ and 'completeness of reals' over $\f{RCA}_0$. And so we can work within this theory $T$ to do applied real analysis, and we know that it is no stronger than $\f{ACA}_0$.

The question is, does $\f{ACA}$ (no subscript zero) prove that every two $ω$-models of $T$ are isomorphic? From the perspective of a set theory, $\f{ACA}$ cannot reason about uncountable sets, but can reason about countable $ω$-models of a 2-sorted FOL theory, which are precisely what I am interested in here. In particular, "for every countable set" translates to "∀X{∈}S" in the language of $\f{ACA}$.

Since $\f{ACA}$ proves the existence of an $ω$-model of $\f{ACA}_0$, we know that $\f{ACA}$ also proves the existence of an $ω$-model of $T$. The question is whether it knows the uniqueness of such models up to isomorphism.

~ ~ ~

The standard proof seems to go through: Take any models $K,M$. Construct the isomorphism $f$ from rationals $Q(K)$ of $K$ to rationals $Q(M)$ of $M$ via arithmetical comprehension. Then construct $g$ from elements of $K$ to elements of $M$ where $g(x) = \sup_M( \{ f(w) : w∈Q(K) ∧ w <_K x \} )$. Here we can use any usual enumeration of $Q(K)$ and apply internal completeness for $M$. Now we simply have to prove that $g$ is an embedding, since self-embedding on $K$ that fixes $Q(K)$ also fixes everything else. Firstly, $g$ is injective since $Q(K)$ is dense in $K$, by internal completeness of $K$. Secondly, $g$ is a homomorphism, which is a bunch of cases but should be similar.

But I am unable to find anything on the reverse mathematical strength of categoricity of the 'reals'. Can anyone confirm what I said here or give any reference? I could slowly check it myself but it would be nice if it was already a well-known result.

  • 3
    $\begingroup$ With the usual definitions of "complete ordered field" (either "all Dedekind cuts are filled" or "all Cauchy sequences converge") there are no countable ones; the reals are, up to isomorphism, the only example. Won't the usual proof of that (i.e., essentially the proof of uncountability of the reals) work in ACA? $\endgroup$ Oct 15, 2021 at 19:02
  • 2
    $\begingroup$ I agree with @AndreasBlass: $\mathsf{ACA}$ (or indeed much less - even $\mathsf{RCA_0}$ is enough) proves that there is no countable complete (in your sense, or any other I can think of) ordered field. This is because $\mathsf{ACA}$ proves more generally that for every countable dense linear order $L$ there is a pair of sequences $(a_i)_{i\in\omega},(b_i)_{i\in\omega}$ such that $a_i<a_{i+1}<b_{i+1}<b_i$ for all $i\in\omega$ and there is no $x\in L$ with $a_i<x<b_i$ for all $i\in\omega$. Your previous comment mixes up external and internal countability. $\endgroup$ Oct 15, 2021 at 19:11
  • 2
    $\begingroup$ @user21820 I don't understand your comment; it seems to be overcomplicating the situation. "There is no countable ordered field (or even just linear ordering) with the least upper bound property" is easily formalizable and provable in $\mathsf{ACA}$, or indeed much less. $\endgroup$ Oct 15, 2021 at 19:21
  • 2
    $\begingroup$ It is of course true that any $M\models\mathsf{ACA}$ has an associated real closed field $R_M$. However, $R_M$ is not countable from the perspective of $M$, even if $M$ itself is countable. I don't understand how $R_M$, or anything like it, is relevant to the question "Does $\mathsf{ACA}$ prove that any two countable complete ordered fields are isomorphic?," which I can only make sense of in a vacuous way. $\endgroup$ Oct 15, 2021 at 19:24
  • 3
    $\begingroup$ "that "countable" part in "countable complete ordered field" was not in the original version of my question" From the original version of your question: "I was wondering, does ACA prove that theory of the reals (with this version of the completeness axiom), in the sense that any two (countable) models are isomorphic?" (emphasis mine). I'm really not sure what you're asking at this point. $\endgroup$ Oct 15, 2021 at 19:27

1 Answer 1


The current version of the question is flawed: the proposed categoricity principle is in fact classically false. Roughly speaking, any "interesting" theory of the appropriate type is going to have lots of non-isomorphic countable $\omega$-models. (For massive overkill let $M,N$ be countable elementary submodels of $V_{\omega_{17}}$ with $M\in N$ and $\vert M\vert^N=\aleph_0$; then the structures we get from $\mathbb{R}\cap M$ and $\mathbb{R}\cap N$ will be non-isomorphic countable $\omega$-models of whatever theory you whip up.)

I think the right way to tackle a question like this is to get away from the language of "countably coded structures," or structures as internal objects, entirely. While this is usually how we implement anything model-theory-flavored in reverse mathematics, it's not at all suitable here due to a "pincer attack" of the observation in the above paragraph on the one hand and the fact that $\mathsf{RCA_0}$ proves the nonexistence of countable complete ordered fields on the other hand (the latter killing approaches which avoid the issue posed by the former).

To find the right way to pose the question I think it's necessary to take a step back and think semantically. Given $M\models\mathsf{ACA_0}$, the object we're interested in initially is the ordered field of reals in the sense of $M$, or a bit more precisely the natural interpretation of this field into $M$. Call this "$\mathbb{R}^M$." Now $\mathbb{R}^M$ is not a "structure in $M$" in the usual sense, nor is it countable from the perspective of $M$ in any good sense. It's more analogous to a proper class than to an internal object. Now intuitively we want to compare $\mathbb{R}^M$ to its "alternatives" - and these alternatives should be objects of exactly the same type. This leads us away from countably coded structures altogether, and suggests the following precisiation of your question:

$(*)\quad$ Suppose $M\models\mathsf{ACA_0}$, so that $\mathbb{R}^M$ is "internally complete." Let $\Phi$ be any tuple of formulas such that $\Phi^M$ is also an $M$-"internally complete" ordered field. Must there be an $M$-definable isomorphism between $\mathbb{R}^M$ and $\Phi^M$?

  • Note that in fact this phrasing lets us shed the language of reverse mathematics altogether: as a way-too-ambitious project we could try to understand when a structure $\mathfrak{A}$ has exactly one internally complete interpretation of an ordered field up to definable isomorphism. In my opinion part of what makes $\mathsf{RCA_0}$ and its extensions fun to think about is exactly that it carves out a subclass of structures on which this sort of project is not too ambitious.

I believe that $(*)$ is in fact what you are trying to ask here. The answer to $(*)$ at first glance appears to be that $\mathsf{ACA_0}$ is already enough, but I'll check in more detail if you clarify that this is indeed a faithful precisiation of the question you're asking.

  • $\begingroup$ I believe your answer would be a semantic analogue of the syntactic version I actually had in mind, which I am in the midst of 'precising' (I didn't know it is an English word haha). Sorry to make you wait. =) $\endgroup$
    – user21820
    Oct 15, 2021 at 19:58
  • $\begingroup$ @user21820 I don't actually think "precisiate" is an English word, it's something I saw a speaker say frequently (Lofti Zadeh, in the context of fuzzy logic) and liked so much I stole it. :P $\endgroup$ Oct 15, 2021 at 19:58
  • $\begingroup$ @user21820 Some serious circumlocution will be required to get a syntactic phrasing of this, since it's quantifying over arbitrary-complexity interpretations and arbitrary-complexity definable isomorphisms and the completeness criterion itself involves quantifying over arbitrary-complexity sequences. Basically, you'll get a family of $\mathsf{ACA_0}$-theorems like "Every $\Sigma_{17}$-interpretation of a $\Sigma_{38}$-complete ordered field is $\Sigma_{42}$-isomorphic to $\mathbb{R}$." It's nasty. $\endgroup$ Oct 15, 2021 at 20:15
  • $\begingroup$ Hmm, could you please check out my current version of the question? I think it's the precise form of what I had in mind. $\endgroup$
    – user21820
    Oct 15, 2021 at 20:34
  • $\begingroup$ @user21820 That version is now false - note that classically your theory $T$ has many non-isomorphic countable $\omega$-models. I've edited to say a bit about this. $\endgroup$ Oct 15, 2021 at 20:58

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge that you have read and understand our privacy policy and code of conduct.

Not the answer you're looking for? Browse other questions tagged or ask your own question.