¿Podemos restringir los esquemas en ZFC para que solo construyan conjuntos con una membresía clara?

ZFC es realmente una pista falsa aquí: el mismo fenómeno ya ocurre en, digamos, PA. Por ejemplo, PA demuestra

hay un numero$n$tal que$n=0$si la conjetura de Goldbach es cierta y$n=1$si la conjetura de Goldbach es falsa.

De manera más general, tenemos:

$(*)\quad$Si$T$es cualquier teoría incompleta con dos fórmulas$\varphi,\psi$cual$T$prueba que cada uno define elementos distintos entonces$T$tiene un "objeto ambiguo".

Volviendo a la pregunta original, tenga en cuenta que Separación no necesita usarse aquí en el contexto de ZFC; por ejemplo, sin usar Separation ZFC demuestra que

Y$(*)$se aplica básicamente a todas las teorías razonables: la única forma de evitarlo es volverse ultradébil , al nivel de teorías que no son capaces de definir dos objetos demostrablemente distintos, o ir a teorías completas, lo que implica perder la axiomatabilidad computable o perder nuevamente casi toda la fuerza lógica. Entonces, en última instancia, la respuesta a su pregunta es: no , no sin renunciar a las propiedades absolutamente fundamentales de ZFC (es decir, su fuerza y ​​​​su axiomatizabilidad computable) .

Cada elección de$\phi$da su propio axioma. Su propuesta es utilizar un esquema más pequeño en el que el único$\phi$utilizados son aquellos para los que, para cualquier conjunto$A$, los mismos elementos de$A$satisfacer$\phi$en todos los modelos. Una formulación equivalente, siempre que nuestra nueva teoría pueda probar cada$x$es el elemento único de algún singleton de$x$, es que nos restringimos a aquellos$\phi$para los cuales los modelos nunca están en desacuerdo sobre lo que satisface$\phi$.

Ahora, una alternativa dada a ZFC, por la cual algunos$\phi$están prohibidos, pueden o no tener esta envidiable propiedad. Pero es una propiedad de la teoría, y queremos usar esa propiedad para definir qué$\phi$aportar axiomas a la teoría. Cuanto más pequeño se vuelve el esquema, menos puede probar la nueva teoría, y es posible que descubras una$\phi$solías pensar que estaba bien ya no lo está. No está claro qué sobrevivirá a este ciclo, y aún menos claro que hay un único$\phi$-elegir el algoritmo que consigue lo que queremos. Entonces, a menos que pueda probar un metateorema que diga cuál$\phi$para elegir hacer esto, no puedo verlo despegar. Irónicamente, la intención aquí de hacer que los productos de la separación estén "bien definidos" tiene una estrategia mal definida.

Eso sí, trata de no decepcionarte demasiado. La responsabilidad de los axiomas como definiciones implícitas es afirmar que se puede dar algún significado a los símbolos en aquellos axiomas bajo los cuales son verdaderos, es decir, que los axiomas tienen un modelo. Su responsabilidad no es saber qué modelo es de su interés. De hecho, si axiomas como estos están incompletos (que tendrán que serlo si son consistentes), no pueden reducir las cosas a un modelo. Los axiomas de ZFC "definen" lo que son los conjuntos, pero solo implícitamente, y ciertamente no de manera única. Y si los múltiples significados de "conjunto" son consistentes con estos axiomas, no debería importarnos si un conjunto específico que define la teoría está sujeto de manera similar a detalles dependientes del modelo.