¿Por qué los cuantificadores apilados en PA corresponden a ordinales hasta$\epsilon_0$?

Question

Estoy tratando de entender por qué la inducción hasta exactamente $\epsilon_0$ es necesario probar el corte de la eliminación teorema de primer orden de la Aritmética de Peano; o, como yo lo entiendo, lo que es equivalente, por qué la longitud de un PA-prueba con todos los recortes eliminado crece (en el peor de los casos) tan rápido como $f_{\epsilon_0}$ en el rápido crecimiento de la jerarquía.

Puedo entender por qué el uso de un axioma de inducción se corresponde con el ordinal de la multiplicación por $\omega$. Como la inducción son los axiomas escrito en el secuente de cálculo, como premisa tenemos una prueba de $\phi(x)\vdash\phi(Sx)$ gratis variable $x$, y como conclusión obtenemos $\phi(0)\vdash\phi(y)$ para cualquier plazo $y$.

Entonces, si la prueba de $\phi(x)\vdash\phi(Sx)$ tiene el ordinal $\omega^\alpha$, la prueba con la conclusión de $\phi(0)\vdash\phi(y)$ es asignado el ordinal $\omega^{\alpha+1}$. E. g. si la prueba de la inducción de paso había ordinal $\omega^0 = 1$, entonces la conclusión $\phi(y)$ tiene el ordinal $\omega^1 = \omega$.

Esta parte tiene perfecto sentido para mí, porque si yo quería eliminar el uso de una inducción de la regla (CJ secuente) podría comenzar con $\phi(0)$ y repetidamente ir a través de la parte de la prueba que he utilizado para comprobar la $\phi(x)\vdash\phi(Sx)$. Decir, que me gustaría repetir la sub-prueba de la inducción paso 17 veces, por ejemplo, con $\phi(14)\vdash\phi(15)$ y así sucesivamente, hasta que llegué a $\phi(17)$, o cualquiera que sea el número que yo quería probar lo $\phi$ aproximadamente.

Yo no entiendo muy bien cómo esto corresponde a la eliminación de los recortes, de por sí (parece crear una nueva serie de recortes, de hecho). Pero todavía es muy intuitivo para mí que la Aritmética de Peano del poder para invocar el axioma de inducción corresponde a la multiplicación por $\omega$. Si tomamos una prueba PA que termina con un solo uso de la inducción axioma para obtener $\phi(y)$, y queremos plasmarlo en una prueba en una media aritmética de la teoría que no tiene la inducción, entonces tendremos que multiplicar el PA-prueba de longitud por cualquier número finito (por ejemplo, si se multiplica por 17) para obtener la prueba de longitud en el inductionless teoría.

La multiplicación repetida por $\omega$ sólo nos lleva hasta el $\omega^\omega$ como una prueba de la teoría de la ordinal, aunque.

De acuerdo a Gentzen, cuando usamos recortes en las fórmulas que involucran cuantificadores, por ejemplo,$\forall p:\exists q:\psi(p,q)$, esto corresponde a ordinal exponenciación. Si la prueba anterior la corte ha ordinal $\alpha$ y cortamos una fórmula con un cuantificador, entonces la prueba por debajo de la corte ha ordinal $\omega^\alpha$. Si cortamos en dos cuantificadores, la prueba por debajo de la corte ha ordinal $\omega^{\omega^\alpha}$. Esto encaja con las otras cosas que he oído acerca de cómo la PA mediante fórmulas con sólo N cuantificadores pueden ser probadas por la coherencia de las PA utilizando sólo N+1 cuantificadores. (Como una cuestión de lado yo estaría interesado en saber cómo utilizar N cuantificadores para demostrar wellfoundedness de un ordinal notación de una pila de $\omega$s N capas.)

Lo que yo no entiendo es por qué la capacidad de utilizar los cuantificadores corresponde ordinal exponenciación. Puedo adivinar en un vago sentido de que si tenemos una prueba de uso de $\forall p:\phi(p)\vdash\phi(17)$, y queremos eliminar el uso de $\forall p:\phi(p)$, entonces tenemos que repetir esa parte de la prueba cada vez que quiero probar $\phi(17)$, $\phi(q)$, y así sucesivamente. Pero esto de nuevo sólo implica que teníamos que repetir que parte de una prueba de un número finito de veces, y la iteración esto nos lleva sólo a $\omega^\omega$, no el deseado $\epsilon_0$, por lo que me debe faltar algo.

