¿Qué es realmente el poset genérico utilizado en el forzamiento?

Question

No soy teórico de conjuntos, pero entiendo la versión 'pop' del forzamiento teórico de conjuntos: por analogía con el álgebra, podemos tomar un modelo de una teoría de conjuntos, y un 'indeterminado' (que es algún poset), y añadirlo a la teoría y luego completar a un modelo con las propiedades deseadas. Entiendo mejor la versión de la teoría de categorías, que consiste en tomar gavillas (valoradas en una categoría dada $Set$ ) sobre dicho poset con una topología de Grothendieck dada (la topología de la doble negación). El topos resultante es de nuevo un modelo de la teoría de conjuntos, pero ahora tiene las propiedades que usted desea, ausentes del original $Set$ .

Pero, ¿qué es este poset, ¿en serio? ¿Es el conjunto de subobjetos del conjunto que quieres añadir a tu teoría/modelo (digamos un conjunto de una cardinalidad específica, o algún árbol con una propiedad)? ¿Está relacionado con una prueba de la propiedad que te interesa? Para aclarar, no estoy interesado en la definición mecánica de un poset genérico apropiado, sino en lo que es moralmente. Puntos extra por decir lo que "es" antes y después de forzar, si es que tiene sentido.

Answer 1

Las otras respuestas son excelentes, pero permítanme aumentarlas con una explicación intuitiva del tipo que usted parece buscar. buscar.

En la mayoría de los argumentos de forzamiento, la idea principal es construir un orden parcial de condiciones que consisten cada una en una pequeña parte del objeto genérico que nos gustaría añadir; cada condición debe hacer una pequeña promesa sobre cómo será el nuevo será el nuevo objeto genérico. En efecto, el filtro genérico proporciona una forma de agrupar estas promesas en un coherente con las propiedades deseadas.

Por ejemplo, con el forzamiento de Cohen $\text{Add}(\omega,\theta)$ queremos añadir $\theta$ Muchos nuevos subconjuntos de $\omega$ con el fin de violar CH, por ejemplo. Así que condiciones que especifican un número finito de bits en un $\omega\times\theta$ matriz de ceros y unos. Cada condición de condición hace una promesa finita sobre cómo se completará la matriz completa. La unión de todas las condiciones en el filtro genérico es un relleno completo de la matriz. La genericidad garantiza que cada columna de esta matriz es un nuevo real no presente en el modelo básico y diferente de todas las demás columnas, ya que cualquier condición finita se puede condición finita puede extenderse de modo que no coincida con cualquier real particular o de cualquier otra columna particular.

Con el colapso forzando $\text{Coll}(\omega,\kappa)$ Nosotros queremos añadir una nueva función suryectiva $f:\omega\to\kappa$ . Así que utilizamos condiciones consistentes en las funciones parciales finitas finitas $p:\omega\to\kappa$ ordenados por extensión. Cada condición es una pequeña parte de la función genérica que queremos añadir, describiendo finitamente mucho de ella. La unión de el filtro genérico proporciona una función total $g:\omega\to \kappa$ y la genericidad del filtro garantizará que $g$ es suryectiva, ya que para cualquier $\alpha<\kappa$ cualquier condición $p$ puede ampliarse a una condición más fuerte teniendo $\alpha$ en el rango.

Y lo mismo con muchos otros argumentos de forzamiento. Diseñamos el orden parcial para que consista en pequeñas piezas del objeto que estamos intentando añadir, cada uno de los cuales hace una pequeña promesa sobre el objeto genérico. Si $G$ es un genérico para este orden parcial, entonces la unión de $G$ es la conjunto de todas estas promesas.

En muchos argumentos forzados, no basta con construir un orden parcial formado por pequeños fragmentos del objeto deseado, ya que también se quiere saber si el forzamiento conserva otras características. Por ejemplo, queremos saber que el forzamiento no colapsa cardinales inadvertidamente o que se puede iterar sin colapsar cardinales. Este Esto añade una arruga a la idea anterior, ya que uno quiere utilizar pequeños trozos del objeto genérico, pero imponer otros requisitos sobre las condiciones que garanticen que el orden parcial tiene una buena condición de cadena o es adecuado y etc. Así que el diseño de una noción de forzamiento es a menudo una entre estos requisitos: hay que encontrar un un equilibrio entre las piezas del objeto genérico deseado objeto genérico deseado y asegurar que el orden parcial tiene propiedades agradables suficientes para que no destruya demasiado. demasiado.

En este sentido, diría que la parte difícil de la mayoría de los de los argumentos de forzamiento no es el dominio de la de forzamiento, la construcción del filtro genérico y de del modelo, aunque ese aspecto del forzamiento no es no es trivial, sino más bien el diseño detallado del orden parcial para lograr el efecto deseado.

Answer 2

