Análisis ordinal

Técnica matemática utilizada en la teoría de la prueba.

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

Además de obtener el ordinal demostrativo de una teoría, en la práctica el análisis ordinal suele producir también otros datos sobre la teoría que se analiza, por ejemplo caracterizaciones de las clases de funciones recursivas, hiperaritméticas o demostrables de la teoría. ^[1] ${\displaystyle \Delta _{2}^{1}}$

Historia

El campo del análisis ordinal se formó cuando Gerhard Gentzen en 1934 utilizó la eliminación de cortes para demostrar, en términos modernos, que el ordinal teórico de la demostración de la aritmética de Peano es ε 0 . Véase la demostración de consistencia de Gentzen .

Definición

El análisis ordinal se ocupa de teorías verdaderas y efectivas (recursivas) que pueden interpretar una porción suficiente de aritmética para hacer afirmaciones sobre notaciones ordinales.

El ordinal demostrativo de una teoría de este tipo 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 probar que están bien fundadas —el supremo de todos los ordinales para los que existe una notación en el sentido de Kleene tal que prueba que es una notación ordinal. Equivalentemente, es el supremo de todos los ordinales tales que existe una relación recursiva en (el conjunto de números naturales) que lo ordena bien con ordinal y tal que prueba la inducción transfinita de enunciados aritméticos para . ${\displaystyle T}$ ${\displaystyle \alpha }$ ${\displaystyle o}$ ${\displaystyle T}$ ${\displaystyle o}$ ${\displaystyle \alpha }$ ${\displaystyle R}$ ${\displaystyle \omega }$ ${\displaystyle \alpha }$ ${\displaystyle T}$ ${\displaystyle R}$

Notaciones ordinales

Algunas teorías, como los subsistemas de aritmética de segundo orden, no tienen una conceptualización o una forma de argumentar sobre los ordinales transfinitos. Por ejemplo, para formalizar lo que significa que un subsistema de Z ₂ "resulte bien ordenado", construimos en cambio una notación ordinal con el tipo de orden . ahora podemos trabajar con varios principios de inducción transfinita junto con , que sustituyen el razonamiento sobre los ordinales de la 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 resulta inesperadamente difícil trabajar. Por ejemplo, Rathjen ofrece un sistema de notación recursiva primitiva que está bien fundamentado si y solo si PA es consistente, ^{[2] p. 3} a pesar de tener un tipo de orden - incluir una notación de este tipo en el análisis ordinal de PA daría como resultado la falsa igualdad . ${\displaystyle (\mathbb {N} ,<_{T})}$ ${\displaystyle \omega }$ ${\displaystyle {\mathsf {PTO(PA)}}=\omega }$

Límite superior

Como una notación ordinal debe ser recursiva, el ordinal de prueba teórica de cualquier teoría es menor o igual que el ordinal de Church-Kleene . En particular, el ordinal de prueba teórica de una teoría inconsistente es igual a , porque una teoría inconsistente prueba trivialmente que todas las notaciones ordinales están bien fundadas. ${\displaystyle \omega _{1}^{\mathrm {CK} }}$ ${\displaystyle \omega _{1}^{\mathrm {CK} }}$

Para cualquier teoría que sea a la vez -axiomatizable y -sólida, la existencia de un orden recursivo que la teoría no puede demostrar que está bien ordenado se sigue del teorema de acotación, y dichas notaciones ordinales demostrablemente bien fundadas están de hecho bien fundadas por -sólida. Por lo tanto, el ordinal demostrativo de una teoría -sólida que tiene una axiomatización siempre será un ordinal recursivo (contable) , es decir, estrictamente menor que . ^{[2] Teorema 2.21} ${\displaystyle \Sigma _{1}^{1}}$ ${\displaystyle \Pi _{1}^{1}}$ ${\displaystyle \Sigma _{1}^{1}}$ ${\displaystyle \Pi _{1}^{1}}$ ${\displaystyle \Pi _{1}^{1}}$ ${\displaystyle \Sigma _{1}^{1}}$ ${\displaystyle \omega _{1}^{\mathrm {CK} }}$

Ejemplos

Teorías con ordinal ω demostrativo

• Q, Aritmética de Robinson (aunque la definición del ordinal de prueba teórica para tales teorías débiles debe ser ajustada) ^{[ cita requerida ]} .
• PA ^– , la teoría de primer orden de la parte no negativa de un anillo discretamente ordenado.

Teorías con ordinal ω demostrativo2

• RFA, aritmética de funciones rudimentarias . ^[3]
• IΔ ₀ , aritmética con inducción sobre predicados Δ ₀ sin ningún axioma que afirme que la exponenciación es total.

Teorías con ordinal ω demostrativo3

• EFA, aritmética de funciones elementales .
• IΔ ₀ + exp, aritmética con inducción sobre predicados Δ ₀ aumentados por un axioma que afirma que la exponenciación es total.
• RCA^*
  ₀, una forma de segundo orden de EFA que a veces se utiliza en matemáticas inversas .