Le pregunté a un amigo para ayudar con esto y ella ha leído a través de Gentzen de la documentación pertinente, y ella me mostró las partes relevantes, y que previamente había comprobado varios textos estándar en la prueba de la teoría y la busqué en Google a su alrededor, y ella también compraban la pregunta alrededor de la lógica de departamento de una universidad importante, y todavía no sabemos la respuesta a esta excepción "porque Gentzen dice a utilizar ordinal exponenciación".

También no se puede encontrar ningún ejemplos de corte de eliminación se lleva a cabo en una prueba con corte en una fórmula cuantificada, que muestra cómo el tamaño de la corte resultante libre de la prueba podría crecer más rápido de lo $f_{\omega^\omega}$. Un ejemplo como este para algunos en particular la prueba sería muy útil, incluso si, de la necesidad, repite los pasos para la eliminación de la corte se ha esbozado más que demostrado. Puedo entender por qué la longitud de un Kirby-París hydra juego crece a la misma tasa que la Goodstein secuencia, y visualizar ambos procesos en la medida en que un ser humano pueda. No puedo visualizar por qué la longitud de un PA-prueba de partida para la corte, libertad crecería al mismo ritmo que los cortes fueron repetidamente eliminado. (Mapeo del proceso en un Kirby-París hydra juego de la altura inicial de al menos 3 tendrían que responder a la pregunta!)

Answer 1

8/14: Sustancialmente editado en respuesta a los comentarios: añadido a la 1ª parte, se agregaron nuevos 2ª y 4ª partes

También hay algo de debate debajo, y un enlace a un parcial de escritura de un caso de corte de eliminación que involucran la función de Ackermann

Si no has encontrado la Gentzen de estilo a prueba de ilustrativo, os recomiendo probar el infinitary prueba. (No todo el mundo le gusta, pero al menos es una perspectiva alternativa sobre ella.) Pohlers "Prueba de la Teoría: Una Introducción", da una agradable presentación de la prueba, y se incluye la prueba PA que ordinales por debajo de $\epsilon_0$ está bien fundada. (Esto incluye el hecho de que usted use $N$-cuantificador de inducción a prueba de fundamento a a $N+1$ exponentes, lo que da una idea en forma adicional cuantificadores tener el efecto que hacen.)

Una característica interesante de la infinitary prueba de ello es que los ordinales son simples límites en las alturas de las pruebas, así que si usted se siente cómodo en la visualización de infinitary pruebas, el origen del aumento de los límites es bastante explícito.

Vale la pena señalar que "infinitary" es un poco de un nombre inapropiado. El infinitary prueba toma la perspectiva de que una prueba de $\forall x\phi(x)$ debe ser una función computable $f$, de modo que, para cada $n$, $f(n)$ es una prueba de $\phi(n)$. Dado que las funciones son todos los computable, no hay nada realmente infinitary sobre ella. La gente suele ignorar la "computable" parte a título expositivo, ya que no tiene sentido sin ese requisito, momento en el que no se ve infinitary, pero esto es sólo porque muchas de las ideas son más claras sin necesidad de estar constantemente comprobación de que las operaciones que estamos describiendo realmente son computables.

$ $

Un seguimiento sobre lo que ordinales media en la prueba de la teoría. Como se señaló en los comentarios, $\omega$ no significa realmente "infinito", que significa "sin especificar fijo entero". Del mismo modo, $\omega+3$ significa realmente "no sólo es esta entero no especificado, pero va a tomar tres pasos para averiguar qué número entero es". Así, en el infinitary prueba de corte de eliminación, cuando decimos que una prueba tiene la altura $\omega$, podemos decir que es una prueba de que, digamos, $\forall x\phi(x)$, donde la altura de la prueba de $\phi(n)$ es $g(n)$ con $g(n)\rightarrow\infty$.

Una prueba de la altura de la $\omega+3$ es una prueba con tres pasos adicionales a continuación una prueba de altura $\omega$. Lo más interesante, una prueba de la altura de la $\omega+\omega$ podría ser una prueba de $\forall x\phi(x)\vee\forall y\psi(y)$ donde para cada una de las $n$, se tiene una prueba de $\phi(n)\vee\forall y\psi(y)$ de la altura de la $\omega+n$. Para encontrar un cuantificador libre de la ejecución de esta prueba, tendríamos primero conecte un $n$ para $x$ y luego, en el nivel adecuado, un $m$ para $y$ para obtener una prueba de $\phi(n)\vee\psi(m)$ de la altura de la $g(n)+h(n,m)$.

$ $

