Cauchy reals and Dedekind reals satisfy "the same mathematical theorems"

Question

The succinct question

The conjecture of Birch and Swinnerton-Dyer (to take a random example) mentions L-functions and hence the complex numbers and hence the real numbers (because the complexes are built from the reals). Two naive questions which probably just indicate that I don't understand logic well enough: (1) if we regard BSD as a statement about an explicit model of the real numbers (e.g. the one built from Cauchy sequences or the one built from Dedekind cuts), then why is it "obvious" that BSD is true for one iff it's true for the other? (2) Is it "obvious" that BSD can be formulated as a statement BSD(F) which makes sense for an arbitrary complete ordered archimedean field F? If so, is it also "obvious" that BSD in this sense is isomorphism-invariant, i.e. if F1 and F2 are isomorphic then BSD(F1) iff BSD(F2)?

I am interesting in learning the techniques behind why mathematicians treat these claims as obvious.

The original question(s)

Up to unique isomorphism, there is only one complete archimedean ordered field, and mathematicians refer to it as "the real numbers". There are two standard constructions for showing that such a field exists, one using Dedekind cuts and the other using Cauchy sequences. To be even more explicit, let me define "the Cauchy reals" in this question to mean the set of equivalence classes of Cauchy sequences modulo the usual equivalence relation (so if $x$ is a Cauchy real then $x$ is an uncountably infinite set) and let me define "the Dedekind reals" as being Kuratowski ordered pairs $\{\{L\}, \{L,R\}\}$ with $L$ and $R$ a partition of the rationals with every element of $L$ less than every element of $R$ and both non-empty and $L$ having no rational sup (so if $x$ is a Dedekind real then $x$ is a finite set).

Because these two constructions give canonically isomorphic objects, mathematicians think of these constructions as giving "the same answer" and never fuss about which version of the real numbers they are using. I guess there must be some underlying logical principle behind why this works, but I now realise I don't know it. What is it?

