Skip to main content
added 130 characters in body
Source Link
tomasz
  • 1.3k
  • 7
  • 18

$\newcommand{\st}{\textrm{st}}\newcommand{\bR}{{\bf R}}\newcommand{\bN}{{\bf N}}$ I think the limit of any definable convergent sequence $(a_n)$ (including $e$) is definable by the formula $$\varphi(x)=(\exists x'\in {\bR}^\st\, x'=x)\land \forall N\in\bN^\st\exists n_0\in \bN^\st\forall n\in \bN^\st_{>n_0}(a_n-x)^2<N^{-1}.$$

Since the language includes natural numbers, we have all of Peano arithmetic, so I think by a similar argument, every computable (and I guess every definable in PA) real should be definable. The point is that if you allow quantifiers which range over a given set, then you automatically make that very set definable, so you have at least as much strength as you would have in the smaller structure.

Edit: The idea was first mentioned by Ramiro de la Vega in comments, which I neglected to read before writing this answer.

$\newcommand{\st}{\textrm{st}}\newcommand{\bR}{{\bf R}}\newcommand{\bN}{{\bf N}}$ I think the limit of any definable convergent sequence $(a_n)$ (including $e$) is definable by the formula $$\varphi(x)=(\exists x'\in {\bR}^\st\, x'=x)\land \forall N\in\bN^\st\exists n_0\in \bN^\st\forall n\in \bN^\st_{>n_0}(a_n-x)^2<N^{-1}.$$

Since the language includes natural numbers, we have all of Peano arithmetic, so I think by a similar argument, every computable (and I guess every definable in PA) real should be definable. The point is that if you allow quantifiers which range over a given set, then you automatically make that very set definable, so you have at least as much strength as you would have in the smaller structure.

$\newcommand{\st}{\textrm{st}}\newcommand{\bR}{{\bf R}}\newcommand{\bN}{{\bf N}}$ I think the limit of any definable convergent sequence $(a_n)$ (including $e$) is definable by the formula $$\varphi(x)=(\exists x'\in {\bR}^\st\, x'=x)\land \forall N\in\bN^\st\exists n_0\in \bN^\st\forall n\in \bN^\st_{>n_0}(a_n-x)^2<N^{-1}.$$

Since the language includes natural numbers, we have all of Peano arithmetic, so I think by a similar argument, every computable (and I guess every definable in PA) real should be definable. The point is that if you allow quantifiers which range over a given set, then you automatically make that very set definable, so you have at least as much strength as you would have in the smaller structure.

Edit: The idea was first mentioned by Ramiro de la Vega in comments, which I neglected to read before writing this answer.

Source Link
tomasz
  • 1.3k
  • 7
  • 18

$\newcommand{\st}{\textrm{st}}\newcommand{\bR}{{\bf R}}\newcommand{\bN}{{\bf N}}$ I think the limit of any definable convergent sequence $(a_n)$ (including $e$) is definable by the formula $$\varphi(x)=(\exists x'\in {\bR}^\st\, x'=x)\land \forall N\in\bN^\st\exists n_0\in \bN^\st\forall n\in \bN^\st_{>n_0}(a_n-x)^2<N^{-1}.$$

Since the language includes natural numbers, we have all of Peano arithmetic, so I think by a similar argument, every computable (and I guess every definable in PA) real should be definable. The point is that if you allow quantifiers which range over a given set, then you automatically make that very set definable, so you have at least as much strength as you would have in the smaller structure.