Análisis ordinal

El análisis ordinal mide la fuerza de una teoría formal mediante el ordinal más pequeño que la teoría no puede probar que está bien ordenado, asignando un ordinal preciso de la teoría de la prueba a cada teoría.

Definition

El ordinal de la teoría de la prueba de una teoría es el supremo de los tipos de orden de los buenos órdenes recursivos cuya buena fundamentación la teoría puede probar; el análisis ordinal es el programa para calcular este invariante y usarlo para comparar y calibrar teorías.

Scope

Este tema cubre la prueba de consistencia de Gentzen para la aritmética utilizando la inducción transfinitiva hasta el ordinal épsilon-cero, los sistemas de notación ordinal, el ordinal de la teoría de la prueba como un invariante de una teoría, los métodos de eliminación de cortes para derivaciones infinitarias y el análisis de subsistemas de aritmética y teorías predicativas.

Core questions

• ¿Cómo mide un ordinal la fuerza de una teoría aritmética?
• ¿Por qué la inducción transfinitiva hasta épsilon-cero prueba la consistencia de la aritmética?
• ¿Cómo se definen las notaciones ordinales para que puedan ser razonadas de forma finita?
• ¿Qué ordinales corresponden a los subsistemas estándar de la aritmética de segundo orden?

Key theories

Prueba de consistencia de Gentzen

Gentzen demostró la consistencia de la aritmética de primer orden asignando ordinales por debajo de épsilon-cero a las pruebas y mostrando que la reducción de cortes las disminuye, por lo que la inducción transfinitiva hasta épsilon-cero certifica la consistencia.

Ordinal de la teoría de la prueba

Cada teoría suficientemente fuerte tiene un ordinal característico que captura la inducción transfinitiva que puede justificar, proporcionando una escala de fuerza lógica de grano fino y en gran medida lineal.

Sistemas de notación ordinal

Los ordinales grandes se representan mediante notaciones sintácticas finitas, como las funciones de Veblen y las funciones de colapso, lo que permite manipular ordinales infinitos dentro de teorías finitas o aritméticas.

Clinical relevance

El análisis ordinal proporciona la medida más refinada disponible de la fuerza de las teorías matemáticas: determina exactamente qué inducciones transfinitas necesita una teoría, clasifica las funciones recursivas demostrables de una teoría y proporciona información de consistencia relativa complementaria a la obtenida de los cardinales grandes.

History

Las pruebas de consistencia de Gentzen de 1936 y 1938 para la aritmética introdujeron el análisis ordinal a través de la inducción transfinitiva hasta épsilon-cero. Schuette, Feferman y otros extendieron el método a teorías predicativas y análisis ramificado, y el desarrollo de funciones de colapso impulsó posteriormente el análisis ordinal hacia sistemas impredicativos fuertes.

Key figures

• Gerhard Gentzen
• Kurt Schuette
• Solomon Feferman
• Wolfram Pohlers

Seminal works

• pohlers2009
• takeuti1987
• schutte1977

Frequently asked questions

What is the proof-theoretic ordinal of first-order arithmetic?

Es épsilon-cero, el límite de la torre de exponenciales omega. La aritmética de primer orden prueba la inducción transfinitiva hasta cualquier ordinal por debajo de épsilon-cero, pero no hasta épsilon-cero mismo, que es exactamente el principio que Gentzen usó para probar su consistencia.

How does ordinal analysis relate to incompleteness?

El segundo teorema de Goedel dice que la aritmética no puede probar su propia consistencia. El análisis ordinal identifica el principio adicional, la inducción transfinitiva hasta épsilon-cero, que sí la prueba, midiendo así con precisión cuán lejos más allá de la teoría se debe llegar para establecer su consistencia.