Marco axiomático utilizado para Class Forcing

En Class Forcing, uno inevitablemente tiene que discutir las clases apropiadas como objetos matemáticos concretos.

Por ejemplo, al definir pretameness en la definición 2.2 del Capítulo 8 del Manual, hablamos de una secuencia de clases, que luego enumeramos. Estoy tratando de entender en qué marco axiomático podríamos estar trabajando.

En ZFC no podemos hablar de clases de esta manera. En NBG podemos hablar de clases, pero no podemos cuantificar sobre ellas. Específicamente, si una clase es miembro de otra clase, entonces debe ser un conjunto, por lo que no podemos hablar de una secuencia infinita de ellos. Pero nuestra secuencia está hecha de clases propias. Si subimos a MK, entonces nuestra teoría ya no es una extensión conservadora de ZFC, y no podemos estar realmente seguros de que nuestras conclusiones sobre los conjuntos sean válidas en ZFC.

Alternativamente, podríamos tratar de justificar nuestra discusión trabajando dentro de V k , para algunos k cardenal inaccesible. Entonces todas nuestras molestas clases se convierten en conjuntos. Pero esto presupone la existencia de tal cardenal, del cual no creo que dependa realmente la teoría del forzamiento de clases.

¿En qué marco axiomático estamos trabajando cuando discutimos el forzamiento de clases?

Solo un comentario menor, si te sientes más cómodo con V k para un cardenal inaccesible que con Kelley-Morse, entonces lo estás haciendo al revés. Desde V k + 1 sería un modelo de Kelley-Morse, esto significa que la suposición es más fuerte desde un punto de vista fundacional.

Respuestas (1)

En primer lugar, puede cuantificar las clases en NBG. De lo contrario, no sería una gran teoría de conjuntos habilitada por clases. Sin embargo, lo que no puede hacer es usar Comprensión con cuantificadores de clase.

Tenga en cuenta que, al igual que en ZFC, si puede indexar sus clases de manera uniforme, entonces lo que tiene es una clase { i , v i I , φ ( v , i ) } dónde φ es una definición uniforme (por ejemplo, un modelo de suelo se puede definir de manera uniforme con la variación de los parámetros). En ese caso, el i La clase se obtiene simplemente tomando { X φ ( v , i ) } . Ciertamente es un objeto de la teoría, y la Comprensión está dentro del poder de NBG (e incluso ZFC, si considera las clases como objetos formales).

Entonces, ciertamente puede usar NBG para formalizar el forzamiento de clases. Siempre que esté cuantificando sobre clases, si es necesario, esto puede convertirse en un esquema-teorema. Es decir, un teorema en el que hay un cuantificador universal metateórico, pero la teoría (en este caso, NBG) prueba todos los casos. Esta situación es similar a la prueba de que L es un modelo de ZFC, que es en sí mismo un esquema-teorema.


En cualquier caso, ha habido mucho trabajo reciente sobre el tema. Puede comenzar consultando los siguientes documentos:

  1. The Ground Axiom , la tesis doctoral de Jonas Reitz que incluye un apéndice con el marco para el forzamiento de clases.

  2. Forzamiento de clases, teorema de forzamiento y compleciones booleanas , por Peter Holy, Regula Krapf, Philipp Lücke, Ana Njegomir, Philipp Schlicht.

  3. Caracterizaciones de pretameness y el Ord-cc , por Peter Holy, Regula Krapf, Philipp Schlicht.

  4. Condiciones suficientes para el teorema de forzamiento y conversión de clases propias en conjuntos , por Peter Holy, Regula Krapf, Philipp Schlicht.

  5. La fuerza exacta del teorema de fuerza de clase , por Victoria Gitman, Joel David Hamkins, Peter Holy, Philipp Schlicht, Kameryn Williams.

No estoy seguro de entender su declaración sobre las clases en NBG. De acuerdo con la axiomatización que he visto, la membresía solo se define para un conjunto en una clase, no para clases en una clase. Entonces, ¿cómo podemos discutir un conjunto de clases, o incluso una clase de clases?
מה הקשר בין מחט לתחת? :)
Aceptar Asaf :). Tienes razón en la cuantificación, no leí bien la fuente. Pero mi principal problema sigue siendo ¿cómo se puede hablar de la secuencia de clases?
Bueno, ¿dónde exactamente quieres hablar sobre una secuencia de clases?
Bueno, en mi tesis :). Más concretamente, estoy tratando de trabajar con una 'colección de modelos internos' de V, y no es fácil...
@AlonNavon: Dada una clase I , puede definir un I -familia indexada de clases para ser solo una subclase S de I × V , donde la clase correspondiente a i I es { X : ( i , X ) S } .
@Alon: Sí, las colecciones de modelos internos no son algo fácil de cuantificar. Si son todos terrenos, o parte del multiverso genérico de uno fijo, entonces podemos hacerlo. Pero de lo contrario, no hay una forma clara de cuantificar esa clase en NBG.
@Alon: una salida es tener un "teorema de plantilla". Es un teorema que cada vez que conectas una clase que tiene tales y tales propiedades (por ejemplo, un modelo interno), entonces puedes probar algo. Entonces la cuantificación sobre una colección de modelos internos está en la meta-teoría. Pero aún obtienes los resultados, en su mayor parte.
@AsafKaragila ¿Qué es exactamente un "teorema de plantilla"? Traté de buscarlo, pero, naturalmente, todo lo que obtuve fueron plantillas matemáticas de Lyx. :)
@Alon: No es un término real. Significa que la cuantificación está en el metateorema. Algo así como podemos probar que para cada axioma de ZFC, se cumple en L. La prueba general es la misma, pero en última instancia es un teorema de plantilla: ZFC prueba cada instancia, pero no de manera uniforme.
@EricWofsey Lo que estás diciendo es construir una clase de pares ( i , X ) , hasta ahora todo bien, y luego usar la comprensión de clase cada vez que queramos referirnos a una clase en particular. Eso es bastante bueno. Incluso podría ser suficiente para mi problema.
@Alon: Iba a hacer ese comentario como lo hizo Eric. Pero es un poco obvio... aparentemente no lo suficientemente obvio. :PAG
@AsafKaragila Con respecto a la pregunta original, ¿básicamente dice que usamos NBG y volvemos a llamar a la metateoría cada vez que surge la necesidad? ¿No es eso un poco sospechoso? Es bueno que haya un truco simple para trabajar con clases indexadas, pero ¿es eso suficiente?
@Alon: No, está bien. Lo hacemos todo el tiempo en la lógica. Por ejemplo, cuando codificamos la lógica en los números naturales en PA, primero lo hacemos en la metateoría y luego decimos "¡Oh, oye, en realidad PA ya prueba todo eso!".
Está bien, aceptaré la respuesta, pero creo que deberías aclarar la respuesta.
@Alon: Estaré encantado de aclarar. Pero no estoy completamente seguro de qué. Siento que hiciste una pregunta (que es válida), pero en realidad querías hacer una pregunta completamente diferente.
Esperaba algún tipo de respuesta de sistema bien definida, como "NBG" o "MK". Si tenemos que apelar a la metateoría, entonces eso debería establecerse explícitamente.
@Alon: ¿Eso es mejor?
Simplemente perfecto. :)