$\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.

countable) models are isomorphic?"(emphasis mine). I'm really not sure what you're asking at this point. $\endgroup$11more comments