En términos topos-teóricos, me gusta describir el forzamiento de la siguiente manera. Se considera un teoría geométrica cuyos modelos son los objetos que desea unir. Por ejemplo, si se quiere unir una inyección de un conjunto A a un conjunto B, entonces se considera la teoría geométrica proposicional cuyas proposiciones básicas son de la forma $[f(a)=b]$ "para unos a∈A y b∈B, y cuyos axiomas son

• $\vdash \bigvee_b [f(a)=b]$ para cada a (es decir, "f está definida en todas partes")

• $[f(a)=b_1]\wedge [f(a)=b_2] \vdash \bot$ siempre que $b_1\neq b_2$ ("f es monovaluada")

• $[f(a_1)=b] \wedge [f(a_2)=b] \vdash\bot$ siempre que $a_1\neq a_2$ ("f es inyectiva")

Si A tiene una cardinalidad mayor que B, entonces esta teoría no tiene modelos en Set. Pero aún podemos considerar su topos clasificatorios que puede no tener puntos. Como el topos clasificador de cualquier teoría, este topos clasificador contiene un "modelo universal" de la teoría (si se quiere, por el lema de Yoneda-un objeto representativo x de cualquier functor F está determinado por un elemento universal de F(x)).

Una forma conveniente de construir el topos clasificador de una teoría geométrica proposicional es considerar el conjunto de conjunciones finitas de fórmulas básicas (que es la categoría libre finitamente completa generada por la teoría) y equiparlo con una topología de Grothendieck procedente de los axiomas. En el ejemplo anterior, una conjunción finita de proposiciones básicas es una relación finita de A a B. Podemos descartar las que no son de un solo valor e inyectivas, ya que los axiomas nos dicen que están cubiertas por la familia vacía; así obtenemos un conjunto de "inyecciones parciales", parecidas a las que suelen mencionar los teóricos de conjuntos.

Por último, si eres un teórico clásico de conjuntos y quieres tener también la ley del medio excluido, puedes considerar un subtopos booleano de este topos clasificador. Un topos booleano obvio es el topos de las láminas de doble negación en el conjunto anterior. Tanto éste como el topos clasificador son subtopos del topos de las gavillas en el poset, y si tienes suerte (no conozco las condiciones exactas necesarias), entonces el subtopos de la doble negación estará contenido en el topos clasificador, y por tanto también contendrá un modelo de la teoría en cuestión (ya que tiene un mapa al topos clasificador de la teoría).

Answer 3

Permítanme añadir un punto de vista que no se ha mencionado anteriormente, a saber, el de los modelos con valor booleano. Todo poset tiene una terminación, que es un álgebra booleana completa.
Para cada poset podemos definir un lenguaje de forzamiento que esencialmente parece de primer orden sólo que usamos los llamados nombres (que dependen del poset y representan elementos de la extensión forzada) como constantes.
Ahora los elementos del álgebra booleana completa pueden considerarse valores de verdad de enunciados en el lenguaje de forzamiento.
Los filtros genéricos del poset y su terminación están en correspondencia 1-1 entre sí.
Un filtro en el álgebra booleana completa corresponde a una teoría consistente en el lenguaje de forzamiento.

Así, elegir un filtro genérico para el poset sobre un modelo de teoría de conjuntos corresponde a elegir una teoría "genérica" en el lenguaje de forzamiento, la teoría que consiste en enunciados en el lenguaje de forzamiento que son verdaderos en la extensión genérica correspondiente.

En realidad, con este planteamiento ni siquiera es necesario acudir realmente a una extensión genérica Si quieres demostrar que CH no es demostrable en ZFC, todo lo que necesitas hacer es construir un poset de modo que en el correspondiente lenguaje de forzamiento todos los axiomas de ZFC tengan valor de verdad 1 en el álgebra booleana completa correspondiente y CH no.
Como todo lo que se sigue de ZFC tiene también valor de verdad 1, CH no se sigue de ZFC. Ahora, por supuesto, los cálculos y argumentos que tienes que hacer para llevar a cabo este programa son tan difíciles como en el caso del enfoque habitual.

Answer 4

Esto es más fácil de entender en términos de locales. La localidad de doble negación asociada a un forzamiento es el espacio en el que vive el filtro genérico. El problema es que los locales de doble negación no triviales no tienen puntos, por lo que hay que adosar uno para formar la extensión genérica.

En otras palabras, si $X$ es la localidad de doble negación con la que queremos forzar, nos gustaría tener un par de morfismos geométricos $Set \to Sh(X) \to Set$ . La segunda parte $Sh(X) \to Set$ no es ningún problema, pero la primera parte $Set \to Sh(X)$ normalmente no existe. Así que ampliamos un poco el universo de conjuntos añadiendo un punto genérico a $X$ . Tenga en cuenta que la locale de doble negación $X$ se destruye en el proceso final de generación de la extensión genérica.