Creo que nunca me había planteado esto de si los naturales en un modelo de ZFC son estándar. Por lo visto es imposible demostrar que hay un modelo estándar de ZFC en ZFC+Con(ZFC): https://mathoverflow.net/questions/331897/existence-of-a-model-of-zfc-in-which-the-natural-numbers-are-really-the-natural
No conocía ese resultado. Es muy sencillo (una vez se le ha ocurrido la idea a otro

). Gracias por la información.
La idea es que dos modelos estándar tienen que tener los mismos números naturales, pero puedes modificar un modelo "por las alturas" sin tocar los números naturales, y hacer así que cambien cosas que no dependen de ellos.
Lo de poder modificarlo para tener modelos no isomorfos e incluso que no satisfagan las mismas fórmulas está claro en base a vuestras respuestas, ¿pero como se debe entender lo que he marcado en negrita?
La idea básica de fondo es que un modelo es estándar si sus únicos números naturales son \( 0, 1, 2, \ldots \), mientras que es no estándar si tiene "números naturales infinitos". Por eso digo que dos modelos estándar tienen los mismos números naturales.
Eso no quita para que tengas un contraejemplo como el que te ha puesto geómetracat: si consideras la aritmética de Peano con una constante adicional \( c \), puedes tener dos modelos estándar no isomorfos debido a que interpretan \( c \) de forma distinta, pero eso no contradice la "idea de fondo" según la cual los números naturales de ambos modelos son los mismos "con la \( c \) interpretada de forma distinta".
Supongo que quieres decir que \( M \) y \( N \) son dos modelos estándar de una teoría \( T \) (que satisfaga lo dicho, claro) si, y solo si, los objetos \( a \) de \( M \) tales que \( M \vDash x \in \Bbb[v_x^a] \) están en biyección con los objetos \( b \) de \( N \) tales que \( N \vDash x \in \Bbb[w_x^b] \) (donde \( v, w \) son valoraciones cualesquiera de \( M \) y \( N \) respectivamente).
Si es así como se debe entender, ¿cómo podría expresarse esto de mejor forma como un metateorema y como se demostraría esta equivalencia respecto a la definición que di al principio de modelo estándar?
Sí, eso es. La demostración es trivial. Según la definición que has dado de modelo estándar, un modelo es estándar si para cada \( \xi\in M \) tal que \( M\vDash x\in \mathbb N[v_x^\xi] \) existe un número natural \( n \) tal que \( M\vDash x = 0^{(n)}[v_x^\xi] \), pero esto es lo mismo que decir que \( \xi = M(0^{(n)} \)) y los teoremas que has indicado permiten demostrar que dicho \( n \) es único, así pues los únicos objetos de \( M \) que cumplen \( M\vDash x\in \mathbb N[v_x^\xi] \) son los objetos \( M(0^{(n)}) \), es decir, los objetos denotados por los numerales, luego si tienes otro modelo \( N \), la biyección que buscas es la dada por \( M(0^{(n)})\mapsto N(0^{(n)}) \).
En cuanto a lo de "expresar esto de mejor forma", todo es cuestión de introducir notación. Puedes llamar "números naturales de \( M \)" a los \( \xi\in M \) que cumplen \( M\vDash x\in \mathbb N[v_x^\xi] \) y demostrar que el conjunto \( N_M \) de los números naturales de \( M \) adquiere de forma natural una estructura de modelo del lenguaje de la aritmética (y si supones que en \( T \) pueden demostrarse los axiomas de Peano, entonces \( N_M \) es un modelo de AP). Lo que dice tu teorema es que dos modelos estándar de \( T \) dan lugar a modelos isomorfos \( N_M \), y si en \( T \) se demuestran los axiomas de Peano, entonces dan lugar a dos modelos isomorfos de AP.
Cuando digo que en \( T \) se pueden demostrar los axiomas de Peano, quiero decir que existen términos \( x+y \), \( x\cdot y \) tales que en \( T \) se demuestra:
\( \forall xy\in \mathbb N\, x+y\in \mathbb N \), \( \forall xy\in \mathbb N\, xy\in \mathbb N \),
así como que la suma y el producto satisfacen las definiciones recurrentes usuales, y además se demuestra el principio de inducción, al menos para fórmulas aritméticas, es decir, para fórmulas construidas a partir de \( 0, x', x+y, xy \).
Por otra parte, si fijamos una teoría concreta como es la aritmética de Peano, donde únicamente tenemos el designador \( 0 \), ¿en este caso se da la unicidad del modelo estándar?
Si fijas concretamente la aritmética de Peano el modelo estándar es único, pero si fijas otra teoría aritmética concreta, aunque sólo tengas el designador \( 0 \), el modelo estándar ya no tiene por qué ser único, pero por la clase de "trucos" que ha empleado geómetracat en su respuesta. Por ejemplo, basta con que tengas un relator para que puedas interpretarlo de forma distinta en distintos modelos estándar.