¿Son conservadoras las anotaciones en ZF?

Question

En la lógica de primer orden con los axiomas de Zermelo-Fraenkel, es conveniente introducir notaciones para los conjuntos que probamos que existen y son únicos. Por ejemplo la unión de dos conjuntos, ZF demuestra que: $$\forall a \forall b\; \exists! u \;\forall t, \; t\in u \Leftrightarrow (t \in a \lor t \in b) $$ Por lo tanto, observamos $u = a \cup b$ . Esto significa que introducimos un símbolo de operador binario $\cup$ con un axioma derivado del teorema anterior. Es fácil demostrar que cualquier modelo de ZF puede extenderse a un modelo de ZF $+\cup$ interpretando $\cup$ como una función que mapea $(a,b)$ al único $u$ arriba.

Sin embargo, hay un fallo en el esquema del axioma de sustitución. Con el nuevo símbolo introducido $\cup$ Hay más fórmulas que pueden entrar en el esquema de sustitución, para producir más axiomas. El razonamiento anterior no comprobó que estos nuevos axiomas son satisfechos por el modelo extendido.

Si dejamos la unicidad y empezamos con este otro teorema de ZF : $\forall a, \; a\neq \emptyset \Rightarrow \exists u, u \in a$ , entonces introduce el símbolo asociado Choice $(a)$ con el siguiente axioma, $$ \forall a, \; a\neq\emptyset \Rightarrow \text{Choice}(a) \in a $$ es fácil derivar el axioma de elección de eso. Añadir el símbolo de elección y su axioma a ZF es consistente, pero no conservador.

¿Hay alguna prueba de que ZF más las operaciones habituales (conjunto vacío, unión, intersección, conjunto de potencias, pares de conjuntos, tuplas, productos cartesianos, ...) es una extensión conservadora de ZF con sólo el símbolo de pertenencia $\in$ ?

Answer 1

Esto es sencillo: cualquier fórmula puede sustituirse por otra sin ninguno de los nuevos símbolos. Por ejemplo, dada una fórmula en el lenguaje ampliado con $\cup$ se puede obtener una fórmula equivalente haciendo las siguientes sustituciones:

• Cada vez $s\cup t=u$ o $u=s\cup t$ aparece (para los términos $s,t,$ y $u$ ), sustitúyalo por $\forall x (x\in u\leftrightarrow(x\in s\vee x\in t))$ .
• Cada vez $s\in t\cup u$ sustitúyalo por $s\in t\vee s\in u$ .
• Cada vez $s\cup t\in u$ sustitúyalo por $\exists x(x=s\cup t\wedge x\in u)$ .

Aquí $s,t,$ y $u$ son términos, y $x$ es una variable que no aparece en $s,t,$ o $u$ . Tenga en cuenta que puede ser necesario iterar estas sustituciones para eliminar todos los usos de $\cup$ (por ejemplo, la tercera regla introduce $x=s\cup t$ que debe ser eliminado utilizando la primera regla, y si un término anidado como $(x\cup y)\cup z$ aparece en la fórmula, las reglas se utilizarán primero para eliminar el $\cup$ y luego para eliminar el interior $\cup$ ). Una inducción directa sobre las fórmulas muestra que cada fórmula del lenguaje ampliado con $\cup$ es equivalente a la fórmula de sustitución.

Así, en particular, si $\varphi$ es cualquier fórmula del lenguaje ampliado con $\cup$ la instancia de Reemplazo utilizando $\varphi$ es equivalente a la instancia de Reemplazo utilizando la fórmula $\varphi'$ que se obtiene al eliminar $\cup$ de $\varphi$ como en el caso anterior. Dado que la sustitución de $\varphi'$ está incluido en ZF, esto significa que el nuevo axioma de sustitución para $\varphi$ es cierto en el modelo con $\cup$ extendida de cualquier modelo de ZF.

(Otra forma de decir esto es que el reemplazo es realmente una declaración sobre todo definible funciones en cualquier modelo. Añadir nuevos símbolos al lenguaje para funciones que ya eran definibles no hará que se puedan definir nuevas funciones).