Definiciones existenciales en ZFC

Una vez que especifica una condición, la unicidad sigue por extensionalidad. Y dado que podemos probar eso, no tiene mucho sentido usar$\exists!y$en el enunciado del axioma, porque$\exists!$no es un cuantificador estándar, sino más bien una declaración abreviada de una fórmula mucho más complicada.

Ahora, quieres hablar sobre funciones de clase como$\mathcal P(\cdot)$o constantes como$\varnothing$o$\omega$. Y esa es una preocupación válida, ya que el lenguaje de la teoría de conjuntos solo tiene la$\in$símbolo.

Introduzca la noción de una extensión conservadora. En lógica, si tienes un idioma$\cal L$y una teoria$T$, y tienes una fórmula$\varphi(x)$tal que$T$demuestra que$\varphi(x)$define un conjunto único, entonces podemos extender el lenguaje a$\cal L^+$añadiendo un símbolo constante$c_\varphi$y el axioma$\varphi(c_\varphi)$.

Ahora podemos demostrar que cualquier modelo de$T$puede interpretarse naturalmente como un modelo para$T+\varphi(c_\varphi)$como una interpretación para el lenguaje$\cal L^+$. Del mismo modo, podemos hacer eso con funciones o relaciones definibles. Y además, cada prueba de$T+\varphi(c_\varphi)$en$\cal L^+$se puede traducir a una prueba de$T$en el idioma$\cal L$.

Y eso es lo que realmente está pasando. En efecto, ampliamos el lenguaje de la teoría de conjuntos para incluir muchos "símbolos convenientes", y sabemos que podemos traducir recursivamente todos los enunciados y demostraciones del lenguaje ampliado al lenguaje original de la teoría de conjuntos con solo$\in$.

Parece haber cierta incertidumbre en cuanto a lo que está preguntando exactamente, pero tal vez esta sea una respuesta a su pregunta.

Si desea utilizar únicamente abreviaturas del tipo utilizado para$A\subset B$, la respuesta es que no intentas traducir términos de forma aislada; intentas traducir las fórmulas en las que aparecen. Dado que las fórmulas bien formadas de la teoría de conjuntos se forman inductivamente a partir de fórmulas atómicas de la forma$\alpha\in\beta$y$\alpha=\beta$, eso significa que si queremos "traducir$\{x:\varphi\}$"Solo tienes que averiguar qué"$\{x:\varphi\}\in\alpha$," "$\alpha\in\{x:\varphi\}$," y "$\alpha=\{x:\varphi\}$" deberían ser abreviaturas de. Aquí hay una versión que funciona adecuadamente en ZF:

• Para$\alpha\in\{x:\varphi\}$, podemos decir que es un sinónimo de$\exists y(\alpha\in y\wedge\forall z(z\in y\leftrightarrow\phi))$.
• Para$\{x:\varphi\}\in\alpha$, decimos que esto es solo la abreviatura de$\exists y(y\in\alpha\wedge y=\{x:\varphi\})$.
• y para$\alpha=\{x:\varphi\}$nos referimos al primer punto y extensionalidad, traduciéndolo como$\forall y(y\in\alpha\leftrightarrow y\in\{x:\varphi\})$.

Si seguimos desempaquetando cualquier fórmula que contenga resúmenes de conjuntos de esta manera, eventualmente los reduciremos a fórmulas en las que los únicos términos son variables y la fórmula atómica son aquellas que involucran$\in$y$=$. Sin embargo, estas fórmulas se vuelven realmente largas y feas; afortunadamente, por las razones que da Asaf, en realidad no tenemos que tener cuidado con esto siempre que nuestros axiomas garanticen la existencia de un conjunto de todas las cosas que satisfacen la propiedad$\varphi$--podemos tratarlos como términos atómicos y continuar.

En el lenguaje de ZFC no existen constantes ni símbolos funcionales, por lo que los únicos términos son variables. Una forma de lidiar con las definiciones es ignorar la posibilidad de introducir nuevos símbolos e imaginar que cada fórmula que usa definiciones es una abreviatura de una fórmula en el lenguaje de ZFC. Las definiciones se pueden considerar como una forma informal pero precisa de cómo escribir fórmulas más cortas y más legibles en lugar de fórmulas muy largas. Debe quedar claro cómo traducir una fórmula que contiene símbolos definidos en una fórmula en el lenguaje ZFC puro.

Por ejemplo,$A\subset B$se puede traducir a$(\forall x)(x\in A\Rightarrow x\in B)$y una fórmula que contiene$\subset$en algún lugar dentro se traduce reemplazando apropiadamente cada subfórmula de la forma$A\subset B$. De manera similar para cualquier símbolo de predicado definido$P(x_1,\dots,x_n)$.