Hablando de manera muy informal, las intuiciones que se describen anteriormente son perfectamente razonable, pero que, básicamente, sólo corresponden a lo que está sucediendo con bastante sencillo (en su mayoría de un cuantificador) fórmulas. Corte de eliminación corresponde a la extracción computable de la información, y cuando se corta fórmulas con varios cuantificadores juntos, la información tiene que ser de ida y vuelta entre los dos lados.

De manera informal, pienso en ello como esto: supongamos que deseamos cortar una prueba de $$(\forall x\exists y\phi)\vee\psi$$ con una prueba de $$(\exists x\forall y\neg\phi)\vee\psi'$$ (corte de eliminación generalmente, es más fácil pensar en un solo lado de formulario). La segunda prueba produce una primera propuesta de valor de $x$ presenciando $\forall y\neg\phi$. La primera prueba podría refutarla mediante la exhibición de un $y$. La segunda prueba se puede utilizar ahora que el valor de $y$ a calcular una segunda adivinar lo $x$ es, la primera prueba de la refuta de nuevo, y así sucesivamente hacia atrás y adelante. Esto podría ir y venir de un gran número de veces (en el orden de los ordinales de la segunda prueba---que es, no sólo un número fijo de veces, pero, si el ordinal es algo como $\omega+1$, un número de veces que se basa en el valor de la primera $y$ o si $\omega+\omega+1$, la primera $y$ nos dice cuántos pasos nos vamos antes de que un valor de $y$ que nos dice cuántos pasos hemos de ir, etc.)

Esta descripción es literalmente cierto cuando se ve a través de la lente de la interpretación funcional. Cuando se ven en términos de infinitary corte de eliminación, estos y forths" corresponden a entrelazado cortes: colocamos la cantidad de copias de la primera prueba (más precisamente, las pruebas de $\exists y\phi(n,y)\vee\psi$ para los distintos valores de $n$) a lo largo de la segunda prueba. Cada uno de estos crea nuevos recortes, que corresponden a la toma de las secciones de la segunda prueba y ubicarlas dentro de las muchas copias de la primera prueba que hemos creado.

$ $

Creo que su indización en la relación entre el rápido crecimiento de la jerarquía y la prueba de la teoría de los números ordinales es una exponencial. La prueba teórica ordinal de $I\Sigma_1$ es $\omega^\omega$, pero esto solo demuestra la primitiva funciones recursivas totales (es decir, $f_n$ con $n<\omega$ en el rápido crecimiento de la jerarquía). No estoy encontrando una referencia sobre la relación exacta, pero me imagino que la diferencia es consistente---que en la forma en que dos cuantificador de inducción es como $\omega^{\omega^n}$, los Conway de la cadena de notación es como $\omega^{\omega^2}$. Así, mientras que dos cuantificador de inducción es suficiente, el trato con los Conway de la cadena de notación se verá como un uso sustancial de dos cuantificador de la inducción (de hecho, creo que implica tres niveles anidados de inducción, dos de las cuales tienen más de dos cuantificador fórmulas, que se alinean bien con un ordinal de $\omega^{\omega^2}$).

Habiendo dicho eso, tu pregunta es todavía perfectamente razonable: ¿cómo funciona el ida y vuelta que he descrito arriba conseguir las cosas que son de crecimiento muy rápido. Supongamos que la primera prueba, de $(\forall x\exists y\phi)\vee\psi$, tiene un sensible de la tasa de crecimiento, digamos, exponencial. La segunda prueba es la iteración de la tasa de crecimiento de la primera prueba, y puede iterar un número ordinal de veces que se basa en la altura de la segunda prueba. Desde la segunda prueba podría fácilmente (dado tal vez algunos recortes adicionales más pequeñas fórmulas) tiene, por ejemplo, la altura de la $\omega^2$. Es decir, si tomamos $f_0(n)=n^n$, $f_{\alpha+1}(n)=f_\alpha(f_\alpha(n))$, y $f_\lambda(n)=f_{\lambda[n]}(n)$, se debe golpear a todo nivel de $f_{\omega^2}(n)$ en esta jerarquía.

Answer 2

Como una cuestión de lado yo estaría interesado en saber cómo utilizar $N$ cuantificadores para probar bien el fundamento de un ordinal notación de una pila de $\omega$'s $N$ capas.

Me puse esto como un reto, un par de años atrás, cuando yo estaba aprendiendo este material; aquí está la solución que se me ocurrió. Espero que no hay errores.

---

Primero vamos a comprobar que estamos de acuerdo en la instalación:

