Creo que la razón principal de reemplazo es visto como una parte esencial de ZF es que sigue naturalmente de la ontología de la teoría de conjuntos, como el resto de los axiomas de ZF. La ontología de la teoría de conjuntos está enraizado en la idea de que los conjuntos son obtenidos por un proceso iterativo a lo largo de un wellordered "ordinal reloj", donde a cada paso todos los conjuntos cuyos elementos se generaron antes, ahora aparecen. Es intuitivamente claro que, con el fin de ser exhaustivo, este proceso debe ir en un largo, largo tiempo. Desde este punto de vista, el axioma de reemplazo puede ser intuitivamente dijo: no se puede utilizar como una indexación de una familia de ordinales que llega al final de la escala ordinal escala de tiempo. Esta es una consecuencia natural de la idea de que el proceso iterativo debe ser exhaustiva.
Otro aspecto interesante de la sustitución, es que (en la mayoría de las formulaciones de ZFC) es lógicamente equivalente a la reflexión. (De manera informal: para cualquier fórmula $\sigma(\vec{x})$, en el lenguaje de la teoría de conjuntos, si $V \models \sigma(\vec{x})$, entonces hay un ordinal $\alpha$ tal que $V_\alpha \models \sigma(\vec{x})$.) Esto es muy útil principio. Uno de sus efectos secundarios es que ZFC es "auto-justificación" en el sentido de que cualquier fragmento finito de ZFC se realiza en un nivel de $V_\alpha$ de la jerarquía acumulativa. En otras palabras, si se prueba que la teoría de conjuntos mediante el examen de un fragmento finito de axiomas en el universo de los conjuntos, uno podría ver que este fragmento finito no es sólo coherente, sino que tiene un modelo de $V_\alpha$ que surge desde el mismo proceso iterativo que todos los conjuntos. En particular, ZFC viene muy cerca de demostrar su propia consistencia, aun cuando sabemos que esto no es posible después de Gödel. Esta característica hace que ZFC es muy atractivo como fundacional de la teoría. (Tenga en cuenta que el PA tiene una similar a la auto-justificación, pero, ETCS no parecen tener este.)
Otro, más práctico, el uso de reemplazo es obtener "hoteles de universos". Grothendieck universos han demostrado ser útiles para la manipulación de objetos grandes. Por desgracia, no se puede demostrar su existencia en ZFC. Sin embargo, es a menudo la verdad que una "razonable teorema" demostrado el uso de Grothendieck universos en realidad es demostrable en ZFC. La razón es que la prueba no suele hacer un uso completo de todas las características de Grothendieck del universo, un fragmento finito de estas características suele ser suficiente y, en tales casos la reflexión proporciona un conjunto $V_\alpha$ con todas las características necesarias para hacer que el argumento de la obra. ETCS no parecen tener una buena forma de obtener "hoteles de universos". Esto también sugiere una alternativa a la sustitución, que es el de tener una jerarquía de universos similares a los utilizados en dependiente del tipo de teoría.
Las operaciones en dependiente de las familias es donde la necesidad de reemplazo surge más. De hecho, es muy difícil incluso hablar dependiente de las familias en el lenguaje de ETCS. El principal problema con ETCS no es necesariamente que no puede probar la existencia de co-productos como $\coprod_{n \in \mathbb{N}} \mathcal{P}^n(\mathbb{N})$, pero que tiene un tiempo difícil incluso hablar acerca de la familia de todas las $\mathcal{P}^n(\mathbb{N})$ en el primer lugar. La introducción de los universos sería una forma interesante de conseguir alrededor de ese problema, pero hay otros medios, todo lo cual es muy probable que la necesidad de sustitución-como principios claros.
Como para la propuesta de solución, es claro que sería mucho más por este tipo de proceso. En lugar de ETCS, voy a trabajar en BZC ampliada con los términos de powersets y de la unión y una constante símbolo de $\omega$. El exponencial delimitadas las fórmulas se definen como delimitada fórmulas, excepto que la delimitación de los términos puede implicar powerset y de la unión.
Hecho. Si $\phi(x,y)$ es un exponencialmente acotado fórmula que BZC demuestra que $\forall x \exists y \phi(x,y)$, entonces hay un número estándar $n$ tal que BZC demuestra que $\forall x \exists y(\phi(x,y) \land |y| \leq |\mathcal{P}^n(x \cup \omega)|)$.
Prueba. Encontrar un modelo de $M$ de BZC y considerar la posibilidad de $x \in M$. Deje $M' = \bigcup_n \{z \in M : |z| \leq |\mathcal{P}^n(x \cup \omega)|\}$ donde $n$ rangos de la norma sólo números. Tenga en cuenta que $M'$ es el modelo de BZC que contiene $x$. Por hipótesis, existe una $y \in M'$ tal que $M' \models \phi(x,y)$. Tenga en cuenta que exponencial acotado fórmulas son absolutos entre el $M'$ e $M$, ya que sólo establece que tenemos que mirar para saber que $\phi(x,y)$ es cierto están en $M'$. Por lo tanto $M \models \phi(x,y)$ también $M \models |y| \leq |\mathcal{P}^n(x \cup \omega)|$, por definición, de $M'$. Ahora bien, el hecho de que no hay una norma fija $n$ que seguramente funciona para todas las $x$ sigue por una compacidad argumento. $\square$
Los ejemplos $\omega, \mathcal{P}(\omega), \mathcal{P}^2(\omega), \ldots$ e $V, V^{\ast}, V^{\ast\ast},\ldots$ son definibles por una fórmula de la forma $\exists z\phi(x,y,z)$ donde $\phi(x,y,z)$ es exponencial acotado. Debido a la agradable biinterpretation entre ETCS y BZC, para estos y otros ejemplos similares, ya sea ETCS no es prueba de que el $n$-ésima iteración existe para cada número natural $n$, o ETCS ya demuestra que la sustitución tiene en esta instancia en particular.
Permítame también abordar un aspecto de la nota de pie de página, que establece que la sustitución sería "la causa más probable" si ZFC fueron encontrados para ser incoherente. La norma de "objeción" a la teoría de conjuntos axiomática es en realidad con la comprensión. Si usted piensa acerca de ello, la comprensión es más bien una declaración audaz: cada fórmula en el lenguaje de la teoría de conjuntos se puede utilizar para definir un subconjunto de un conjunto dado. El problema es que las fórmulas pueden ser complejas más allá (humano) de la comprensión, es difícil justificar el uso de la comprensión de las fórmulas que no podemos entender. De hecho, no está claro que la comprensión está plenamente justificada por la ontología de la teoría de conjuntos descritos anteriormente. (Tenga en cuenta que el mismo tipo de objeción se aplica a PA, donde uno se pregunta, para la inducción para mantener arbitrarias de fórmulas.)