En cuanto a los símbolos de funciones definidas, todo lo que necesitamos es saber cómo traducir una fórmula de la forma$y=F(x_1,\dots,x_n)$, esto se reemplaza por la fórmula$\varphi(y,x_1,\dots,x_n)$utilizado como una definición de$F$. Entonces también sabemos traducir$y\in F(x_1,\dots,x_n)$: lo reemplazamos por$(\exists z)(y\in z\wedge\varphi(z,x_1,\dots,x_n))$. Del mismo modo podemos traducir$F(x_1,\dots,x_n)\in y$. El hecho de que para cualquier$x_1,\dots,x_n$hay exactamente uno$y$satisfactorio$\varphi(y,x_1,\dots,x_n)$puede considerarse como un "conocimiento previo", no es necesario codificarlo directamente en la traducción.

Por cierto,$\{x\in A\!:x\in B\}$también es una abreviatura que debe traducirse a un lenguaje ZFC puro; fórmula$y=\{x\in A\!:x\in B\}$por supuesto es reemplazado por$(\forall x)(x\in y\Leftrightarrow(x\in A\wedge x\in B))$.

Al ver sus comentarios a la respuesta de Asaf, creo que otra forma de resolver su problema sería con otro punto de vista: pensar en términos de cálculo secuencial (clásico).

Suponga que desea probar el teorema "Para cualquier conjunto$A$, existe$B$tal que hay una inyección$A\to B$, y sin sobreyección$A\to B$". La opción habitual para probar este teorema es usar$B=P(A)$. Pero, ¿cómo escribir esto formalmente?

Cuando haces tu cálculo de secuencias, en algún momento llegas a$ZF\vdash \exists B, \phi_P(A,B)$dónde$\phi_P(x,y)$es una abreviatura de la fórmula "$y$es el conjunto de potencia de$x$".

En este punto piensas "Deja$B$ser el poder de$A$", y su prueba de deducción natural continúa con$ZF, \phi_P(A,B)\vdash ...$" donde "..." es algo que debe ser.

Cuando llegas a "$ZF, \phi_P(A,B)\vdash$hay una inyección$A\to B$y sin sobreyección$A\to B$", puede usar una de las reglas de inferencia del cálculo secuencial:

De$\Gamma, \phi(t)\vdash \psi$($t$no gratis en$\Gamma$) y$\Gamma \vdash \exists x, \phi(x)$, inferir$\Gamma\vdash \psi$.

aplicar esto a$\phi(x) = \phi_P(A,x)$, y$\psi = \exists y, \Omega(y)$dónde$\exists B, \Omega(B)$es la fórmula que estamos tratando de probar, finalmente obtienes$ZF\vdash \exists B, \Omega(B)$. Usando la generalización,$ZF\vdash \forall A, \exists B, blabla$.

Así que hemos usado el powerset de$A$en una prueba formal, pero la cosa es que puedes nombrarla (almacenarla en cierto sentido) como una variable no usada, poniendo su definición del lado de las hipótesis, y usando la variable (ahora usada) en la prueba, usando su definición en varios puntos de la demostración.

Eso es si quieres usar el objeto definido para probar algo más. Si desea probar algunas propiedades del objeto definido, hay cosas similares que puede hacer, por ejemplo, en lugar de probar$\forall A, |P(A)|>|A|$puedes probar$\forall A, \forall B, \phi_P(A,B)\implies |B|>|A|$etc. Como solo hay uno$B$tal que$\phi_P(A,B)$, este último teorema es lo mismo que intentas probar.

He hecho esto de una manera puramente sintáctica pero, por supuesto, en mi opinión, es importante tener en cuenta el aspecto semántico de las cosas y, en este sentido, la respuesta de Asaf que menciona las extensiones conservadoras es muy interesante. Tenga en cuenta que también mencionó el aspecto sintáctico ("traducir una prueba en$\mathcal{L}^+$en una prueba en$\mathcal{L}$recursivamente"), lo único que hice "más" es dar pistas sobre cómo se puede lograr esta traducción.

Si alguien puede mejorar mi respuesta corrigiendo algunos errores que probablemente cometí, tales modificaciones son, por supuesto, muy bienvenidas.

Un enfoque que utiliza fx Bourbaki es la introducción del operador de Hilbert . Al hacerlo, no necesita más primitivas, ya que los cuantificadores se pueden expresar en términos del operador de Hilbert.

La ventaja de usar esto es que el lenguaje permite que una construcción convierta un predicado en un objeto (cumpliendo el predicado si es posible).

Esto es similar a la solución ad-hoc para simplemente permitir la definición de un símbolo por un predicado que tiene una validez única.