¿Es inducción de conjunto relativamente coherente?

Question

Una forma de estado el axioma de la fundación es que el $\in$ relación en cualquier transitiva conjunto está bien fundado en el siguiente sentido:

• Una relación $(X,\prec)$ está bien fundada, si para cualquier subconjunto $S\subseteq X$ que es inductivo, en el sentido de que $y\in S$ todos los $y\prec x$ implica $x\in S$, en el hecho de $S=X$.

Este es el de la clásica equivalente a la más usual de la definición, pero de manera constructiva más razonable. Ahora constructivas conjunto de teorías como la CZF, uno a menudo encuentra un diferente axioma de la "fundación" llamado set-inducción o epsilon-inducción:

• Para cualquier fórmula $\phi$ si $\phi(x)$ todos los $x\in y$ implica $\phi(y)$ para cualquier conjunto $y$, entonces, en el hecho de $\phi(x)$ es cierto para todos los conjuntos de $x$.

Esto sin duda implica que $\in$ está bien fundada sobre cualquier conjunto transitivo, en el sentido de arriba, y lo contrario es cierto si cada conjunto tiene un cierre transitivo y tiene la plena axioma de separación, puesto que a partir de cualquier conjunto transitivo $x$ usted puede formar a $\lbrace y\in x \mid \phi(y) \rbrace$ y a la conclusión de que todo es de $x$.

Ahora clásico, uno puede demostrar que el axioma de fundación es consistente, en relación a los otros axiomas de la teoría de conjuntos, por la simple restricción de ningún modelo para la submodel de bien fundada conjuntos. Yo creo que usted puede hacer esto en CZF para la versión de "la fundación" he dicho anteriormente, que cada transitiva conjunto está bien fundada. Mi pregunta es, ¿se puede hacer algo similar con la inducción? Me preocupa más CZF, pero también me gustaría estar interesado en saber acerca de los resultados en cualquier otra teoría que carece de la plena axioma de separación.

(Por CIERTO, es posible que uno podría tener que pelearme un poco con lo que quiero decir por "los otros axiomas de la CZF" para hacer de este trivial. Para una cosa, vamos a colocar el axioma de infinitud, ya que veo que no hay garantía de que $\omega$ sería "muy bien fundada" en el sentido).

Answer 1

A finales respuesta: NO. Al menos con respecto a CZF.

CZF con el Conjunto de Inducción tiene la prueba de la teoría ordinal de la Bachmann-Howard ordinal.

CZF sin Establecer la Inducción es más débil. No se puede pensar en una referencia directa, pero:

• Crosilla y Rathjen "Inaccesible Conjunto de Axiomas puede tener poca consistencia de la fuerza"

Está demostrado que CZF sin establecer la inducción, pero con un inaccesibles conjunto axioma tiene pruebas de la teoría ordinal $\Gamma_0$.

Esto es estrictamente menor que el Bachmann-Howard ordinal, así que no hay consistencia relativa de la prueba es posible.

Answer 2

Vamos a KP⁰ ser la inducción libre de un fragmento de KP. Es decir, los axiomas de KP⁰ son extensionality, vinculación, unión, Δ₀-separación, Δ₀-colección, y (ya que veo que no hay manera de demostrar esto a partir de los otros axiomas) la existencia de transitivas cierres.

Siguiente Barwise, puedo definir la clase de Σ-fórmulas para ser el más pequeño de la clase que contiene fórmulas atómicas y sus negaciones, y que es cerrado bajo la conjunción, la disyunción, delimitada cuantificación, y sin límite cuantificación existencial. Del mismo modo, yo defino la de Π-fórmulas para ser el más pequeño de la clase que contiene fórmulas atómicas y sus negaciones, y que es cerrado bajo la conjunción, la disyunción, delimitada cuantificación, y sin límite cuantificación universal. La negación de una Σ-fórmula φ es canónicamente equivalente a un Π-fórmula y viceversa; voy a identificar φ con su canónica equivalente sin más comentarios.

Los siguientes tres hechos son estándar en KP. La habitual de las pruebas en realidad ir a través de KP⁰.

Σ-Reflexión. Para cada Σ-fórmula KP⁰ ⊦ φ ↔ ∃aφ^(a), donde φ^(a) se obtiene a partir de φ mediante la sustitución de cada ilimitado cuantificador ∃x por el correspondiente delimitada cuantificador ∃x∈un.

Σ-Colección. Para cada Σ-fórmula φ(u,v),

KP⁰ ⊦ ∀u∈x∃vφ(u,v) →∃y∀u∈x∃v∈yφ(u,v).

Δ-Separación. Para cada Σ-fórmula φ(u) y cada Π-fórmula ψ(u),

KP⁰ ⊦ ∀u∈x(f(u) ↔ ψ(u)) → ∃y∀u∈x(u ∈ y ↔ φ(u)),

donde y no se encuentra libre en la φ ni ψ.

En lugar de Mike Shulman fundación axioma, voy a utilizar el clásico equivalente axioma de regularidad:

(Reg) x ≠ ∅ → ∃y∈x(x∩y = ∅).

