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 rewrited 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 works 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".

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".

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 rewrited 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. 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 works 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".

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 rewrited 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 works 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".