• WKL^*
  ₀, una forma de segundo orden de EFA que a veces se utiliza en matemáticas inversas .

La gran conjetura de Friedman sugiere que muchas matemáticas "ordinarias" pueden demostrarse en sistemas débiles que tengan este como su ordinal de prueba teórica.

Teorías con ordinal ω demostrativonorte(paranorte= 2, 3, ... ω)

• IΔ ₀ o EFA aumentado por un axioma que garantiza que cada elemento del n -ésimo nivel de la jerarquía de Grzegorczyk es total. ${\displaystyle {\mathcal {E}}^{n}}$

Teorías con ordinal ω demostrativoω

• RCA ₀ , comprensión recursiva .
• WKL ₀ , lema de König débil .
• PRA, aritmética recursiva primitiva .
• IΣ ₁ , aritmética con inducción sobre Σ ₁ -predicados.

Teorías con ordinal ε demostrativo0

• PA, aritmética de Peano ( demostrada por Gentzen usando eliminación de corte ).
• ACA ₀ , comprensión aritmética .

Teorías con ordinal de prueba teóricaOrdinal de Feferman-Schütte Γ 0

• ATR ₀ , recursión transfinita aritmética .
• Teoría de tipo Martin-Löf con un número arbitrario de universos de niveles finitos.

Este ordinal se considera a veces el límite superior de las teorías "predicativas".

Teorías con ordinal de prueba teóricaOrdinario de Bachmann-Howard

• ID ₁ , la primera teoría de definiciones inductivas .
• KP, teoría de conjuntos de Kripke-Platek con el axioma de infinito .
• CZF, teoría de conjuntos constructivos de Zermelo-Fraenkel de Aczel .
• EON, una variante débil del sistema matemático explícito de Feferman T ₀ .

Las teorías de conjuntos de Kripke-Platek o CZF son teorías de conjuntos débiles sin axiomas para el conjunto potencia completo dado como conjunto de todos los subconjuntos. En cambio, tienden a tener axiomas de separación restringida y formación de nuevos conjuntos, o bien conceden la existencia de ciertos espacios de funciones (exponenciación) en lugar de extraerlos de relaciones mayores.

Teorías con ordinales demostrativos más grandes

Problema sin resolver en matemáticas :

¿Cuál es el ordinal demostrativo teórico de la aritmética completa de segundo orden? ^[4]

(más problemas sin resolver en matemáticas)

• ${\displaystyle \Pi _{1}^{1}{\mbox{-}}{\mathsf {CA}}_{0}}$, Π ₁ ¹ la comprensión tiene un ordinal teórico de prueba bastante grande, que fue descrito por Takeuti en términos de "diagramas ordinales", ^{[5] p. 13} y que está limitado por ψ ₀ (Ω _ω ) en la notación de Buchholz . También es el ordinal de , la teoría de definiciones inductivas finitamente iteradas. Y también el ordinal de MLW, teoría de tipos de Martin-Löf con tipos W indexados Setzer (2004). ${\displaystyle ID_{<\omega }}$
• ID _ω , la teoría de definiciones inductivas iterativas ω . Su ordinal de demostración teórica es igual al ordinal de Takeuti-Feferman-Buchholz .
• T ₀ , el sistema constructivo de matemáticas explícitas de Feferman tiene un ordinal de prueba teórica más grande, que también es el ordinal de prueba teórica de KPi, la teoría de conjuntos de Kripke-Platek con admisibles iterados y . ${\displaystyle \Sigma _{2}^{1}{\mbox{-}}{\mathsf {AC}}+{\mathsf {BI}}}$
• KPi, una extensión de la teoría de conjuntos de Kripke-Platek basada en un ordinal recursivamente inaccesible , tiene un ordinal de prueba teórica muy grande descrito en un artículo de 1983 de Jäger y Pohlers, donde I es el inaccesible más pequeño. ^[6] Este ordinal es también el ordinal de prueba teórica de . ${\displaystyle \psi (\varepsilon _{I+1})}$ ${\displaystyle \Delta _{2}^{1}{\mbox{-}}{\mathsf {CA}}+{\mathsf {BI}}}$
• KPM, una extensión de la teoría de conjuntos de Kripke-Platek basada en un ordinal de Mahlo recursivo , tiene un ordinal de prueba teórica muy grande θ, que fue descrito por Rathjen (1990).
• TTM, una extensión de la teoría de tipos de Martin-Löf mediante un universo Mahlo, tiene un ordinal de prueba teórica aún más grande . ${\displaystyle \psi _{\Omega _{1}}(\Omega _{M+\omega })}$
• ${\displaystyle {\mathsf {KP}}+\Pi _{3}-Ref}$tiene un ordinal de prueba teórica igual a , donde se refiere al primer débilmente compacto, debido a (Rathjen 1993) ${\displaystyle \Psi (\varepsilon _{K+1})}$ ${\displaystyle K}$
• ${\displaystyle {\mathsf {KP}}+\Pi _{\omega }-Ref}$tiene un ordinal de prueba teórica igual a , donde se refiere al primer -indescriptible y , debido a (Stegert 2010). ${\displaystyle \Psi _{X}^{\varepsilon _{\Xi +1}}}$ ${\displaystyle \Xi }$ ${\displaystyle \Pi _{0}^{2}}$ ${\displaystyle \mathbb {X} =(\omega ^{+};P_{0};\epsilon ,\epsilon ,0)}$
• ${\displaystyle {\mathsf {Stability}}}$tiene un ordinal de prueba teórica igual a donde es un análogo cardinal del ordinal menos estable para todos y , debido a (Stegert 2010). ${\displaystyle \Psi _{\mathbb {X} }^{\varepsilon _{\Upsilon +1}}}$ ${\displaystyle \Upsilon }$ ${\displaystyle \alpha }$ ${\displaystyle \alpha +\beta }$ ${\displaystyle \beta <\alpha }$ ${\displaystyle \mathbb {X} =(\omega ^{+};P_{0};\epsilon ,\epsilon ,0)}$

