Gödel 2 dice que ninguna subteoría de PA puede demostrar que Con $_{PA}$ y aunque la mayoría de las teorías naturales $T$ ampliar la AP puede probar Con $_{PA}$ Esto es relativamente poco interesante, ya que cualquier persona que dude de la consistencia de la AP seguramente desconfiaría $T$ . Si todas las teorías "naturales" estuvieran totalmente ordenadas sería el fin, pero el significado de La prueba de consistencia de Gentzen es que establece Con $_{PA}$ de un sistema incomparable PRA + $\epsilon_0$ que uno puede creer sin confiar ya en la AP en primer lugar.
Para ver que PRA + $\epsilon_0 \not\subseteq$ PA, es sencillo, ya que este último demuestra la inducción hasta $\epsilon_0$ , Con $_{PA}$ y el teorema de Goodstein, ninguno de los cuales PA puede demostrar (si es consistente).
Pero mostrando PA $\not\subseteq$ PRA + $\epsilon_0$ me hace rascarme la cabeza. Wikipedia reclamos esta última "no demuestra la inducción matemática ordinaria para todas las fórmulas", lo que sí hace la AP por definición. Pero allí no se da ninguna justificación o referencia, y no es obvio para mí (ni para mi director de tesis) cómo probar esta afirmación (asumiendo una metateoría que pueda probar su consistencia y quizás más).
También estoy interesado en saber si hay alguna otra afirmación (idealmente "natural") que la AP demuestre pero la ARP + $\epsilon_0$ no lo hace. Se me ocurren muy pocas cosas que la AP pruebe, pero la ARP por sí sola no lo hace, y es parece necesariamente se tratará de funciones de rápido crecimiento como la de Ackermann. Así, por ejemplo, la totalidad de Ackermann es el ejemplo clásico de algo que PA puede demostrar pero no PRA, pero si no me equivoco esa afirmación también puede demostrarse por inducción hasta $\omega^\omega$ por lo que no resuelve esta cuestión. Para resumir:
¿Cómo demostramos de forma rigurosa que PRA + $\epsilon_0$ no demuestra el esquema de inducción de PA? ¿Hay otros enunciados que tengan esta propiedad, y por qué?
