Ciertamente, ZFC $\vdash$ Con(ZF) $\rightarrow$ Con(ZF+ $\lnot$ AC), pero el argumento habitual de forzamiento para construir un modelo de ZF+ $\lnot$ AC parece requerir la elección para encontrar un filtro genérico.
Respuestas
¿Demasiados anuncios?Esto tiene una solución sencilla, casi una excusa: el absolutismo.
Nótese que el enunciado es, de hecho, un enunciado de primer orden en el lenguaje de la aritmética. Y dicho enunciado es demostrable a partir de $\sf ZF$ si y sólo si es demostrable a partir de $\sf ZFC$ .
Como sabes lo segundo, en realidad sabes lo primero.
Aunque en realidad, basta con verificar lo siguiente en $\sf ZF$ :
-
El teorema de exhaustividad se mantiene para los lenguajes contables sin elección. Por lo tanto, si $\sf ZFC$ es consistente, tiene un modelo.
-
Las extensiones forzadas y simétricas funcionan sin utilizar el axioma de elección.
Así que si $\sf ZFC$ es consistente, tiene un modelo contable, donde el forzamiento funciona como siempre, las extensiones simétricas funcionan como siempre, y por lo tanto si hay un modelo de $\sf ZF$ hay uno en el que el axioma de elección falla.
También hay que añadir que el axioma de elección no es realmente necesario para encontrar un filtro genérico sobre un modelo transitivo contable. La razón es que el modelo es de hecho contable, por lo que los elementos del conjunto forzado dentro del modelo forman un conjunto contable externo. Utilizando este hecho, así como el hecho de que sólo hay contablemente muchos conjuntos densos en el modelo podemos definir un filtro genérico recursivamente sin apelar al axioma de elección.
Dado que AC se mantiene en $\mathbf L$ ZF demuestra que "Con(ZF) $\to$ Con(ZF+ $\neg$ AC)" relativizado a $\mathbf L$ . Pero la declaración de consistencia relativa es una declaración aritmética, y $\mathbf L$ tiene los mismos ordinales (y en particular los mismos enteros) que el universo circundante, por lo que Con(ZF) $\to$ Con(ZF+ $\neg$ AC) es absoluta.