I am hoping that there is some theorem of logic that says that if I formulate a conjecture (in ZFC set theory, say) about all complete archimedean ordered fields and then I prove the conjecture for the Cauchy reals, then I can somehow deduce that it is also true for the Dedekind reals. But as it stands this is not true. For example, a stupid conjecture about all complete archimedean ordered fields is that they are all equal (as sets in ZFC) to the Cauchy reals. This conjecture is false in general, true for the Cauchy reals, and not true for the Dedekind reals. On the other hand, clearly any "sensible" (I don't know a formal definition of this) mathematical question about complete archimedean ordered fields will be true for the Cauchy reals iff it's true for the Dedekind reals. What would a proof look like? Does one need to give some kind of algorithm which changes a certain kind of proof about Cauchy reals to Dedekind reals? In what generality does this sort of thing work? What are the ingredients? Note that I cannot guarantee that my proof treats the Cauchy reals only as a complete archimedean ordered field, even though I "know in my heart" that there is no advantage in actually starting to look at elements of elements.

Here is a related question. Take a normal mathematical conjecture which mentions the reals (for example the Birch and Swinnerton-Dyer conjecture, which mentions L-functions, which are functions on the complex numbers, and a complex number is usually defined to be a pair of reals). Every mathematician knows that it doesn't matter at all whether we use the Dedekind reals or the Cauchy reals. So what is the proof that BSD is true for the L-functions built using the Dedekind reals iff it's true for the L-functions built using the Cauchy reals? It seems to me that we could attempt to use the preceding paragraph, but only once we know that some version of BSD can be formulated using any complete archimedean ordered field, and that the resulting formulation is "a sensible maths question". My gut feeling is that this is "obvious"; however I would rather hear some general principle which I can invoke than actually have to say something coherent about why this is true.

Background

A few years ago I would have found this kind of question extremely confusing to think about, and would have either dismissed it as trivial or just said that the real numbers were unique up to unique isomorphism and there were probably "theorems of logic" which resolved these issues. But I have a better understanding of what mathematics is now, and I realise that I am not quite sure about how all this works. Here is an attempt to explain what I think are the guts of the first question.

Let's say I am doing "normal" mathematics, and I come up with a "normal" mathematical conjecture that mentions real numbers in some way, e.g. the conjecture that pi + e is transcendental, or some much more complicated conjecture which mentions the real numbers implicitly, like the Birch and Swinnerton-Dyer conjecture (which mentions the complex numbers, which are built from the real numbers). No mathematician would ask me whether I mean the Cauchy reals or the Dedekind reals in my conjecture. Let's say I decide to offer $1,000,000 for a proof of my conjecture.

Now say some wag who is into computer proof formalisation asks me what foundational system I am using when I make my conjecture, so I say "ZFC set theory". And then they remark that the real numbers have two definitions in ZFC set theory, one using Cauchy sequences and one as Dedekind cuts, and which real numbers was my conjecture about? I am a mathematician, so I know it doesn't matter, so I say "the Cauchy reals" just to shut them up. The next day I realise I could have been more clever, so I take the trouble to reformulate my conjecture so that instead of explicitly mentioning "the real numbers" I make it into a conjecture about all complete archimedean ordered fields (the fact that this reformulation is possible could be thought of as a definition of "normal" mathematics in the paragraph above). Of course I "know" that this does not change my conjecture in any substantial way. I decide to get in touch with the wag to tell them my change of viewpoint, so I call them up, but before I can get a word in, they very excitedly tell me that they left their new deep learning AI ZFC computer proof generator system on all night working on my conjecture about the Cauchy reals, and it has managed to come up with a proof which is a billion lines long and incomprehensible, but each line is formally checked to be valid in ZFC, so it must be right, and can they please have the $1,000,000. I explain that I have now changed my conjecture and it's now a statement about all complete archimedean ordered fields, and ask them if their proof works for all such fields. "Definitely not!" they reply. "My AI needs to generate proofs of trivial things like 3 < 5 to prove your conjecture, and it does it by thinking about the definition of < on the Cauchy reals and coming up with a proof of 3 < 5 which is specific to Cauchy reals. My AI also does a bunch of other weird things with Cauchy reals, and some of them I don't understand at all; they are probably just weird ways of proving standard facts about complete archimedean ordered fields but I can't be sure". "Well, does everything you do for the Cauchy reals have some analogue for the Dedekind reals?" I ask. And they reply "I don't know, all I can guarantee is that my proof is valid in ZFC set theory, and therefore I have proved your conjecture in its Cauchy form. You are claiming that the Cauchy form and the complete archimedean ordered field form are obviously equivalent, hence I have proved your more general conjecture."

I think the wag must be right, but I do not understand the details of why.

Answer 1

Here's a low-tech way to look at it, which to me seems perfectly convincing.

Let C be some implementation of the reals via Cauchy sequences and D be some implementation of the reals via Dedekind cuts. Here C is "really" something like a tuple consisting of the set of reals, a relation corresponding to addition, etc.; D is a tuple with (allegedly) equivalent things implemented differently.

Let P(X) be the proposition that X is a tuple of the right size and that, when considered as an implementation of the real numbers, X satisfies the Birch-Swinnerton-Dyer conjecture. We have a proof -- perhaps a bizarre incomprehensible implementation-dependent one -- of P(C), in ZFC.

I claim that (again, in ZFC) P(C) iff P(D). Sketch of proof: 1. Up to canonical isomorphism there is only one complete ordered field. 2. C and D are complete ordered fields. 3. Therefore there is an isomorphism between C and D; in fact we can even write it down. 4. We can use this to build an isomorphism between C's complex numbers and D's complex numbers, and then between C's L-functions and D's L-functions, and C's elliptic curves and D's elliptic curves, and so on for every object required to state the BSD conjecture. 5. If we have a specific elliptic curve over D, these isomorphisms yield its equivalent over C (and vice versa); they pair up the groups of rational points in the two cases, showing that they have the same rank; they pair up the corresponding L-functions, showing that they have the same order of zero at s=1. 6. And we're done.

None of this requires that these isomorphisms be applied to the proof of P(C). That proof can be as C-specific as you like. What the isomorphisms show is that the things BSD says are equal come out the same way however you implement the real numbers.

How do we know that we can actually construct this pile of isomorphisms? By thinking about what objects we need in order to state the BSD conjecture, and how we build them, and noting that nothing in the process cares about "implementation details" of the real numbers. If you're sufficiently confident of your memory, you could do this "negatively" by noting that if when you were learning about elliptic curves and L-functions a lecturer had said something like "and of course this is true because the number 1 is just the same thing as the set containing just the empty set" you'd have noticed and been horrified. Otherwise, you can (tediously but straightforwardly) go through the usual textbooks and check that the constructions are all "sane".

EDITED to add:

Although I stand by everything above, I can't escape the feeling that Kevin already knows all that and I'm therefore not answering quite the question he's meaning to ask. Let me put some words into Kevin's mouth:

Yes, yes, of course. Every mathematician who thinks about this stuff at all has something like that mental picture. But what really justifies that breezy confidence that that big pile of isomorphisms is really there? I understand that it feels obvious that none of the machinery you need to state something like the BSD conjecture depends on "implementation details". But this is the sort of thing mathematicians are good at getting wrong. It wasn't until the 20th century that we noticed how many extra axioms you really need to add to Euclid's system to make the proofs in the Elements rigorous. The axiom of comprehension probably seemed obviously innocuous until Bertrand Russell asked whether the set of non-self-membered sets shaves itself. A more isomorphism-y example: it seems transparently obvious that a set $X$ is the same size as $\{\{x\}\,:\,x\in X\}$, but this fails if you work in NF instead of ZFC. Maybe there's some implementation detail no one ever noticed we were assuming. How can we be sure?

Again, personally I'm very confident that I'd have noticed if some implementation detail were being slipped into anything in "normal" mathematics (or at least, I'm as confident as that I'd have noticed any other sort of gap in the proofs -- I don't think there's anything special here), and very confident that if I missed one some of the many many other mathematicians, some of them much smarter than I am, who have read the same textbooks and been to the same lectures would have noticed. But I think Kevin's asking whether there's some simple principle that makes it obvious without any need either to trust that sort of thing, or to check in detail through everything in the textbooks, and I want to be clear that this answer doesn't purport to give one; my feeling is that there couldn't possibly be one, any more than there could be some simple principle that makes it obvious (with the same restrictions) that there are no other logical holes in those same textbooks, and for essentially the same reason.

Answer 2

Here is a way to do this in ZFC. Similar ideas work in a bunch of other contexts.

First, given any set $A$ in the universe of sets $V$ we can form the set theoretic universe $V(A)$ by mimicking the cumulative hierarchy, where the elements of $A$ are considered to be atoms. Start with $V_0(A) = A$, at successors $V_{\alpha+1}(A) = V_\alpha(A) \cup \mathcal{P}(V_\alpha(A))$, at limits $V_\delta(A) = \bigcup_{\alpha<\delta} V_\alpha(A)$. (Some care must be taken to carefully distinguish atoms. Indeed, $A$ will appear at some point in the pure part of $V(A)$ and we don't want to confound this pure $A$ with the set of atoms $A$. Fortunately, it is well-understood how to do this formally. Since these details are irrelevant, I will not mention them further.)

If $A$ has additional structure, say it's a complete ordered field, then that structure will appear quickly in the hierarchy since we add all possible subsets at each step. Therefore $A$ has all the same ordered field structure it originally had in $V$. Even completeness carries through since the subsets of $A$ in $V(A)$ come from subsets of the original $A$ in $V$. The difference is that $A$ has no internal structure in $V(A)$ since we can't inspect the innards of atoms: all we can say about atoms is whether two atoms equal or not. The main kicker is that if $A'$ is any isomorphic structure to $A$, then the isomorphism of $A'$ and $A$ lifts uniquely to an isomorphism of $V(A')$ and $V(A)$!

A normal mathematical statement about $A$ in $V$, say BSD, makes perfect sense about the structure $A$ in $V(A)$. This is because BSD makes no mention at all of the innards of the elements of $A$. Furthermore, if BSD holds of the original $A$ in $V$ then it will hold of the $A$ in $V(A)$ since they have identical external structure. Because $V(A')$ is isomorphic to $V(A)$, the isomorphism ensures that BSD holds of $A'$ in $V(A')$. Then, for the reverse reason explained above, BSD holds of the original $A'$ in $V$.

For this transfer from $A$ to $A'$, we only needed that BSD was a normal mathematical statement in the sense that it relies only on the external structure of $A$ and $A'$ and not on the innards of these structures. Whether some proof of BSD for $A$ relies heavily on the innards of $A$ is irrelevant since the statement proven makes no mention of the internal structure of $A$ and will therefore transfer to any isomorphic structure as described above.

Answer 3

From a logical viewpoint, this has nothing to do with platonism, ZFC, or the cumulative hierarchy. $ \def\nn{\mathbb{N}} \def\zz{\mathbb{Z}} \def\qq{\mathbb{Q}} \def\rr{\mathbb{R}} \def\cc{\mathbb{C}} $

Almost all reasonable mathematical statements about the reals are actually about any structure that satisfies the axiomatization of the reals. It is clear that this axiomatization can be expressed in very weak foundational systems, whether or not compatible with ZFC. Of course, if you are only familiar with ZFC then you may have to look at how things go in ZFC (as François G. Dorais has explained). But ZFC is really a red herring here.

The Cauchy-sequence or Dedekind-cut constructions merely serve to prove the existence of such a structure that satisfies the axiomatization of the reals. From then on, we can literally forget the exact objects in the construction (which is precisely what $∃$-intro does), because we are only interested in theorems concerning the axiomatized properties (interface) of the reals. Similarly when you construct the complex numbers by a quadratic extension of $\rr$ by some object $i$ such that $i^2 = -1$ in the field extension $\rr(i)$, it is completely irrelevant what objects are 'used' as elements in the field extension. For instance, you could use linear polynomials in $X$ with addition and multiplication modulo $X^2+1$. All that matters is that you get an algebraically closed field containing an isomorphic copy of the reals. Relatedly, we can assume that $\rr ⊆ \cc$ because we only care about the axiomatized properties of $\rr$, which are preserved under isomorphism. One could manually preserve the original $\rr$ as an actual subset of its quadratic extension, but that is unnecessary for the reason I just stated.

Long before $\rr$, to even get from $\nn$ to $\zz$ we could either encode an integer as a sign with a magnitude, or as an equivalence class of pairs from $\nn$. Does it matter? No, because all we care about are certain properties.

If someone claims to have proved something about reals but their proof needs to look at the concrete implementation of reals, then that someone simply has taken a silly route. This is akin to expressing an algorithm in the SOAP assembly language for the IBM 650, instead of expressing it in at least a high-level language supporting loops and function calls. Good software is always written to separate interface from implementation, and so are good proofs (whether in a formal system or not).

Consider simple examples. The IVT (intermediate value theorem) concerns continuous functions on a closed bounded interval of the reals. To state it directly, we must be able to quantify over real functions. This only needs 3rd-order arithmetic (since a real can be naturally encoded as a function of naturals, which is 2nd-order, so a function from reals to reals would be 3rd-order). More generally, if you want to talk about objects in specific higher-order types where the 0th-order type is the naturals, then all you need is HOA (higher-order arithmetic). Practically any modern foundational system for mathematics can interpret HOA, namely that there is a computable translation of proofs from HOA into the system that interprets it. You can check that Z set theory for instance interprets HOA, and if you want some extra interesting sets you might want some form of AC (axiom of choice).

Anyway, IVT is provable in HOA using only the axiomatization of the reals. And so are EVT (extreme value theorem), MVT (mean value theorem), Dini's theorem for real functions, ... You only need to go beyond HOA if you want to handle arbitrary types, such as general metric spaces, topological spaces and so on. Even then, every mathematical structure of interest will be defined via axiomatization, and all proofs based on that axiomatization alone would of course carry over to all those structures.

There is one possible snag, namely what if the proof was found by a computer rather than a human? Well, if the proof is really just one huge mess, then the easiest solution has been provided by Gareth McCaughan: We can tack on a proof of the equivalence of the desired theorem about Cauchy-reals with the same theorem stated for any isomorphic copy of the reals, and hence we can treat the given computer-generated proof as a black-box. More generally, we can write a computer program $P$ such that, given any desired statement $Q$ about a model $M$ of some second-order axiomatization $A$ that only uses $M$ via its interface $A$, $P(Q)$ outputs a proof that $Q(M)$ implies $Q(N)$ for every model $N$ of $A$. Then we do not even have to manually construct such kind of tack-on proofs but can just run that single program $P$ on any theorem that that 'wag' throws at you, and not just for those about reals. The exact details would depend on the chosen foundational system, but Z set theory certainly suffices.

Answer 4

I see a lot of confusion in the comments about what you are asking and why. The way I interpret your question is this:

Given the fact that mathematical statements about (or involving) the reals can be divided into two classes,

A. those that are “isomorphism invariant” (their truth does not depend on which model of the reals you’re using) and

B. those that aren’t,

what is a way to decide whether a given statement belongs to class A or to class B?

I’ll offer a sociological rather than mathematical criterion: if the statement is (as in your example) an open problem with a $1,000,000 prize, or is otherwise a famous/important question, you can be pretty darn sure that it’s in class A; or, conceivably (but with a much lower likelihood) that it’s in class B but that the statement of the question would make very clear which model of the reals it pertains to.

The remaining possibility, that the question contains some kind of hidden ambiguity that makes it belong in class B but in a way that isn’t formally stated, seems essentially inconceivable to me in the context of well-known open problems. The reason is that most working mathematicians are Platonists who, when they think of the real numbers, think of some ideal set satisfying the properties they know the real numbers satisfy, and never concern themselves with pesky foundational issues regarding the actual model of the reals underlying the discussion. For such people, the statements in class A are the only interesting statements (and in some Platonist sense, the only “real” statements) about the reals. A model-dependent question would likely never deserve to be labeled as important, unless it was in some explicit foundations of math context where that model dependence would be an explicit part of the statement of the problem.

As for a formal mechanism that you are asking about for distinguishing between class A and class B statements, as others have said, you need to check that the statement will survive being passed through an isomorphism. How this is done in practice for something like BSD would probably be extremely tedious (and in my opinion isn’t worth the trouble), but an intuitive level, if the statement is phrased in a “coordinate-free” manner that doesn’t appeal to Dedekind cuts or other objects used in a specific realization of the reals, that’s probably good enough to declare “it’s obvious” and go and do something more productive with your time. Well, at least it would be for a Platonist like me.

Answer 5

There is no need to even go as far as $\mathbb{R}$ for an example of this type of phenomena. Even $\mathbb{Z}$ could be defined as different sets in ZFC. Let $\omega$ be the first infinite cardinal, as usual

Option 1: We could take $\mathbb{Z}=(\omega\times \{0\})\cup ((\omega-\{0\})\times \{1\}),$ where the second coordinate tells us whether the integer is positive or negative.

Option 2: Switch second coordinates.

Now, if our background theory is ZFC, we can certainly create statements about $\mathbb{Z}$ that are true for one of our constructions, and false for the other. (For instance, consider the statement: The additive identity of $\mathbb{Z}$ is an ordered pair whose second coordinate is the empty set.)

What makes BSD and other questions often avoid this kind of problem, is that they are stated in a language of rings, or topological rings, etc... where the derived objects (like analytic rank) will be invariant when extended to a language allowing multiple identical copies of the structure at hand. (When it isn't immediately clear whether or not a definition or property is well-defined/invariant for the given context, good mathematical writing requires one to point this out.) And, yes, it is obvious that BSD only requires $\mathbb{R}$ to be a completion of $\mathbb{Q}$ at the archimedean place. (Obvious, because we would otherwise have required more in the statement of BSD.) And, yes, you can show that analytic ranks and algebraic ranks are preserved by isomorphisms between completions.

Answer 6

There is no need to use explicit models of $\mathbb R$ in formulations of Swinnerton-Dyer conjecture. You could extend $\mathbf{ZFC}$ with symbols $(\mathbb R,+_\mathbb R,\times_\mathbb R,<_\mathbb R,0_\mathbb R,1_\mathbb R)$ (in addition to symbols $=,\in$) and add obvious axioms of Reals. After that you obtain new system, say $\mathbf{ZFC}+\mathbb R$ in which you able to formulate any theorem about Reals model-independently using those new symbols. To be sure that $\mathbf{ZFC}+\mathbb R$ is conservative extension of $\mathbf{ZFC}$ you should to justify your axioms by construction of either Dedekind or Cauchy reals. So, you should to proof in $\mathbf{ZFC}$ statement $$\exists \mathbb R_{Cauchy}, +_{\mathbb {R}_{Cauchy}},\times_{\mathbb {R}_{Cauchy}},<_{\mathbb R_{Cauchy}},0_{\mathbb R_{Cauchy}},1_{\mathbb R_{Cauchy}} ({axiom}_1 \wedge {axiom}_2 \wedge ... \wedge {axiom}_n)$$ where ${axiom}_1,...,{axiom}_n$ is axioms of real numbers rewritten in terms of Cauchy reals, for example ${axiom}_1$ is $$0_{\mathbb R_{Cauchy}} \in \mathbb{R}_{Cauchy}$$ ${axiom}_2$ is $$\forall x \forall y (x \in \mathbb R_{Cauchy} \wedge y \in \mathbb R_{Cauchy} \to x+_{\mathbb R_{Cauchy}} y = y +_{\mathbb R_{Cauchy}} x)$$ and so on (of course you additionaly need to state that $+_{\mathbb R_{Cauchy}}$ is well-defined function on $\mathbb {R}_{Cauchy}$ and write $((x,y),t) \in +_{\mathbb{R}_{Cauchy}}$ rather than $x +_{\mathbb{R}_{Cauchy}} y = t$) . After that you could (externally, on metalevel) deduce that your system $\mathbf{ZFC}+\mathbb{R}$ is conservative extension of $\mathbf{ZFC}$ so you could work now inside $\mathbf{ZFC} + \mathbb{R}$ instead of $\mathbf{ZFC}$ and formulate statements about Reals model-independently.

Maybe it sounds a little bit artificial but this is exactly how proof-checkers work see Note on definitions on Metamath Proof Explorer. Also, for example, see axiom ax-resscn and construction-dependent theorem axresscn which is justification of axiom ax-resscn and "should not be referenced directly".

Answer 7

I think it is essentially the Frege–Hilbert controversy on the nature of mathematical axioms, cf. e.g. https://plato.stanford.edu/entries/frege-hilbert/ :

The central difference between Frege and Hilbert over the nature of axioms, i.e., over the question whether axioms are determinately true claims about a fixed subject-matter or reinterpretable sentences expressing multiply-instantiable conditions, lies at the heart of the difference between an older way of thinking of theories, exemplified by Frege, and a new way that gathered strength at the end of the nineteenth century.

Frege (i) understands the consistency and independence of thoughts to turn not just on the surface syntax of the sentences that express them but also on the contents of the simple terms used in their expression, and (ii) consistency and independence, so understood, are not demonstrable in Hilbert’s manner.

[On] Frege’s conception of logic … given a good formal system, a sentence σ is deducible from a set Σ only if the thought expressed by σ is in fact logically entailed by the thoughts expressed by the members of Σ. (This simply requires that one’s axioms and rules of inference are well-chosen.) But the converse is false: that σ is not deducible in such a system from Σ is no guarantee that the thought expressed by σ is independent of the set of thoughts expressed by the members of Σ. For it may well be, as in the cases treated explicitly by Frege’s own analyses, that further analysis of the thoughts and their components will yield a more-complex structure. When this happens, the analysis may return yet-more complex (sets of) sentences σ′ and Σ′ such that σ′ is, after all, deducible from Σ′. … This is the explanation of Frege’s rejection of Hilbert’s treatment of consistency and independence …

Taking a theory to be axiomatized by a set of multiply-interpretable sentences, Hilbert’s view is that the consistency of such a set suffices for the existence of the (or a) collection of mathematical entities mentioned in the theory. The consistency, for example, of a theory of complex numbers is all that’s needed to justify the mathematical practice of reasoning in terms of such numbers. For Frege on the other hand, consistency can never guarantee existence. His preferred example to make this point is that the consistency (in Hilbert’s sense) of the trio of sentences 1. A is an intelligent being, 2. A is omnipresent, 3. A is omnipotent is insufficient to guarantee their instantiation. (See, e.g., Frege’s letter to Hilbert of 6 January 1900.)

Hilbert is clearly the winner in this debate, in the sense that roughly his conception of consistency [and logic] is what one means today by consistency [and logic] in the context of formal theories.

Answer 8

I have a proposal for a (Nearly trivial) instance of such a theorem. Let $Form_{(+,\cdot,\lt)}$ be the set of a logical formulas constructed from the atoms $x+y$, $x\cdot y$, and $x\lt y$, with $x=y$ defined as $\forall z(z\lt x\leftrightarrow z\lt y)$. Then it is a simple to see (Though I will write it here anyway) that if $(\mathbb R,+,\cdot,\lt)$ and $(\mathbb R',+,\cdot,\lt)$ are Dedkind complete ordered fields, then $(\mathbb R,+,\cdot,\lt)\prec(\mathbb R',+,\cdot,\lt)$, where "$\prec$" denotes elementarity in $Form_{(+,\cdot,\lt)}$.

Given an ismorphisim $\pi: (\mathbb R,+,\cdot,\lt)\rightarrow(\mathbb R',+,\cdot,\lt)$, it is immediate that the relation holds for atomic formula, and inductively for logical connectives. Let $\exists x(\phi(x,x_0...x_n))$ be a $Form_{(+,\cdot,\lt)}$ formula, such that $(\mathbb R,+,\cdot,\lt)\vDash \exists x(\phi(x,x_0...x_n))$, and let $z$ be a witness to this. $$(\mathbb R,+,\cdot,\lt)\vDash\phi(z,x_0...x_n)\leftrightarrow(\mathbb R',+,\cdot,\lt)\vDash\phi(\pi(z),\pi(x_0)...\pi(x_n))$$

Therefore $(\mathbb R',+,\cdot,\lt)\vDash\exists x(\phi(x,\pi(x_0)...\pi(x_n)))$, and so $(\mathbb R,+,\cdot,\lt)\prec(\mathbb R',+,\cdot,\lt)$. Why is this important? Well every formula about the Reals in $Form_{(+,\cdot,\lt)}$ is therefore absolute between Dedkind complete ordered fields.

They also satisfy the same second order assertions. Extend the language $Form_{(+,\cdot,\lt)}$ with an atomic formula $x\in X$, and call $x$ a real if $M(x)\leftrightarrow \exists X(x\in X)$. For a non-real $X$, then extend the isomorphisim $\pi$ to $\pi'$ by $\pi'(X)=\{\pi(x)|x\in X\}$, and say $X=Y$ if and only if $\forall x(x\in X\leftrightarrow x\in Y)$. Note that then $x\in X\leftrightarrow \pi'(x)\in \pi'(X)$, and so by the same argument as before $(\mathbb R,+,\cdot,\lt,\in)\prec(\mathbb R',+,\cdot,\lt,\in)$.

So in order to get a result you want what we really want to show is that nearly every sensible statement about the Reals can be coded in just $Form_{(+,\cdot,\lt,\in)}$. This can be verified individually, but a will give you an example: $x=0$, $x=1$, $x\in \mathbb N$, $x\in \mathbb Z$, $x\in \mathbb Q$, $x\in \mathbb {CR}$ (Constructible numbers), as well as algebraic functions can be written in $Form_{(+,\cdot,\lt,\in)}$. First off, $x=0\leftrightarrow \forall y(M(y)\rightarrow x+y=y)$, and similarly with $x=1$.

$$x\in\mathbb N\leftrightarrow \forall X(0\in X\land\forall n\in X(n+1\in X))$$

$$x\in\mathbb Z\leftrightarrow x\in\mathbb N\lor\exists y\in\mathbb N(x+y=0)$$

$$x\in\mathbb Q\leftrightarrow \forall X((X\supseteq\mathbb Z\land\forall y,z\in X({y\over z}\in X))\rightarrow x\in X)$$ (See below)

$$x\in\mathbb {CR}\leftrightarrow \forall X((X\supseteq\mathbb Q\land\forall y\in X(\sqrt{y}\in X))\rightarrow x\in X)$$ (See below)

For the rest, $x={y\over z}\leftrightarrow x\cdot y=z$ and $x=\sqrt y\leftrightarrow x\cdot x=y$. This process is just a couple examples. In fact, you could even though this for the Riemann Hypothesis and other complex mathematical problems. Therefore, your conjecture would almost certainly be absolute between the Cauchy and Dedkind reals.