La respuesta es que no podemos escribir una fórmula que seguramente define un buen orden de R ZFC (al menos suponiendo que ZFC es consistente), aunque no sé cuya crédito por ello.
Supongamos que φ(x,y) seguramente define un bijection de R con un ordinal (esto es equivalente a la forma de estado, sólo lo que es más fácil trabajar con él más adelante). Tenga en cuenta que ZF demuestra que cada pedido tiene un único isomorfismo con un único ordinal, por lo que no depende de nada.
Deje M ser una contables transitiva modelo [de suficiente axiomas] de ZFC. Considere la posibilidad de obligar a la que se añade una Cohen real. Las condiciones de esta obligando son finitos funciones de p:ω→2 (aquí nos referimos a funciones parciales, por supuesto), ordenado por la inversa de la inclusión.
Denotar por ˙c={(p,ˇk)∣p(k)=1} el nombre canónico de los Cohen real. Deje G M- filtro genérico, y deje c denotar la interpretación de nuestros Cohen real por G.
En M[G] hay algo de α tal que M[G]⊨φ(c,α), por lo que para algunos p∈G tenemos que p⊩.
Ahora elija cualquiera de los m,n\notin\operatorname{dom}(p) y considerar la permutación de \omega que es el ciclo de (m\ n). Esta permutación es en M, y se puede aplicar a las condiciones de la forzamiento (por la acción \pi p(\pi n)=p(n)). Así que podemos pensar en ello como un automorphism de la forzando. Algunos hechos básicos:
- Un automorphism de la obligando extiende de manera única a un automorphism de los nombres.
- p\Vdash\phi(\dot x) si y sólo si \pi p\Vdash\phi(\pi\dot x) por un automorphism \pi.
- En el Cohen forzar, si \pi es un automorphism inducida como el anterior por una permutación de \omega, y no es la identidad automorphism, a continuación,1\Vdash\pi\dot c\neq\dot c.
- Si x\in M, \pi\check x=\check x donde \check x es el nombre canónico de x.
Ahora tenemos que \pi p\Vdash\varphi(\pi\dot c,\pi\check\alpha). Pero \pi p=p, y por lo tanto p\Vdash\varphi(\pi\dot c,\check\alpha). Lo cual es una contradicción ya que ahora p\Vdash\varphi\text{ defines an injective function}\land\pi\dot c\neq\dot c\land\varphi(\dot c,\check\alpha)\land\varphi(\pi\dot c,\check\alpha).