La mayoría de las teorías capaces de describir el conjunto potencia de los números naturales tienen ordinales demostrativos que son tan grandes que aún no se ha dado una descripción combinatoria explícita. Esto incluye , la aritmética de segundo orden completa ( ) y las teorías de conjuntos con conjuntos potencia que incluyen ZF y ZFC. La fuerza de ZF intuicionista (IZF) es igual a la de ZF. ${\displaystyle \Pi _{2}^{1}-CA_{0}}$ ${\displaystyle \Pi _{\infty }^{1}-CA_{0}}$

Tabla de análisis ordinales

Llave

Esta es una lista de símbolos utilizados en esta tabla:

• ψ representa varias funciones de colapso ordinales tal como se definen en sus respectivas citas.
• Ψ representa el Psi de Rathjen o de Stegert.
• φ representa la función de Veblen.
• ω representa el primer ordinal transfinito.
• ε _α representa los números épsilon .
• Γ _α representa los números gamma (Γ ₀ es el ordinal de Feferman-Schütte )
• Ω _α representa los ordinales incontables (Ω ₁ , abreviado Ω, es ω 1 ). Se considera que la contabilidad es necesaria para que un ordinal se considere demostrable.
• ${\displaystyle \mathbb {S} }$es un término ordinal que denota un ordinal estable y el ordinal menos admisible por encima de . ${\displaystyle \mathbb {S} ^{+}}$ ${\displaystyle \mathbb {S} }$
• ${\displaystyle \mathbb {I} _{N}}$es un término ordinal que denota un ordinal tal que ; N es una variable que define una serie de análisis ordinales de los resultados de forall . cuando N=1, ${\displaystyle L_{\mathbb {I} _{N}}\models {\mathsf {KP}}\omega +\Pi _{N}-{\mathsf {Collection}}+(V=L)}$ ${\displaystyle \Pi _{N}-{\mathsf {Collection}}}$ ${\displaystyle 1\leq N<\omega }$ ${\displaystyle \psi _{\omega _{1}^{CK}}(\varepsilon _{\mathbb {I} _{1}+1})=\psi _{\omega _{1}^{CK}}(\varepsilon _{\mathbb {I} +1})}$

Esta es una lista de las abreviaturas utilizadas en esta tabla:

