Análisis ordinal

Mathematical technique used in proof theory

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 solidez. Si las teorías tienen el mismo ordinal de teoría de prueba, a menudo son equiconsistentes , y si una teoría tiene un ordinal de teoría de prueba mayor que otra, a menudo puede probar la consistencia de la segunda teoría.

Además de obtener el ordinal de la teoría de prueba de una teoría, en la práctica el análisis ordinal generalmente también proporciona otros datos sobre la teoría que se está analizando, por ejemplo, caracterizaciones de las clases de funciones demostrablemente recursivas, hiperaritméticas o 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 de la teoría de la prueba de la aritmética de Peano es ε 0 . Véase la prueba de coherencia de Gentzen .

Definición

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

El ordinal de la teoría de la prueba de tal teoría es el supremo de los tipos de orden de todas las notaciones ordinales (necesariamente recursivas , ver la siguiente sección) que la teoría puede demostrar que están bien fundadas : el supremo de todos los ordinales para los cuales existe una notación en Kleene. sentido tal que demuestra que es una notación ordinal. De manera equivalente, 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 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 la aritmética de segundo orden, no tienen conceptualización ni forma de presentar argumentos sobre los ordinales transfinitos. Por ejemplo, para formalizar lo que significa que un subsistema de Z ₂ "resulte estar bien ordenado", construimos en su lugar 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 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ógica con los que es inesperadamente difícil trabajar. Por ejemplo, Rathjen ofrece un sistema de notación recursiva primitivo que está bien fundamentado si y sólo si PA es consistente, ^{[2] p. 3} a pesar de tener un tipo de orden : incluir dicha 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 }$

límite superior

