Aquí es cómo iba a formalizar la noción de definability.
Definición. Deje $\phi\left(x\right)$ ser una fórmula en el lenguaje de la teoría de conjuntos (con la única variable libre $x$), y deje $\mathsf T$ ser un conjunto de oraciones en el lenguaje de la teoría de conjuntos (usualmente $\mathsf{T=ZF}$ o $\mathsf{T=ZFC}$). Podemos decir $\phi\left(x\right)$ define un conjunto en $\mathsf T$fib
$$
\mathsf T\vdash\existe !x\phi\left(x\right).
$$
Aquí, $\exists !x\phi\left(x\right)$ es una abreviatura para una fórmula que significa "no hay una única $x$ tal que $\phi\left(x\right)$".
Ejemplo. La fórmula $\forall y\left(y\notin x\right)$ define un conjunto en $\mathsf{ZFC}$.
Definición. En primer lugar observamos que si $\phi\left(x\right)$ define un conjunto en $\mathsf T$, luego por la adición de algunas constantes símbolo $c$ a nuestro idioma, y el axioma $\phi\left(c\right)$$\mathsf T$, obtenemos un conservador extensión de $\mathsf T$. A continuación, voy a decir que $c$ es un término constante para $\mathsf T$ y que $\phi\left(x\right)$ define $c$ $\mathsf T$.
Ejemplo. La fórmula $\forall y\left(y\notin x\right)$ define $\emptyset$$\mathsf{ZFC}$. Del mismo modo, si $c$ es un término constante para $\mathsf{ZFC}$ entonces $\bigcup c$, $\mathcal P\left(c\right)$ y $\left\{x\in c:\psi\left(x\right)\right\}$. Esto nos permite utilizar $\emptyset$, $\bigcup$, $\mathcal P$ y establecer el constructor de la notación como nos haría normalmente cuando se trabaja en $\mathsf{ZFC}$.
Aquí es cómo me gustaría tratar de describir la diferencia entre una Opción y la otra de construcción de los axiomas en esta configuración. Primero, considere cualquier edificio axioma de $\mathsf{ZF}$, es decir, cualquier cosa excepto Extensionality o Fundación. Es un ejercicio para ver que el axioma puede ser escrita en la forma $\forall y_1,\dots,y_n\exists x\varphi\left(x,y_1,\dots,y_n\right)$ donde $\mathsf{ZF}\vdash\forall y_1,\dots,y_n\exists !x\varphi\left(x,y_1,\dots,y_n\right)$ (nota de la "!" aquí). (Técnicamente, el Infinito no es de esta forma en su formulación habitual, pero puede ser sustituido un axioma de la definición de $\omega$$\mathsf{ZF}$.) Por lo tanto, si $c_1,\dots,c_n$ son constantes en términos de $\mathsf{ZF}$, $\varphi\left(x,c_1,\dots,c_n\right)$ define un conjunto en $\mathsf{ZF}$. Sin embargo, si $\mathsf{ZF}$ es reemplazado por $\mathsf{ZFC}$, entonces este argumento claramente se rompe.
Creo que es en este sentido que definability corresponde a no necesitar el axioma de elección. Sin embargo, también se podría tratar de formalizar esta idea de la siguiente manera.
Conjetura. Si $\phi\left(x\right)$ define un conjunto en $\mathsf{ZFC}$, $\phi\left(x\right)$ define un conjunto en $\mathsf{ZF}$.
También se podría interpretar esto como diciendo que "el axioma de elección no ayuda con la singularidad de pruebas". Sin embargo, es falso (suponiendo que $\mathsf{ZF}$ es consistente).
Contraejemplo. Deje $\phi\left(x\right)$ ser la fórmula que significa "$x$ es un primer ordinal (es decir, bien solicitar el cardenal), y para cada conjunto infinito $y$ hay una inyección de $x\to y$". Claramente $\mathsf{ZF}\vdash\left(\exists x\phi\left(x\right)\right)\Leftrightarrow\phi\left(\omega\right)$, e $\mathsf{ZFC}\vdash\phi\left(\omega\right)$. Pero (nos la formalización de la noción de "conjunto infinito" de forma adecuada, y suponiendo que $\mathsf{ZF}$ es consistente), $\mathsf{ZF}\not\vdash\phi\left(\omega\right)$. Por lo tanto $\phi\left(x\right)$ define $\omega$$\mathsf{ZFC}$, pero no define un conjunto en $\mathsf{ZF}$.
Vea también: http://en.wikipedia.org/wiki/Definable_set
