Análisis ordinal

---

En la teoría de la prueba , el análisis ordinal asigna ordinales (a menudo grandes ordinales contables ) a las teorías matemáticas como una medida de su fuerza. Si las teorías tienen el mismo ordinal teórico de prueba, a menudo son equiconsistentes , y si una teoría tiene un ordinal teórico de prueba más grande que otra, a menudo puede probar la consistencia de la segunda teoría.

El campo del análisis ordinal se formó cuando Gerhard Gentzen en 1934 usó la eliminación por corte para probar, en términos modernos, que el ordinal de la teoría de prueba de la aritmética de Peano es ε ₀ . Vea la prueba de consistencia de Gentzen .

El análisis ordinal se refiere a teorías verdaderas y efectivas (recursivas) que pueden interpretar una parte suficiente de la aritmética para hacer declaraciones sobre notaciones ordinales.

El ordinal de la teoría de la demostración de tal teoría es el supremo de los tipos de orden de todas las notaciones ordinales (necesariamente recursivas , véase la siguiente sección) que la teoría puede demostrar que están bien fundadas , el supremo de todos los ordinales para los que existe una notación en la notación de Kleene. sentido tal que prueba que es una notación ordinal . Equivalentemente, es el supremo de todos los ordinales tal que existe una relación recursiva en (el conjunto de números naturales) que lo ordena bien con el ordinal y tal que prueba${\ estilo de visualización T}$${\displaystyle \alpha }$${\displaystyle o}$${\displaystyle T}$${\displaystyle o}$${\displaystyle \alpha }$ ${\displaystyle R}$${\displaystyle \omega }$${\displaystyle \alpha }$${\displaystyle T}$inducción transfinita de enunciados aritméticos para .${\displaystyle R}$

Algunas teorías, como los subsistemas de la aritmética de segundo orden, no tienen una conceptualización ni una forma de argumentar sobre los ordinales transfinitos. Por ejemplo, para formalizar lo que significa que un subsistema de Z ₂ "demuestre estar bien ordenado", en su lugar construimos una notación ordinal con tipo de orden . ahora puede trabajar con varios principios de inducción transfinitos a lo largo de , que sustituyen el razonamiento sobre ordinales de teoría de conjuntos.${\displaystyle T}$${\displaystyle \alpha }$ ${\displaystyle (A,{\tilde {<}})}$${\displaystyle \alpha }$${\displaystyle T}$${\displaystyle (A,{\tilde {<}})}$

Sin embargo, existen algunos sistemas de notación patológicos con los que es inesperadamente difícil trabajar. Por ejemplo, Rathjen proporciona un sistema de notación recursivo primitivo que está bien fundado si PA es consistente, ^[1] a pesar de tener un tipo de orden ; incluir tal notación en el análisis ordinal de PA daría como resultado una igualdad falsa .${\displaystyle (\mathbb {N} ,<_{T})}$${\displaystyle \omega }$${\displaystyle {\mathsf {PTO(PA)}}=\omega }$

---