Para cualquier teoría que sea axiomatizable y sólida, la existencia de un orden recursivo que la teoría no logra demostrar que está bien ordenada se deriva del teorema de la limitación, y dichas notaciones ordinales demostrablemente bien fundadas están de hecho bien fundadas por la solidez. . Así, el ordinal de la teoría de la prueba de una teoría sólida que tiene una axiomatización siempre será un ordinal recursivo (contable) , es decir, menor que el ordinal de Church-Kleene . ^{[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 de teoría de prueba ω

• Q, aritmética de Robinson (aunque la definición del ordinal de la teoría de la prueba para teorías tan débiles debe modificarse) ^{[ cita necesaria ]} .
• PA ^– , la teoría de primer orden de la parte no negativa de un anillo discretamente ordenado.

Teorías con ordinal de teoría de prueba ω 2

• 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 de teoría de prueba ω 3

• 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 utilizada a veces en matemáticas inversas .
• WKL^*
  ₀, una forma de segundo orden de EFA utilizada a veces en matemáticas inversas .

La gran conjetura de Friedman sugiere que muchas matemáticas "ordinarias" pueden demostrarse en sistemas débiles que tienen esto como su ordinal de teoría de prueba.

Teorías con ordinal de teoría de prueba ω n (para n = 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 de teoría de prueba ω ω

• 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 de teoría de prueba ε 0

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

Teorías con el ordinal de teoría de prueba, el ordinal de Feferman-Schütte Γ 0

• ATR ₀ , recursividad transfinita aritmética .
• Teoría de tipos de Martin-Löf con arbitrariamente muchos universos de niveles finitos.

A veces se considera que este ordinal es el límite superior de las teorías "predicativas".

Teorías con el ordinal de teoría de la prueba, el ordinal de Bachmann-Howard

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

Las teorías de conjuntos de Kripke-Platek o CZF son teorías de conjuntos débiles sin axiomas para el conjunto de potencias 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 conceden la existencia de ciertos espacios funcionales (exponenciación) en lugar de separarlos de relaciones más grandes.

Teorías con ordinales de teoría de prueba más grandes

Problema no resuelto en matemáticas :

¿Cuál es el ordinal de la teoría de la prueba 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 de Π ₁ ¹ tiene un ordinal de teoría de prueba bastante grande, que fue descrito por Takeuti en términos de "diagramas de ordinales", ^{[5] p. 13} y que está acotado por ψ ₀ (Ω _ω ) en la notación de Buchholz . También es el ordinal de , la teoría de las definiciones inductivas finitamente iteradas. Y también el ordinal de MLW, la teoría de tipos de Martin-Löf con W-Types indexados Setzer (2004). ${\displaystyle ID_{<\omega }}$
• ID _ω , la teoría de las definiciones inductivas iteradas ω . Su ordinal de teoría de la prueba es igual al ordinal de Takeuti-Feferman-Buchholz .
• T ₀ , el sistema constructivo de matemáticas explícitas de Feferman tiene un ordinal de teoría de prueba más grande, que también es el ordinal de teoría de prueba de KPi, 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 teórico de prueba 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 la teoría de la prueba 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 teoría de prueba muy grande θ, que fue descrito por Rathjen (1990).
• TTM, una extensión de la teoría de tipos de Martin-Löf por un universo Mahlo, tiene un ordinal teórico de prueba aún mayor ψ _{Ω 1} (Ω _{M + ω} ).
• ${\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 teoría de prueba igual a , donde se refiere al primero -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 teórico de prueba igual a donde hay un análogo cardinal del menos ordinal que es -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 de potencias de los números naturales tienen ordinales de teoría de prueba que son tan grandes que aún no se ha dado ninguna descripción combinatoria explícita. Esto incluye aritmética completa de segundo orden ( ) y teorías de conjuntos con conjuntos de potencias que incluyen ZF y ZFC. La fuerza del ZF intuicionista (IZF) es igual a la del 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 ordinal como se definen en sus respectivas citas.
• Ψ representa la Psi de Rathjen o 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 ). La contabilización se considera necesaria para que un ordinal se considere prueba teórica.
• ${\displaystyle \mathbb {S} }$es un término ordinal que denota un ordinal estable y el ordinal menos admisible arriba . ${\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 la aritmética de 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 aritmética de funciones 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 aritmética de funciones elementales .
  • ${\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 aritmética de funciones elemental aumentada por un axioma que garantiza 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 ve aumentado por un axioma que garantiza que cada elemento del enésimo nivel 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 la 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 por ν 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}})}}}$es un automorfismo en . ${\displaystyle {\widehat {\mathsf {ID}}}_{\nu }}$
  • ${\displaystyle {\mathsf {ID}}_{\nu }}$extiende PA por ν puntos mínimos fijos iterados 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 ν veces.
  • ${\displaystyle {\mathsf {Aut(U(ID))}}}$es un automorfismo en . ${\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 usa en aritmética de primer orden. ${\displaystyle \Pi _{0}^{1}}$

• Aritmética de segundo orden
  • ${\displaystyle {\mathsf {RCA}}_{0}^{*}}$es una forma de segundo orden que a veces se usa en matemáticas inversas . ${\displaystyle {\mathsf {EFA}}}$
  • ${\displaystyle {\mathsf {WKL}}_{0}^{*}}$es una forma de segundo orden que a veces se usa en matemáticas inversas. ${\displaystyle {\mathsf {EFA}}}$
  • ${\displaystyle {\mathsf {RCA}}_{0}}$es comprensión recursiva .
  • ${\displaystyle {\mathsf {WKL}}_{0}}$es el lema de Kőnig débil .
  • ${\displaystyle {\mathsf {ACA}}_{0}}$es la comprensión aritmética .
  • ${\displaystyle {\mathsf {ACA}}}$es más el esquema completo de inducción de segundo orden. ${\displaystyle {\mathsf {ACA}}_{0}}$
  • ${\displaystyle {\mathsf {ATR}}_{0}}$es recursividad transfinita aritmética .
  • ${\displaystyle {\mathsf {ATR}}}$es más el esquema completo de inducción de segundo orden. ${\displaystyle {\mathsf {ATR}}_{0}}$
  • ${\displaystyle {\mathsf {\Delta }}_{2}^{1}{\mathsf {-CA+BI+(M)}}}$es más la afirmación "cada 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 del 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 está formado por conjuntos inaccesibles.
  • ${\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 ve aumentado por 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 ve aumentado por la afirmación "existe al menos un ordinal de Mahlo recursivamente"?
  • ${\displaystyle {\mathsf {KP}}\omega +(M\prec _{\Sigma _{1}}V)}$es con un axioma que establece que 'existe un conjunto M transitivo y no vacío 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 debilita significativamente la teoría). ${\displaystyle \in }$

• Teoría de tipos
  • ${\displaystyle {\mathsf {CPRC}}}$es el cálculo de Herbelin-Patey de construcciones recursivas primitivas.
  • ${\displaystyle {\mathsf {ML}}_{\mathsf {n}}}$es la teoría de tipos sin tipos W y con universos. ${\displaystyle n}$
  • ${\displaystyle {\mathsf {ML}}_{<\omega }}$es la teoría de tipos sin tipos W y con un número finito de universos.
  • ${\displaystyle {\mathsf {MLU}}}$es la teoría de tipos con un operador del siguiente universo.
  • ${\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 tipos W.
  • ${\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 la teoría de tipos con tipos W indexados.
  • ${\displaystyle {\mathsf {ML}}_{1}{\mathsf {W}}}$es la teoría de tipos con tipos W y un universo.
  • ${\displaystyle {\mathsf {ML}}_{<\omega }{\mathsf {W}}}$es la teoría de tipos con tipos W 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 la teoría de tipos con un universo 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 constructiva
  • ${\displaystyle {\mathsf {CZF}}}$es la teoría constructiva de conjuntos 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}}}$es con un universo Mahlo. ${\displaystyle {\mathsf {CZF}}}$

• Matemáticas explícitas
  • ${\displaystyle {\mathsf {EM}}_{0}}$son matemáticas explícitas básicas más comprensión elemental
  • ${\displaystyle {\mathsf {EM}}_{0}{\mathsf {+JR}}}$es más 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 de la de Feferman . ${\displaystyle {\mathsf {T}}_{0}}$
  • ${\displaystyle {\mathsf {T}}_{0}}$es , donde está la generación inductiva. ${\displaystyle {\mathsf {EM}}_{0}{\mathsf {+J+IG}}}$ ${\displaystyle {\mathsf {IG}}}$
  • ${\displaystyle {\mathsf {T}}}$es , donde está el esquema de inducción de segundo orden completo. ${\displaystyle {\mathsf {EM}}_{0}{\mathsf {+J+IG+FZ}}_{2}}$ ${\displaystyle {\mathsf {FZ}}_{2}}$

Ver también

• Equiconsistencia
• Gran propiedad cardinal
• Ordinal de Feferman-Schütte
• Ordinal Bachmann-Howard
• Clase de complejidad
• La prueba de coherencia de Gentzen

Notas

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

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

3. ^ También se puede escribir comúnmente como en ψ 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 en ψ de Madore. ${\displaystyle \psi (\varepsilon _{\Omega _{\omega }+1})}$

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

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

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

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

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

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

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

13. ^ representa el primer cardenal indescriptible. Utiliza Ψ de Stegert en lugar de ψ 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 cardenal Mahlo. Utiliza (presumiblemente) la ψ 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 ámbito del análisis ordinal. Consultado el 29 de septiembre de 2021.
3. Krajicek, enero (1995). Aritmética acotada, lógica proposicional y teoría de la complejidad. Prensa de la Universidad de Cambridge. págs. 18-20. ISBN 9780521452052.define los conjuntos rudimentarios y las funciones rudimentarias, y los demuestra equivalentes a los predicados Δ ₀ de los naturales. Se puede encontrar un análisis ordinal del sistema en Rose, HE (1984). Subrecursión: funciones y jerarquías . Universidad de Michigan: Clarendon Press. ISBN 9780198531890.
4. M. Rathjen, Teoría de la prueba: de la aritmética a la teoría de conjuntos (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. Matemáticas. Soc., págs. 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 de modelos para el análisis ordinal" (1997).
8. M. Rathjen, W. Carnielli, "Hidras y subsistemas de 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". Revista de lógica simbólica vol. 49, núm. 3 (1984).
12. B. Afshari, M. Rathjen, "Análisis ordinal y el teorema de Ramsey infinito" (2012)
13. Marcone, Alberto; Montalbán, Antonio (2011). "Las funciones de Veblen para los teóricos de la computabilidad". La revista de lógica simbólica . 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 Manual de lógica matemática , Estudios de lógica y fundamentos de las matemáticas, vol. 90 (1977), ed. J. Barwise, pub. Holanda del Norte.
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 aritmética de segundo orden", Journal of Symbolic Logic vol. 51 (1986), págs. 360-373.
18. Fischer, Martín; Nicolai, Carlo; Pablo Dopico Fernández (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 [matemáticas.LO].
19. SG Simpson, "Investigación de Friedman sobre subsistemas de aritmética de segundo orden". En Investigación sobre los fundamentos de las matemáticas de Harvey Friedman , Estudios de lógica y los fundamentos de las matemáticas vol. 117 (1985), ed. L. Harrington, M. Morley, A. Šcedrov, SG Simpson, pub. Holanda del Norte.
20. J. Avigad, "Un análisis ordinal de la teoría de conjuntos admisibles utilizando recursividad en notaciones ordinales". Revista de lógica matemática vol. 2, núm. 1, págs. 91-112 (2002).
21. S. Feferman, "Teorías inductivas iteradas del punto fijo: aplicación de la conjetura de Hancock". En Patras Logic Symposion , Estudios de lógica y fundamentos de las matemáticas vol. 109 (1982).
22. S. Feferman, T. Strahm, "El desarrollo de la aritmética no finitista", Annals of Pure and Applied Logic vol. 104, núm. 1--3 (2000), págs.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, núm. (1983), págs. 63-70.
24. U. Buchholtz, G. Jäger, T. Strahm, "Teorías de la fuerza de la teoría de la prueba ψ ( Γ Ω + 1 ) {\ Displaystyle \ psi (\ Gamma _ {\ Omega +1})} ". En Conceptos de prueba en matemáticas, filosofía e informática (2016), ed. D. Probst, P. Schuster. DOI 10.1515/9781501502620-007.
25. T. Strahm, "Progresiones autónomas de punto fijo y recursividad transfinita de punto fijo" (2000). En Coloquio de Lógica '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), págs.493-508.
27. T. Strahm, "Progresiones autónomas de punto fijo y recursividad transfinita de punto fijo" (2000)
28. C. Rüede, "Elección dependiente transfinita y reflexión del modelo ω". Revista de lógica simbólica vol. 67, núm. 3 (2002).
29. C. Rüede, "El análisis teórico de la prueba de la elección dependiente transfinita Σ11". Anales de lógica pura y aplicada vol. 122 (2003).
30. T. Strahm, "Pruebas de buen orden para Mahlo metapredicativo". Revista de lógica simbólica vol. 67, núm. 1 (2002)
31. F. Ranzi, T. Strahm, "Un sistema de tipos flexible para el pequeño ordinal 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". Anales de lógica pura y aplicada, vol. 166 (2015), págs. 409-463. ${\displaystyle \Pi _{1}^{1}}$
33. Krombholz, Martín; Rathjen, Michael (2019). "Límites superiores del teorema menor del gráfico". arXiv : 1907.00412 [matemáticas.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 de análisis impredicativos (estudios sobre teoría de la prueba, monografías, volumen 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 tipográficas de Martin-Löf"
38. A. Setzer, "Un modelo para una teoría de tipos con el universo Mahlo" (1996).
39. M. Rathjen, "Teoría de la prueba de la reflexión". Anales de lógica pura y aplicada vol. 68, edición. 2 (1994), págs. 181-224.
40. Stegert, Jan-Carl, "Teoría de la prueba ordinal de la teoría de conjuntos de Kripke-Platek aumentada por principios de reflexión fuertes" (2010).
41. Arai, Toshiyasu (1 de abril de 2023). "Conferencias sobre análisis ordinal". arXiv : 2304.00246 [matemáticas.LO].
42. Arai, Toshiyasu (7 de abril de 2023). "Prueba de fundamento para la reflexión". arXiv : 2304.03851 [matemáticas.LO]. ${\displaystyle \Pi _{1}^{1}}$
43. Arai, Toshiyasu (12 de febrero de 2024). "Un análisis ordinal de -Colección". arXiv : 2311.12459 [matemáticas.LO]. ${\displaystyle \Pi _{N}}$
44. Valentín Blot. "Una interpretación computacional directa de la aritmética de segundo orden mediante recursividad 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), Teoría de la prueba , Apuntes de conferencias de matemáticas, vol. 1407, Berlín: Springer-Verlag, doi :10.1007/978-3-540-46825-7, ISBN 3-540-51842-8, señor  1026933
• Pohlers, Wolfram (1998), "Teoría de conjuntos y teoría de números de segundo orden", Manual de teoría de la prueba , Estudios de lógica y fundamentos de las matemáticas, vol. 137, Ámsterdam: Elsevier Science BV, págs. 210–335, doi :10.1016/S0049-237X(98)80019-0, ISBN 0-444-89840-9, señor  1640328
• Rathjen, Michael (1990), "Notaciones ordinales basadas en un cardinal débilmente Mahlo"., Arch. Matemáticas. Lógica , 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. Matemáticas. Soc., págs. 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), Subrecursión. Funciones y jerarquías , guías lógicas de Oxford, 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, SEÑOR  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 ed.), Ámsterdam: North-Holland Publishing Co., ISBN 0-444-87943-9, señor  0882549
• Rathjen, Michael (1994), "Teoría de la prueba de la reflexión", Annals of Pure and Applied Logic , 68 (2): 181–224, doi :10.1016/0168-0072(94)90074-4
• Stegert, Jan-Carl (2010), Teoría de prueba ordinal de la teoría de conjuntos de Kripke-Platek aumentada por principios de reflexión fuertes