Cómo definir Conway clase de todos los juegos rigurosamente?

Question

Estoy leyendo a John Conway En Números Y Juegos.

En el curso de la definición de la surrealista números, Conway define el término juego más o menos como sigue.

• $(\emptyset,\emptyset)$ es un juego.
• Si $L$ $R$ son conjuntos cuyos elementos son los juegos, a continuación, $(L,R)$ es un juego.
• Todos los juegos están construidos de esta forma.

Obviamente esta es una definición informal, por lo que me gustaría ver un formalizado versión. Sin embargo, la "solución" a este problema que se tratan en el Apéndice de la Parte 0 no tiene sentido para mí.

Alguien puede proporcionar una definición formal del predicado $\mathrm{Game}$ que devuelve true si la entrada es un juego?

Tenga en cuenta que el problema aquí es muy distinta de la cuestión debatida aquí: son surrealista números en realidad bien definida en ZFC?.

---

Lo que he intentado hasta ahora. Es tentador para proceder como sigue. Definir que una clase de $C$ es cerrado iff siempre $L$ $R$ son conjuntos con $L,R \subseteq C,$$(L,R) \in C.$, Entonces la clase de juegos se define como la intersección de todos los cerrados de las clases de la incorporación de $(\emptyset,\emptyset)$.

Hay un par de problemas con esta. En primer lugar, en ZFC, no tenemos clases, sólo los predicados. Así que, ¿cómo hacemos un refrito con la noción de la intersección de todos los cerrados de clases en términos de predicados? Es incluso posible? Estoy dispuesto a utilizar NBG o MK si es estrictamente necesario, pero creo que no lo es.

En segundo lugar, ¿cómo sabemos que existe un cerrado de la clase? No queremos utilizar la jerarquía acumulativa para la construcción de una clase, porque el punto de Conway enfoque es que tenemos los ordinales de forma gratuita como un subconjunto de la surreals.

---

Edit. En los comentarios, se mencionó que $\in$-recursividad hace Conway definición rigurosa. Alguien puede explicar precisamente cómo se hace?

Por ejemplo, no $\in$-recursividad nos permiten definir "juego", mediante la afirmación de que $x$ es un juego iff existen conjuntos de $L,R$ tal que $(L,R)=x$ y los elementos de $L$ $R$ son juegos.

Answer 1

He aquí una definición de la noción de "juego" en ZF; esencialmente, se trata de re-hacer, para este ejemplo en particular, la técnica general para la eliminación de la recursividad en favor de definiciones explícitas.

Voy a comenzar con un auxiliar de definición, que voy a llamar "pruebas"; la intuición es que un conjunto de pruebas si contiene suficiente información para verificar que cada uno de sus elementos es un juego. Formalmente, un conjunto $E$ se evidencia si se trata de un conjunto de pares ordenados y, para cada par $(L,R)\in E$ ambos $L$ $R$ son conjuntos y todos sus miembros están también en $E$. [Técnicamente, podría omitir la cláusula "tanto en $L$ $R$ son conjuntos," porque en ZF todo es un conjunto, pero creo que la definición es más fácil de entender con que la cláusula incluida.] Tenga en cuenta que esta es una explícita definición de lo que significa para un conjunto de pruebas.

Ahora definir un conjunto $G$ a ser un juego de iff es un miembro de algún $E$ que es la evidencia.