Abstracción del argumento general de forzamiento a partir de argumentos específicos de cada caso

Question

Me he preguntado si la literatura tiene una abstracción de lo que muestra el argumento del forzamiento en general, con el fin de separarlo de los argumentos específicos de cada caso que dan lugar a resultados específicos de independencia. Lo que estoy pensando sería algo en la línea de:

Supongamos que $T$ es una teoría sobre el lenguaje de ZFC + símbolos de función nula $\mathbb{P}, \le$ tal que $T \vdash ZFC$ y $T \vdash$ $(\mathbb{P}, {\le})$ es un orden parcial. Definir la teoría correspondiente $T_f$ sobre el lenguaje de ZFC + símbolos de función nula $\mathbb{P}, \le$ + un predicado unario $\cdot \in M$ + un símbolo de función unario $\cdot^G$ consistir en:

• $T^M$
• $\mathbb{P} \in M$ , ${\le} \in M$
• $M$ es transitivo
• $G := \{ (p, \check p) \mid p \in \mathbb{P} \}^G$ es un $M$ -filtro genérico de $\mathbb{P}$
• $\forall x, \exists \tau\in M, x = \tau^G$
• $\forall \sigma, \tau \in M, \sigma^G \in \tau^G \leftrightarrow \exists (p, \sigma') \in \tau, p \in G \wedge \sigma^G = (\sigma')^G$ .
• $\forall \sigma, \tau \in M, \sigma^G = \tau^G \leftrightarrow [\forall (p, \sigma') \in \sigma, p \in G \rightarrow (\sigma')^G \in \tau^G$ y viceversa $]$ .

Entonces $T_f \vdash ZFC$ y si $T$ es coherente, entonces también lo es $T_f$ .

---

Así, la idea de la prueba serían las normas: para la construcción externa, tomar un subconjunto finito apropiado de $T$ construye un modelo contable transitivo $M$ de $T$ encontrar un filtro genérico $G$ de $\mathbb{P}$ y demuestre que $M[G]$ satisface un subconjunto finito de $T_f$ y dado que esto funciona para un subconjunto finito arbitrario de $T_f$ concluimos que $T_f$ es consistente por compacidad. Para la construcción interna, demuestre que $T \vdash (\Vdash \phi)$ para cada axioma $\phi$ de $T_f$ y que dada una demostración formal de $\Gamma \vdash \phi$ en el idioma de $T_f$ tenemos $T \vdash (\Gamma \Vdash \phi)$ .

Y entonces, podremos demostrar resultados generales que serán útiles en los casos concretos. Así, por ejemplo, yo esperaría que $\forall \tau_1, \ldots, \tau_n \in M, \phi(\tau_1^G, \ldots, \tau_n^G) \leftrightarrow \exists p \in G, (p \Vdash \phi(\tau_1, \ldots, \tau_n))^M$ sería un metateorema de $T_f$ . Del mismo modo, podríamos demostrar $T_f \vdash (ORD^M = ORD)$ y el resultado de que si $T \vdash \mathbb{P}$ tiene la condición de cadena contable, entonces $T_f \vdash (\forall \alpha, \beta \in ORD^M, \alpha = \beta \rightarrow (\alpha = \beta)^M)$ .

Y finalmente, por ejemplo en la prueba de que CH es independiente, podríamos establecer $T$ ser $ZFC + (\mathbb{P}, \le) = \operatorname{Fn}(\aleph_2 \times \aleph_0, 2)$ y demostrar que en este caso, $T_f \vdash 2^{\aleph_0} \ge \aleph_2$ .

---

Admito que no estoy seguro de si mi definición de $T_f$ es completa (o incluso lo suficientemente completa como para mostrar las propiedades deseadas), o por otro lado si $T_f$ podría ser redundante (en particular, sospecho que la condición de que $G$ es un $M$ -filtro genérico de $\mathbb{P}$ puede ser redundante). Y podría ser necesaria una variante para el forzamiento definible por ordinal para obtener varios modelos de $ZF + \lnot AC$ . Sólo quería ver si algo como esto se ha escrito antes.

Answer 1

En mi opinión, esto o algo parecido es la forma "correcta" de resumir lo que consigue el forzamiento en general. Supongo que su $T_f$ incluye la definición recursiva de la evaluación de los nombres $\tau^G$ Si no es así, probablemente deberías añadirlo (y puede que haga que algunos de tus axiomas sean redundantes). Además, puede que quieras añadir que todos los ordinales están en $M$ (a menos que sus axiomas ya lo impliquen).

Más concretamente, yo plantearía el hecho general básico sobre el forzamiento de la siguiente manera (porque prefiero los modelos con valores booleanos para la teoría general): Sea $B$ sea el álgebra booleana abierta regular de $\mathbb P,\leq$ . Entonces la construcción habitual del universo booleano-valorado proporciona una $B$ -interpretación valorada de $T_f$ en $T$ .