• Aritmética de primer orden
  • ${\displaystyle {\mathsf {Q}}}$¿Es aritmética Robinson?
  • ${\displaystyle {\mathsf {PA}}^{-}}$es la teoría de primer orden de la parte no negativa de un anillo discretamente ordenado.
  • ${\displaystyle {\mathsf {RFA}}}$Es una función aritmética rudimentaria .
  • ${\displaystyle {\mathsf {I\Delta }}_{0}}$es aritmética con inducción restringida a Δ ₀ -predicados sin ningún axioma que afirme que la exponenciación es total.
  • ${\displaystyle {\mathsf {EFA}}}$Es una función aritmética elemental .
  • ${\displaystyle {\mathsf {I\Delta }}_{0}^{\mathsf {+}}}$es aritmética con inducción restringida a Δ ₀ -predicados aumentados por un axioma que afirma que la exponenciación es total.
  • ${\displaystyle {\mathsf {EFA}}^{\mathsf {n}}}$es una función aritmética elemental aumentada por un axioma que asegura que cada elemento del n -ésimo nivel de la jerarquía de Grzegorczyk es total. ${\displaystyle {\mathcal {E}}^{n}}$
  • ${\displaystyle {\mathsf {I\Delta }}_{0}^{\mathsf {n+}}}$se amplía con un axioma que garantiza que cada elemento del nivel n -ésimo de la jerarquía de Grzegorczyk es total. ${\displaystyle {\mathsf {I\Delta }}_{0}^{\mathsf {+}}}$ ${\displaystyle {\mathcal {E}}^{n}}$
  • ${\displaystyle {\mathsf {PRA}}}$es aritmética recursiva primitiva .
  • ${\displaystyle {\mathsf {I\Sigma }}_{1}}$es aritmética con inducción restringida a Σ ₁ -predicados.
  • ${\displaystyle {\mathsf {PA}}}$es aritmética de Peano .
  • ${\displaystyle {\mathsf {ID}}_{\nu }\#}$es pero con inducción solo para fórmulas positivas. ${\displaystyle {\widehat {\mathsf {ID}}}_{\nu }}$
  • ${\displaystyle {\widehat {\mathsf {ID}}}_{\nu }}$extiende PA mediante ν puntos fijos iterados de operadores monótonos.
  • ${\displaystyle {\mathsf {U(PA)}}}$No es exactamente un sistema aritmético de primer orden, pero captura lo que se puede obtener mediante el razonamiento predicativo basado en los números naturales.
  • ${\displaystyle {\mathsf {Aut({\widehat {ID}})}}}$se itera de forma autónoma (en otras palabras, una vez que se define un ordinal, puede usarse para indexar una nueva serie de definiciones). ${\displaystyle {\widehat {\mathsf {ID}}}_{\nu }}$
  • ${\displaystyle {\mathsf {ID}}_{\nu }}$extiende PA por ν iterados menos puntos fijos de operadores monótonos.
  • ${\displaystyle {\mathsf {U(ID}}_{\nu }{\mathsf {)}}}$no es exactamente un sistema aritmético de primer orden, pero captura lo que se puede obtener mediante el razonamiento predicativo basado en definiciones inductivas generalizadas iteradas n-veces.
  • ${\displaystyle {\mathsf {Aut(U(ID))}}}$se itera de forma autónoma . ${\displaystyle {\mathsf {U(ID}}_{\nu }{\mathsf {)}}}$
  • ${\displaystyle {\mathsf {W-ID}}_{\nu }}$Es una versión debilitada basada en tipos W. ${\displaystyle {\mathsf {ID}}_{\nu }}$
  • ${\displaystyle {\mathsf {TI}}[\Pi _{0}^{1-},\alpha ]}$es una inducción transfinita de longitud α no mayor que -fórmulas. Resulta ser la representación de la notación ordinal cuando se utiliza en aritmética de primer orden. ${\displaystyle \Pi _{0}^{1}}$

• Aritmética de segundo orden

En general, un subíndice 0 significa que el esquema de inducción está restringido a un solo conjunto de axiomas de inducción.

• • ${\displaystyle {\mathsf {RCA}}_{0}^{*}}$es una forma de segundo orden que a veces se utiliza en matemáticas inversas . ${\displaystyle {\mathsf {EFA}}}$
  • ${\displaystyle {\mathsf {WKL}}_{0}^{*}}$es una forma de segundo orden que a veces se utiliza en matemáticas inversas. ${\displaystyle {\mathsf {EFA}}}$
  • ${\displaystyle {\mathsf {RCA}}_{0}}$Es comprensión recursiva .
  • ${\displaystyle {\mathsf {WKL}}_{0}}$es un lema de König débil .
  • ${\displaystyle {\mathsf {ACA}}_{0}}$Es comprensión aritmética .
  • ${\displaystyle {\mathsf {ACA}}}$es más el esquema de inducción de segundo orden completo. ${\displaystyle {\mathsf {ACA}}_{0}}$
  • ${\displaystyle {\mathsf {ATR}}_{0}}$es recursión transfinita aritmética .
  • ${\displaystyle {\mathsf {ATR}}}$es más el esquema de inducción de segundo orden completo. ${\displaystyle {\mathsf {ATR}}_{0}}$
  • ${\displaystyle {\mathsf {\Delta }}_{2}^{1}{\mathsf {-CA+BI+(M)}}}$es más la afirmación "toda oración verdadera con parámetros se cumple en un modelo (codificado contable) de ". ${\displaystyle {\mathsf {\Delta }}_{2}^{1}{\mathsf {-CA+BI}}}$ ${\displaystyle {\mathsf {\Pi }}_{3}^{1}}$ ${\displaystyle \beta }$ ${\displaystyle {\mathsf {\Delta }}_{2}^{1}{\mathsf {-CA}}}$

• Teoría de conjuntos de Kripke-Platek
  • ${\displaystyle {\mathsf {KP}}}$Es la teoría de conjuntos de Kripke-Platek con el axioma de infinito.
  • ${\displaystyle {\mathsf {KP\omega }}}$es la teoría de conjuntos de Kripke-Platek, cuyo universo es un conjunto admisible que contiene . ${\displaystyle \omega }$
  • ${\displaystyle {\mathsf {W-KPI}}}$Es una versión debilitada basada en tipos W. ${\displaystyle {\mathsf {KPI}}}$
  • ${\displaystyle {\mathsf {KPI}}}$afirma que el universo es un límite de conjuntos admisibles.
  • ${\displaystyle {\mathsf {W-KPi}}}$Es una versión debilitada basada en tipos W. ${\displaystyle {\mathsf {KPi}}}$
  • ${\displaystyle {\mathsf {KPi}}}$Afirma que el universo es un conjunto inaccesible.
  • ${\displaystyle {\mathsf {KPh}}}$afirma que el universo es hiperinaccesible: un conjunto inaccesible y un límite de conjuntos inaccesibles.
  • ${\displaystyle {\mathsf {KPM}}}$Afirma que el universo es un conjunto de Mahlo.
  • ${\displaystyle {\mathsf {KP+\Pi }}_{\mathsf {n}}-{\mathsf {Ref}}}$se amplía mediante un cierto esquema de reflexión de primer orden. ${\displaystyle {\mathsf {KP}}}$
  • ${\displaystyle {\mathsf {Stability}}}$es KPi aumentado por el axioma . ${\displaystyle \forall \alpha \exists \kappa \geq \alpha (L_{\kappa }\preceq _{1}L_{\kappa +\alpha })}$
  • ${\displaystyle {\mathsf {KPM}}^{+}}$El KPI se amplía con la afirmación "existe al menos un ordinal Mahlo recursivo".
  • ${\displaystyle {\mathsf {KP}}\omega +(M\prec _{\Sigma _{1}}V)}$se trata de un axioma que establece que 'existe un conjunto no vacío y transitivo M tal que '. ${\displaystyle {\mathsf {KP}}\omega }$ ${\displaystyle M\prec _{\Sigma _{1}}V}$

Un superíndice cero indica que se elimina la -inducción (lo que hace que la teoría sea significativamente más débil). ${\displaystyle \in }$

• Teoría de tipos
  • ${\displaystyle {\mathsf {CPRC}}}$es el cálculo Herbelin-Patey de construcciones recursivas primitivas.
  • ${\displaystyle {\mathsf {ML}}_{\mathsf {n}}}$es teoría de tipos sin tipos W y con universos. ${\displaystyle n}$
  • ${\displaystyle {\mathsf {ML}}_{<\omega }}$es una teoría de tipos sin W-tipos y con un número finito de universos.
  • ${\displaystyle {\mathsf {MLU}}}$Es una teoría de tipos con un operador de universo próximo.
  • ${\displaystyle {\mathsf {MLS}}}$es una teoría de tipos sin tipos W y con un superuniverso.
  • ${\displaystyle {\mathsf {Aut(ML)}}}$es un automorfismo en la teoría de tipos sin W-tipos.
  • ${\displaystyle {\mathsf {ML}}_{1}{\mathsf {V}}}$es la teoría de tipos con un universo y el tipo de conjuntos iterativos de Aczel.
  • ${\displaystyle {\mathsf {MLW}}}$es teoría de tipos con tipos W indexados.
  • ${\displaystyle {\mathsf {ML}}_{1}{\mathsf {W}}}$Es una teoría de tipos con tipos W y un universo.
  • ${\displaystyle {\mathsf {ML}}_{<\omega }{\mathsf {W}}}$Es una teoría de tipos con W-tipos y un número finito de universos.
  • ${\displaystyle {\mathsf {Aut(MLW)}}}$es un automorfismo en la teoría de tipos con tipos W.
  • ${\displaystyle {\mathsf {TTM}}}$Es una teoría de tipos con un universo de Mahlo.
  • ${\displaystyle \lambda 2}$es el Sistema F , también cálculo lambda polimórfico o cálculo lambda de segundo orden.

• Teoría de conjuntos constructivos
  • ${\displaystyle {\mathsf {CZF}}}$Es la teoría de conjuntos constructivos de Aczel.
  • ${\displaystyle {\mathsf {CZF+REA}}}$es más el axioma de extensión regular. ${\displaystyle {\mathsf {CZF}}}$
  • ${\displaystyle {\mathsf {CZF+REA+FZ}}_{2}}$es más el esquema de inducción de segundo orden completo. ${\displaystyle {\mathsf {CZF+REA}}}$
  • ${\displaystyle {\mathsf {CZFM}}}$está con un universo Mahlo. ${\displaystyle {\mathsf {CZF}}}$

• Matemáticas explícitas
  • ${\displaystyle {\mathsf {EM}}_{0}}$Es matemática explícita básica más comprensión elemental.
  • ${\displaystyle {\mathsf {EM}}_{0}{\mathsf {+JR}}}$¿ Es más la regla de unión? ${\displaystyle {\mathsf {EM}}_{0}}$
  • ${\displaystyle {\mathsf {EM}}_{0}{\mathsf {+J}}}$es más unir axiomas ${\displaystyle {\mathsf {EM}}_{0}}$
  • ${\displaystyle {\mathsf {EON}}}$es una variante débil del Feferman . ${\displaystyle {\mathsf {T}}_{0}}$
  • ${\displaystyle {\mathsf {T}}_{0}}$es , donde es generación inductiva. ${\displaystyle {\mathsf {EM}}_{0}{\mathsf {+J+IG}}}$ ${\displaystyle {\mathsf {IG}}}$
  • ${\displaystyle {\mathsf {T}}}$es , donde es el esquema de inducción de segundo orden completo. ${\displaystyle {\mathsf {EM}}_{0}{\mathsf {+J+IG+FZ}}_{2}}$ ${\displaystyle {\mathsf {FZ}}_{2}}$

Véase también

• Equiconsistencia
• Gran propiedad cardinal
• Ordinal de Feferman-Schütte
• Ordinario de Bachmann-Howard
• Clase de complejidad
• Prueba de consistencia de Gentzen

Notas

1. ^ Para ${\displaystyle 1<n\leq \omega }$

2. ^ La función de Veblen con mínimos puntos fijos iterados infinitamente y numerables. ^{[ aclaración necesaria ]} ${\displaystyle \varphi }$

3. ^ También se puede escribir comúnmente como ψ de Madore. ${\displaystyle \psi (\varepsilon _{\Omega +1})}$

4. ^ Utiliza ψ de Madore en lugar de ψ de Buchholz.

5. ^ También se puede escribir comúnmente como ψ de Madore. ${\displaystyle \psi (\varepsilon _{\Omega _{\omega }+1})}$

6. ^ representa el primer ordinal recursivamente compacto débil. Utiliza ψ de Arai en lugar de ψ de Buchholz. ${\displaystyle K}$

7. ^ También el ordinal de prueba teórica de , ya que la cantidad de debilitamiento dada por los tipos W no es suficiente. ${\displaystyle {\mathsf {Aut(W-ID)}}}$

8. ^ representa el primer cardinal inaccesible. Utiliza el ψ de Jäger en lugar del ψ de Buchholz. ${\displaystyle I}$

9. ^ representa el límite de los cardinales inaccesibles. Utiliza (presumiblemente) el ψ de Jäger. ${\displaystyle L}$ ${\displaystyle \omega }$

10. ^ representa el límite de los cardinales inaccesibles. Utiliza (presumiblemente) el ψ de Jäger. ${\displaystyle L^{*}}$ ${\displaystyle \Omega }$

11. ^ representa el primer cardinal de Mahlo. Utiliza el ψ de Rathjen en lugar del ψ de Buchholz. ${\displaystyle M}$

12. ^ representa el primer cardinal débilmente compacto. Utiliza el Ψ de Rathjen en lugar del ψ de Buchholz. ${\displaystyle K}$

13. ^ representa el primer cardinal indescriptible. Utiliza el Ψ de Stegert en lugar del ψ de Buchholz. ${\displaystyle \Xi }$ ${\displaystyle \Pi _{0}^{2}}$

14. ^ es el más pequeño tal que ' es -indescriptible') y ' es -indescriptible '). Utiliza Ψ de Stegert en lugar de ψ de Buchholz. ${\displaystyle Y}$ ${\displaystyle \alpha }$ ${\displaystyle \forall \theta <Y\exists \kappa <Y(}$ ${\displaystyle \kappa }$ ${\displaystyle \theta }$ ${\displaystyle \forall \theta <Y\forall \kappa <Y(}$ ${\displaystyle \kappa }$ ${\displaystyle \theta }$ ${\displaystyle \rightarrow \theta <\kappa }$

15. ^ representa el primer cardinal de Mahlo. Utiliza (presumiblemente) el ψ de Rathjen. ${\displaystyle M}$

Citas

1. M. Rathjen, "Teoría de la prueba admisible y más allá". En Estudios de lógica y fundamentos de las matemáticas, vol. 134 (1995), págs. 123-147.
2. Rathjen, El reino del análisis ordinal. Consultado el 29 de septiembre de 2021.
3. Krajicek, Jan (1995). Aritmética limitada, lógica proposicional y teoría de la complejidad. Cambridge University Press. pp. 18-20. ISBN 9780521452052.define los conjuntos rudimentarios y las funciones rudimentarias, y demuestra que son equivalentes a los predicados Δ ₀ de los números naturales. Se puede encontrar un análisis ordinal del sistema en Rose, HE (1984). Subrecursion: functions and hierarchies . Universidad de Michigan: Clarendon Press. ISBN 9780198531890.
4. M. Rathjen, Proof Theory: From Arithmetic to Set Theory (p. 28). Consultado el 14 de agosto de 2022.
5. Rathjen, Michael (2006), "El arte del análisis ordinal" (PDF) , Congreso Internacional de Matemáticos , vol. II, Zúrich: Eur. Math. Soc., pp. 45–69, MR  2275588, archivado desde el original el 22 de diciembre de 2009{{citation}}: CS1 maint: bot: original URL status unknown (link)
6. D. Madore, Un zoológico de ordinales (2017, p.2). Consultado el 12 de agosto de 2022.
7. J. Avigad, R. Sommer, "Un enfoque teórico-modelo para el análisis ordinal" (1997).
8. M. Rathjen, W. Carnielli, "Hidras y subsistemas de la aritmética" (1991)
9. Jeroen Van der Meeren; Rathjen, Michael; Weiermann, Andreas (2014). "Una caracterización teórica del orden de la jerarquía de Howard-Bachmann". arXiv : 1411.4481 [matemáticas.LO].
10. G. Jäger, T. Strahm, "Teorías de segundo orden con ordinales y comprensión elemental".
11. G. Jäger, "La fuerza de la admisibilidad sin fundamento". Journal of Symbolic Logic vol. 49, núm. 3 (1984).
12. B. Afshari, M. Rathjen, "Análisis ordinal y el teorema infinito de Ramsey" (2012)
13. Marcone, Alberto; Montalbán, Antonio (2011). "Las funciones de Veblen para los teóricos de la computabilidad". The Journal of Symbolic Logic . 76 (2): 575–602. arXiv : 0910.5442 . doi :10.2178/jsl/1305810765. S2CID  675632.
14. S. Feferman, "Teorías de tipo finito relacionadas con la práctica matemática". En Handbook of Mathematical Logic , Studies in Logic and the Foundations of Mathematics vol. 90 (1977), ed. J. Barwise, pub. Holanda Septentrional.
15. M. Heissenbüttel, "Teorías de la fuerza ordinal y " (2001) ${\displaystyle \varphi 20}$ ${\displaystyle \varphi 2\varepsilon _{0}}$
16. D. Probst, "Un análisis ordinal modular de subsistemas metapredicativos de aritmética de segundo orden" (2017)
17. A. Cantini, "Sobre la relación entre los principios de elección y comprensión en la aritmética de segundo orden", Journal of Symbolic Logic vol. 51 (1986), págs. 360--373.
18. Fischer, Martin; Nicolai, Carlo; Pablo Dopico Fernandez (2020). "Verdad no clásica con fuerza clásica. Un análisis teórico de la prueba de la verdad compositiva sobre HYPE". arXiv : 2007.07188 [math.LO].
19. SG Simpson, "Investigación de Friedman sobre subsistemas de aritmética de segundo orden". En Investigación de Harvey Friedman sobre los fundamentos de las matemáticas , Estudios de lógica y fundamentos de las matemáticas vol. 117 (1985), ed. L. Harrington, M. Morley, A. Šcedrov, SG Simpson, pub. Holanda Septentrional.
20. J. Avigad, "Análisis ordinal de la teoría de conjuntos admisibles utilizando recursión en notaciones ordinales". Journal of Mathematical Logic vol. 2, no. 1, pp.91--112 (2002).
21. S. Feferman, "Teorías iterativas inductivas de punto fijo: aplicación de la conjetura de Hancock". En Patras Logic Symposion , Studies in Logic and the Foundations of Mathematics vol. 109 (1982).
22. S. Feferman, T. Strahm, "El desarrollo de la aritmética no finitista", Annals of Pure and Applied Logic vol. 104, no.1--3 (2000), pp.75--96.
23. S. Feferman, G. Jäger, "Principios de elección, la regla de la barra y esquemas de comprensión iterados de forma autónoma en el análisis", Journal of Symbolic Logic vol. 48, no. (1983), pp.63--70.
24. U. Buchholtz, G. Jäger, T. Strahm, "Teorías de la fuerza teórica de la prueba ψ ( Γ Ω + 1 ) {\displaystyle \psi (\Gamma _{\Omega +1})}". En Conceptos de prueba en matemáticas, filosofía y ciencias de la computación (2016), ed. D. Probst, P. Schuster. DOI 10.1515/9781501502620-007.
25. T. Strahm, "Progresiones autónomas de punto fijo y recursión transfinita de punto fijo" (2000). En Logic Colloquium '98 , ed. SR Buss, P. Hájek y P. Pudlák. DOI 10.1017/9781316756140.031
26. G. Jäger, T. Strahm, "Teorías del punto fijo y elección dependiente". Archivo de lógica matemática vol. 39 (2000), pp.493--508.
27. T. Strahm, "Progresiones autónomas de punto fijo y recursión transfinita de punto fijo" (2000)
28. C. Rüede, "Elección dependiente transfinita y reflexión sobre el modelo ω". Journal of Symbolic Logic vol. 67, núm. 3 (2002).
29. C. Rüede, "El análisis teórico de la demostración de la elección dependiente transfinita Σ11". Annals of Pure and Applied Logic vol. 122 (2003).
30. T. Strahm, "Pruebas de ordenación adecuada para el Mahlo metapredicativo". Journal of Symbolic Logic, vol. 67, n.º 1 (2002)
31. F. Ranzi, T. Strahm, "Un sistema de tipos flexible para el ordinal pequeño de Veblen" (2019). Archivo de Lógica Matemática 58: 711–751.
32. K. Fujimoto, "Notas sobre algunos sistemas de segundo orden de definiciones y comprensiones inductivas iteradas y subsistemas relevantes de la teoría de conjuntos". Annals of Pure and Applied Logic, vol. 166 (2015), págs. 409--463. ${\displaystyle \Pi _{1}^{1}}$
33. Krombholz, Martin; Rathjen, Michael (2019). "Límites superiores del teorema del grafo menor". arXiv : 1907.00412 [math.LO].
34. W. Buchholz, S. Feferman, W. Pohlers, W. Sieg, Definiciones inductivas iteradas y subsistemas de análisis: estudios teóricos de prueba recientes
35. W. Buchholz, Teoría de la prueba de subsistemas impredicativos de análisis (Estudios en teoría de la prueba, Monografías, Vol 2 (1988))
36. M. Rathjen, "Investigaciones de subsistemas de aritmética de segundo orden y teoría de conjuntos en fuerza entre Π 1 1 − C A {\displaystyle \Pi _{1}^{1}{\mathsf {-CA}}} y Δ 2 1 − C A + B I {\displaystyle \Delta _{2}^{1}{\mathsf {-CA+BI}}} : Parte I". Consultado el 21 de septiembre de 2023.
37. M. Rathjen, "La fuerza de algunas teorías de tipos de Martin-Löf"
38. Véase el resultado de conservatividad en Rathjen (1996), "La propiedad recursiva de Mahlo en la aritmética de segundo orden", Math. Log. Quart. , 42dando el mismo ordinal que ${\displaystyle {\mathsf {KPM}}}$
39. A. Setzer, "Un modelo para una teoría de tipos con universo de Mahlo" (1996).
40. M. Rathjen, "Teoría de la demostración de la reflexión". Anales de lógica pura y aplicada, vol. 68, núm. 2 (1994), págs. 181-224.
41. Stegert, Jan-Carl, "Teoría de prueba ordinal de la teoría de conjuntos de Kripke-Platek aumentada por principios de reflexión fuerte" (2010).
42. Arai, Toshiyasu (1 de abril de 2023). "Conferencias sobre análisis ordinal". arXiv : 2304.00246 [math.LO].
43. Arai, Toshiyasu (7 de abril de 2023). "Prueba de fundamento para la -reflexión". arXiv : 2304.03851 [math.LO]. ${\displaystyle \Pi _{1}^{1}}$
44. Arai, Toshiyasu (12 de febrero de 2024). "Un análisis ordinal de -Collection". arXiv : 2311.12459 [math.LO]. ${\displaystyle \Pi _{N}}$
45. Valentin Blot. "Una interpretación computacional directa de la aritmética de segundo orden mediante recursión de actualización" (2022).

Referencias

• Buchholz, W.; Feferman, S.; Pohlers, W.; Sieg, W. (1981), Definiciones inductivas iteradas y subsistemas de análisis , Lecture Notes in Math., vol. 897, Berlín: Springer-Verlag, doi :10.1007/BFb0091894, ISBN 978-3-540-11170-2
• Pohlers, Wolfram (1989), Proof Theory , Lecture Notes in Mathematics, vol. 1407, Berlín: Springer-Verlag, doi :10.1007/978-3-540-46825-7, ISBN 3-540-51842-8, Sr.  1026933
• Pohlers, Wolfram (1998), "Teoría de conjuntos y teoría de números de segundo orden", Handbook of Proof Theory , Studies in Logic and the Foundations of Mathematics, vol. 137, Ámsterdam: Elsevier Science BV, págs. 210–335, doi :10.1016/S0049-237X(98)80019-0, ISBN 0-444-89840-9, Sr.  1640328
• Rathjen, Michael (1990), "Notaciones ordinales basadas en un cardinal débilmente Mahlo", Arch. Math. Logic , 29 (4): 249–263, doi :10.1007/BF01651328, MR  1062729, S2CID  14125063
• Rathjen, Michael (2006), "El arte del análisis ordinal" (PDF) , Congreso Internacional de Matemáticos , vol. II, Zúrich: Eur. Math. Soc., pp. 45–69, MR  2275588, archivado desde el original el 22 de diciembre de 2009{{citation}}: CS1 maint: bot: original URL status unknown (link)
• Rose, HE (1984), Subrecursion. Funciones y jerarquías , Oxford logic guides, vol. 9, Oxford, Nueva York: Clarendon Press, Oxford University Press
• Schütte, Kurt (1977), Teoría de la prueba , Grundlehren der Mathematischen Wissenschaften, vol. 225, Berlín-Nueva York: Springer-Verlag, págs. xii+299, ISBN 3-540-07911-4, Sr.  0505313
• Setzer, Anton (2004), "Teoría de la prueba de la teoría de tipos de Martin-Löf. Una descripción general", Mathématiques et Sciences Humaines. Matemáticas y Ciencias Sociales (165): 59–99
• Takeuti, Gaisi (1987), Teoría de la prueba , Estudios de lógica y fundamentos de las matemáticas, vol. 81 (segunda edición), Ámsterdam: North-Holland Publishing Co., ISBN 0-444-87943-9, Sr.  0882549
• Rathjen, Michael (1994), "Teoría de la prueba de la reflexión", Anales de lógica pura y aplicada , 68 (2): 181–224, doi :10.1016/0168-0072(94)90074-4
• Stegert, Jan-Carl (2010), Teoría de la prueba ordinal de la teoría de conjuntos de Kripke-Platek aumentada por principios de reflexión fuerte