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.

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 mathcalP(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.

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

Option 1: We could take $mathbbZ=(omegatimes 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 $mathbbZ$ that are true for one of our constructions, and false for the other. (For instance, consider the statement: The additive identity of $mathbbZ$ is an ordered pair whose second coordinate is the empty set.)

What makes BSD and other questions avoid this kind of problem, is that they are not phrased in the language of ZFC. They are stated in the language of rings, or topological rings, etc...

So, a proof in ZFC of such statements cannot rely on any specific realization of $mathbbZ$ or $mathbbR$ as a specific set, but would follow Terry's idea of conservatively extending ZFC with a symbol for that set, satisfying the necessary conditions.

And, yes, it is obvious that BSD only requires $mathbbR$ to be a completion of $mathbbQ$ 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.