Deje $X$ ser un conjunto ordenado con el fin de relación $\leq$. A continuación, $\omega^X$ es el conjunto de funciones de $X \to \omega$ tal que todos, pero un número finito de elementos de $X$ mapa a $0$. Vamos a escribir los elementos de $\omega^X$ para buscar secuencias, como: $(a_i)_{i \in X}$ donde $i$ mapas a $a_i$. Tenemos $(a_i) > (b_i)$ si hay un índice de $d$ con $a_d > b_d$ e $a_e = b_e$ para $e > d$. (Expresando esto en la PA requiere toneladas de $\beta$-codificación, pero voy a asumir que ya están completamente cómodo con ese pincel y de los problemas debajo de la alfombra.) El símbolo $0$ indican el mínimo elemento de $\omega$, el mínimo elemento de $X$ y el mínimo elemento de $\omega^{X}$; lo que me refiero debe ser claro en el contexto.

Deje $\phi$ ser un primer pedido de declaración de una variable libre $x$ van más de $X$. Deje $I(x,X,\phi)$ denotar la declaración: $$ \left( \exists x \in X : \phi(x) \right) \implies \exists z \in X : \phi(z) \ \wedge \ \forall w \in X : \phi(w)\! \implies \! w \geq z $$ En otras palabras, si cualquier elemento de $X$ obedece a $\phi$, entonces existe al menos un elemento de $X$ obedeciendo $\phi$. Nos dicen que PA demuestra $X$ es bien ordenado si, por cualquier $\phi$, PA demuestra $I(x,X,\phi)$.

Queremos mostrar que, si PA demuestra que $X$ es bien ordenado, entonces PA que además demuestra que $\omega^X$ está bien ordenado.

---

La estrategia de la prueba es la única cosa que podría ser. Voy a describir una receta que, dado un primer orden de la frase $\phi(x)$, con $x$ van más de $\omega^X$, produce un primer orden de la frase $\phi'(x')$ con $x'$ van más de $X$. Voy a mostrar entonces que $I(x', X, \phi')$ implica $I(x,\omega^X, \phi)$. La sentencia de $\phi'$ tendrá tres instancias de $\phi$: Uno, precedidos por $\forall \neg$, uno precedidos por $\exists$ y un precedidos por $\exists \forall \neg$. Si $\phi$ es de $\Sigma_n$, a continuación, estos son en $\Pi_n$, $\Sigma_n$ y $\Sigma_{n+1}$ respectivamente. Creo que esto demuestra que esta construcción se lleva a $\Sigma_n$ a $\Sigma_{n+1}$ (pero debo admitir que no estoy completamente seguro de que en este argumento.)

Escribir $\omega \uparrow n$ para torres de $\omega$'s apilados $n$ alto. A continuación, este argumento se reduce demostrando $I(x,\omega \uparrow n, \phi)$ a probar $I(x', \omega \uparrow (n-1), \phi')$, y el que reduce a $I(x'', \omega \uparrow (n-2), \phi'')$ etcétera, hasta llegar a $I(x^{n-1}, \omega, \phi^{n-1})$. En el proceso, hemos añadido volvió un $\Sigma_k$ declaración en un $\Sigma_{k+n}$ declaración. Por supuesto, $I(x^{n-1}, \omega, \phi^{n-1})$ es un axioma de la PA, así que será realizado.

---

Para mejorar la legibilidad, voy a cambiar las notaciones $\phi'$ e $x'$ a $\delta$ e $d$. En general, voy a tratar de utilizar las cartas desde el principio del alfabeto para los elementos de $X$ y letras de la final para los elementos de $\omega^X$.

Aquí está la frase crucial $\delta(d)$: $$\left( \exists x \in \omega^X : \phi(x) \right) \implies \exists z \in \omega^X : \phi(z) \ \wedge \ \forall w \in \omega^X : \phi(w)\! \implies \! \left( w \geq z \ \vee \ \forall_{e \geq d} : w_e=z_e \right) $$ En otras palabras, $\delta(d)$ es esencialmente la inducción de la reclamación $I(x,\omega^X, \phi)$, pero se nos permite tener $w<z$ mientras $w$ e $z$ está de acuerdo en la parte de $X$ pasado $d$.

Escribirse sin $\implies$, esto es de la forma $$\forall_x \neg \phi(x) \vee \exists_z \left( \phi(z) \wedge \forall_w \neg \phi(w) \vee (\mbox{stuff without }\ \phi) \right).$$ Por lo $\delta$ precede $\phi$ con $\forall \neg$, con $\exists$ e con $\exists \forall \neg$ como se había prometido.