Este resultado puede aplicarse de varias maneras: (1) Tal cual, abarca el forzamiento sobre el universo. (2) Aplicado en un $T$ -modelo, proporciona la $B$ -de ese modelo de suelo. A continuación, se puede dividir por un ultrafiltro arbitrario en $B$ para obtener un $2$ -valorado modelo. Si su modelo básico es contable, puede dividir por un ultrafiltro genérico y obtener la construcción habitual de extensiones forzadas de un modelo contable. (3) Dado que la interpretación es sintáctica, se puede utilizar para dar una prueba finita de que, si $T$ es coherente, entonces también lo es $T_f$ .

Por supuesto, como otros han señalado y como ya estaba implícito en su pregunta, cualquier aplicación particular del forzamiento requerirá inventar un método adecuado. $\mathbb P$ para ese fin concreto. La prueba de que su $T_f$ implica la conclusión deseada será entonces esencialmente la misma que la prueba tradicional de que la conclusión deseada es forzada por $\mathbb P$ . Así que este $T_f$ no te ahorra trabajo en problemas concretos, pero (en mi opinión) te da una comprensión más clara de lo habitual de lo que es el forzamiento en general.

Answer 2

(Ignoraré la cuestión de los fragmentos finitos de la teoría - en su lugar, trataré toda la $T_f$ de una vez usando una metateoría más fuerte de lo necesario, y dejarlo como un ejercicio para "fragmentarlo". :P)

El forzamiento puede desarrollarse a lo largo de arbitraria modelos contables. Esto significa que podemos demostrar que $T_f\models ZFC$ y que $T_f$ es coherente si $T$ es simplemente copiando los argumentos habituales, vía Lowenheim-Skolem descendente:

• Para demostrar que $T_f\models ZFC$ supongamos WLOG que $T_f$ es coherente (de lo contrario es trivial). Sea $A$ sea un modelo contable de $T_f$ Entonces $A$ es literalmente un conjunto que fuerza la extensión de su $M$ que es un modelo contable de ZFC y así obtenemos $A\models ZFC$ como siempre.

• Supongamos $T$ es coherente. Sea $M$ sea un modelo contable de $T$ y $\mathbb{P}\in M$ un poset. Dado que $M$ es contable, realmente existe un $G\subseteq\mathbb{P}$ que es $\mathbb{P}$ -generic over $M$ . Construcción $M[G]$ como siempre obtenemos que la expansión obvia de $M[G]$ satisface $T_f$ .

Pero en contra de su título, tenga en cuenta que los teoremas de forzamiento - que estamos usando aquí - no son "caso por caso"; no veo qué generalidad puede tener el $T_f$ -se suma a la habitual. En particular, demostrar la consistencia relativa de $ZFC+\neg CH$ requiere que escribamos la definición adecuada de $Fn(\omega,2)$ (o similar) tanto en un caso como en otro, de modo que las aplicaciones específicas requieren definiciones específicas, mientras que el propio método y los lemas clave son totalmente generales.

Answer 3

El caso es que una vez superado el escollo de las cuestiones metateóricas del forzamiento, simplemente se pasa al "forzamiento sobre el universo", que no es más que trabajar en $V$ , tome un orden parcial, y suponga que de alguna manera, también tiene un $V$ -filtro genérico para su orden parcial, incluso si $V$ se suponía que era el universo de "todos" los conjuntos.

Hay un enfoque utilitarista de las matemáticas que dice que añadir axiomas que simplifiquen un argumento, aunque sean innecesarios, e incluso si la simplificación es "algorítmica", es algo bueno. Esto justifica el uso de la metateoría de la teoría de conjuntos sobre algo tan débil como la Aritmética Recursiva Primitiva, y es una justificación para asumir siempre que tenemos un modelo contable transitivo de cualquier teoría que queramos, si así lo deseamos para hacer nuestro forzamiento.

No es necesario recurrir al truco de Feferman de añadir un nuevo símbolo para un submodelo elemental contable del universo. Para ello, este modelo no va a ser un modelo de $\sf ZFC$ internamente hablando. Y nos parece bien, porque el argumento es metateórico. Entonces, ¿por qué nos molestamos tanto?

De hecho, recordando mis primeros días de uso de los argumentos de forzamiento, el único problema de "sólo forzar sobre el universo" es que puede resultar confuso para los recién llegados. Por eso es importante que tengamos buenos libros que expliquen el forzamiento, y gente que responda a las preguntas en Internet, etc. Pero como he dicho, una vez superado ese obstáculo, las pruebas de forzamiento más claras y directas son simplemente "forzar sobre el universo".