$\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.
Best Answer
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:
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.