---

Lo que queda es demostrar que el $I(d, \delta, X)$ implica $I(x, \phi, \omega^X)$. Usted puede disfrutar haciendo esto por sí mismo más que leer mi solución.

Si $\phi(x)$ es falsa para todas las $x$,, a continuación, $I(x, \phi, \omega^X)$ es vacuously verdadero. Así que podemos asumir que hay un $x$ obedeciendo $\phi(x)$.

Elija $d_1$ suficientemente grande como para que $x_e=0$ para todos los $e \geq d_1$. A continuación, $\delta(d_1)$ es cierto porque, para cualquier $w \in \omega^X$, o tenemos $w \geq x$ o $ \forall_{e \geq d_1} : w_e=0$. Así que hay algo de $d$, lo que hace que $\delta$ cierto. Deje $d$ ser el menor elemento de $X$, lo que hace que $\delta$ cierto.

Si $d=0$, estamos hecho, ya que el $\delta(0)$ es, precisamente,$I(x,X, \phi)$. Así que asumir por el bien de la contradicción que $d>0$.

Deje $\bar{z} \in \omega^X$ a ser el elemento que se ha prometido a existir de acuerdo a $\delta(d)$. Hay sólo un número finito $i$ para que $\bar{z}_i$ es distinto de cero. Deje $c$ ser el mejor $i$, que es menos de $d$. Por lo $\bar{z}$ parece $$(\ldots, 0,0,0,\bar{z}_c, 0,0, \ldots, 0,0, \ldots, 0,0, \bar{z}_d, 0, 0, \ldots).$$ Si $\bar{z}_i$ es cero para todos los $i<d$, luego tome $c=0$. Nuestro objetivo es demostrar $\delta(c)$; esto contradice la minimality de $d$, por lo que completa la prueba.

Deje $\ell$ ser el elemento más pequeño de $\omega$ tal de que no existe $y \in \omega^X$ con las siguientes propiedades: $$\phi(y) \ \wedge \ y_c=\ell \ \wedge \ \forall_{e > c} : y_e = \bar{z}_e$$ Hay por lo menos uno de esos $\ell$, ya que puede tomar $y=\bar{z}$ e $\ell = \bar{z}_c$, por lo que hay menos $\ell$ porque $\omega$ está bien ordenado. Deje $y$ a ser el elemento de $\omega^X$ anterior.

Yo reclamo que la toma de $y$ en lugar de $z$ hace $\delta(c)$ cierto. Deje $w$ obedecer $\phi(w)$. Así que o $w \geq \bar{z}$ o $\forall_{e \geq d} w_e = \bar{z}_e$. Debemos mostrar que cualquiera de las $w \geq y$ o $\forall_{e \geq c} w_e = y_e$.

Caso 1 Hay algunos $e \geq d$ con $w_e \neq \bar{z}_e$.

A continuación,$w > \bar{z}$. Desde $\forall_{f \geq d} : y_f=\bar{z}_f$, también tenemos $w > y$, como se desee.

Caso 2 Para todos los $e \geq d$ tenemos $w_e = \bar{z}_e$. Sin embargo, hay un $e$ con $c < e < d$ e $w_e \neq \bar{z}_e$.

Para $e$ en este rango, $\bar{z}_e = y_e = 0$. Por lo $w > y$, como se desee.

Caso 3: Para todos los $e > c$, tenemos $w_e = \bar{z}_e$. Sin embargo, $w_c \neq y_c$.

Por la construcción de $y$, tenemos $w_c > y_c$ e lo $w>y$.

Caso 4: Para todos los $e \geq c$, tenemos $w_e =y_e$.

Este es el caso en el que $\delta(c)$ es cierto.

Ahora hemos demostrado que $\delta(c)$ es cierto, contradiciendo ese $d$ fue mínima. En vez de eso, $d$ se $0$. Como se describió anteriormente, esto concluye la prueba. $\square$.

---

Me temo que no entiendo corte de eliminación, pero Sawin sugiere más arriba que esto es también una respuesta a tu pregunta principal.

Answer 3

Me gusta el borrador del libro de H. Jervell sobre teoría de la prueba:

• http://folk.uio.no/herman/bevisteori.ps

Explica el uso de$\varepsilon_0$ y, como no experto, lo encontré bastante legible. Desafortunadamente no creo que pueda reconstruir el argumento de memoria, pero pensé en recomendarle el libro.