Este axioma ya implica una cierta cantidad de la inducción, porque de D-separación.

Δ-Inducción. Para cada Σ-fórmula φ(u) y cada Π-fórmula ψ(u),

PK⁰ + Reg ⊦ ∀u(φ(u) ↔ ψ(u)) → (∀u(∀v∈uφ(v) → φ(u)) → ∀uφ(u)).

Para su comodidad, ahora voy a asumir que el lenguaje contiene un símbolo de función rk(x) para el rango ordinal de un conjunto. Dejar que un ser Un modelo de PK⁰ + Reg. De un corte es un buen segmento inicial I de los ordinales de Una que no tiene menos de límite superior; una Σ-cut (resp. Π-cut) es uno que puede ser definida por un Σ-fórmula (resp. -Π de la fórmula).

Σ-Corte Lema. Si a es un modelo de PK⁰ + Reg y yo es una Σ-corte en Un, entonces_I = {x ∈ A : rk(x) ∈ I} es un modelo de PK⁰ + Reg.

Croquis de la prueba. El principal punto de discordia es Δ₀-colección. Supongamos que φ(u,v) es un Δ₀-fórmula que_me ⊧ ∀u∈x∃vφ(u,v). Considerar el conjunto de los números ordinales

J = {α ∈ R : ∃u∈x∀v(rk(v) < α → φ(u,v))}.

Este es un Π definibles por el segmento inicial de la I. no Tenemos I = J, ya que violaría Δ-inducción. Pick β ∈ I \ J. Trabajando en Una, podemos encontrar un conjunto y tal que

∀u∈x∃v∈y(rk(v) < β ∧ φ(u,v)).

Si es necesario, se puede cortar y para que rk(y) ≤ β y, por tanto, y ∈ A_I. ∎

Si tiene un mínimo Σ-cortar, entonces esto le da un modelo de KP⁰ que satisface Σ-inducción. Por desgracia, hay modelos de PK⁰ + Reg sin un mínimo de Σ-cut.

Ahora, en el lado positivo, un menor giro de la prueba de la Σ-corte lema da el siguiente.

Π-Corte Lema. Si a es un modelo de KP⁰ que satisface Π-inducción y yo es el corte de Un, entonces_I es un modelo de KP⁰.

(Π-inducción implica que el Π conjunto J se define como anteriormente debe tener un mínimo de límite superior β ∈ I. El resto de la prueba es idéntica.)

Así que cuando Un satisface Π-inducción, podemos tomar una lo suficientemente pequeño corte de Un a conseguir un modelo de KP (con inducción completa). De hecho, podemos tomar la máxima fundado segmento inicial de los ordinales de Una, con la salvedad de que este corte es muy a menudo sólo ω.

Cuando tengo la oportunidad, voy a tratar de añadir ejemplos que muestran que no se puede hacer mejor que el Σ-corte lema y la Π-corte lema.

---

Adenda. Me tropecé a través de dos artículos que abordan estas cuestiones. El primer papel es por Domenico Zambella de la Fundación frente a la inducción de Kripke-Platek la teoría de conjuntos [J. Symb. La lógica 63 (1998), MR1665739] donde se muestra que la fundación implica abrir la inducción, pero no Σ₁-inducción sobre KP⁰ (sin transitiva cierres). Esto se complementa con Antonella Mancini y Domenico Zambella Una Nota sobre Recursiva de los Modelos de las Teorías de [la catedral de Notre Dame, J. la Lógica Formal 42 (2001), MR1993394] donde generalizar Tennenbaum del Teorema mostrando que los fragmentos de KP que demostrar Σ₁-inducción no tienen computable otros modelos que la estándar.

Answer 3

Creo que no debería ser un problema, mostrando que la "muy bien fundada" o "clase-bien fundada" conjuntos de satisfacer a la mayoría de los axiomas básicos de la teoría de conjuntos que involucran sólo a $\Delta_0$-cuantificadores, por ejemplo, los pares, los sindicatos, $\Delta_0$-separación. El problema deben estar principalmente con los axiomas como la sustitución y la colección que implican ilimitado cuantificadores ya que "la clase-fundamento" no es especificado por una sola fórmula, de modo que no puede restringir los cuantificadores ir encima de esos conjuntos. De hecho, ni siquiera está claro que la clase-bien-fundado conjuntos satisfacen conjunto de la inducción, ya que el significado de los cuantificadores ha cambiado.

He encontrado una respuesta parcial a un problema relacionado en Mathias papel de "La fuerza de Mac Lane teoría de conjuntos." En La Prop. 6.39 demuestra que en un metatheory con una lo suficientemente fuerte como axioma de la separación ($\Sigma_1$), si partimos de un modelo de N de un cierto débiles de la teoría, incluyendo KP y $\Sigma_1$-fundación y cuyos números naturales son en realidad bien fundada (en el sentido de la metatheory), a continuación, el submodel M de N que consta de los "conjuntos" cuyo rango de N es en realidad bien fundada constituye un modelo de la misma teoría de la plus "de la clase de la fundación" (= conjunto de la inducción). Como era de esperar, la principal dificultad está en la demostración de $\Delta_0$-de la colección.