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 de la teoría de la prueba, a menudo son equiconguentes , y si una teoría tiene un ordinal de la teoría de la prueba más grande que otra, a menudo puede probar la consistencia de la segunda teoría.
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 demostración de la aritmética de Peano es ε 0 . Vea la prueba de consistencia 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 demostración de tal teoríaes el ordinal más pequeño (necesariamente recursivo , ver la siguiente sección) que la teoría no puede probar está bien fundado: el supremo de todos los ordinalespara el cual existe una notaciónen el sentido de Kleene de tal manera que prueba 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 ordinal y tal que prueba la inducción transfinita de enunciados aritméticos para.
Límite superior
La existencia de un ordinal recursivo que la teoría no puede probar está bien ordenado se sigue de la teorema de la delimitación, como el conjunto de números naturales que una teoría efectiva demuestra que son notaciones ordinales es un conjunto (ver Teoría hiperaritmética ). Así, el ordinal de la teoría de la prueba de una teoría siempre será un ordinal recursivo (contable) , es decir, menor que el ordinal de Church-Kleene. .
Ejemplos de
Teorías con ordinal de teoría de la prueba ω
- Q, aritmética de Robinson (aunque la definición del ordinal de la teoría de la demostración para teorías tan débiles debe modificarse).
- 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 la prueba ω 2
- RFA, aritmética de funciones rudimentarias . [1]
- IΔ 0 , aritmética con inducción en Δ 0 -predica sin ningún axioma que afirme que la exponenciación es total.
Teorías con ordinal de teoría de la prueba ω 3
- EFA, aritmética de funciones elementales .
- IΔ 0 + exp, aritmética con inducción en Δ 0 -predicados aumentados por un axioma que afirma que la exponenciación es total.
- RCA*
0, una forma de EFA de segundo orden que a veces se utiliza en matemáticas inversas . - WKL*
0, una forma de EFA de segundo orden que a veces se utiliza en matemáticas inversas .
La gran conjetura de Friedman sugiere que gran parte de las matemáticas "ordinarias" se pueden probar en sistemas débiles que tienen esto como su ordinal teórico de la demostración.
Teorías con ordinal de teoría de la prueba ω n (para n = 2, 3, ... ω)
- IΔ 0 o EFA aumentado por un axioma que asegura que cada elemento del n -ésimo nivelde la jerarquía de Grzegorczyk es total.
Teorías con ordinal de teoría de la prueba ω ω
- RCA 0 , comprensión recursiva .
- WKL 0 , lema de König débil .
- PRA, aritmética recursiva primitiva .
- IΣ 1 , aritmética con inducción en Σ 1 -predica.
Teorías con ordinal teórico-demostrativo ε 0
- PA, aritmética de Peano ( mostrado por Gentzen usando eliminación de cortes ).
- ACA 0 , comprensión aritmética .
Teorías con ordinal de teoría de la prueba el ordinal de Feferman-Schütte Γ 0
- ATR 0 , recursividad aritmética transfinita .
- Teoría de tipos de Martin-Löf con muchos universos de niveles finitos arbitrariamente.
Este ordinal a veces se considera el límite superior de las teorías "predicativas".
Teorías con ordinal de teoría de la prueba ordinal de Bachmann-Howard
- ID 1 , la teoría de las definiciones inductivas.
- KP, teoría de conjuntos de Kripke-Platek con el axioma del infinito .
- CZF, teoría de conjuntos constructiva de Zermelo-Fraenkel de Aczel .
- EON, una variante débil del sistema matemático explícito de Feferman T 0 .
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 otorgan la existencia de ciertos espacios funcionales (exponenciación) en lugar de extraerlos de relaciones más grandes.
Teorías con ordinales de teoría de la prueba más grandes
- , Π 1 1 comprensión tiene un ordinal teórico de la prueba bastante grande, que fue descrito por Takeuti en términos de "diagramas ordinales", y que está acotado por ψ 0 (Ω ω ) en la notación de Buchholz . También es el ordinal de, la teoría de las definiciones inductivas de iteración finita. Y también el ordinal de MLW, teoría de tipos de Martin-Löf con Setzer de tipos W indexados (2004) .
- T 0 , el sistema constructivo de matemáticas explícitas de Feferman tiene un ordinal teórico de la prueba más grande, que también es el ordinal teórico de la prueba de la teoría de conjuntos KPi, Kripke-Platek con admisibles iterados y.
- KPM, una extensión de la teoría de conjuntos de Kripke-Platek basada en un cardinal de Mahlo , tiene un ordinal de teoría de la demostración muy grande ϑ, que fue descrito por Rathjen (1990) .
- MLM, 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 + ω ).
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 la prueba que son tan grandes que aún no se ha dado una descripción combinatoria explícita. Esto incluye aritmética de segundo orden y teorías de conjuntos con conjuntos de potencia que incluyen ZF y ZFC (a partir de 2019[actualizar]). La fuerza del intuicionista ZF (IZF) es igual a la de ZF.
Ver también
- Equiconsistencia
- Gran propiedad cardinal
- Feferman – Schütte ordinal
- Ordinal de Bachmann-Howard
- Clase de complejidad
Referencias
- Buchholz, W .; Feferman, S .; Pohlers, W .; Sieg, W. (1981), Definiciones inductivas iteradas y subsistemas de análisis , Lecture Notes in Math., 897 , Berlín: Springer-Verlag, doi : 10.1007 / BFb0091894 , ISBN 978-3-540-11170-2
- Pohlers, Wolfram (1989), Teoría de la prueba , Lecture Notes in Mathematics, 1407 , Berlín: Springer-Verlag, doi : 10.1007 / 978-3-540-46825-7 , ISBN 3-540-51842-8, MR 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, 137 , Amsterdam: Elsevier Science BV, págs. 210–335, doi : 10.1016 / S0049 -237X (98) 80019-0 , ISBN 0-444-89840-9, MR 1640328
- Rathjen, Michael (1990), "Notaciones ordinales basadas en un cardenal débilmente Mahlo". , Arch. Matemáticas. Lógica , 29 (4): 249–263, doi : 10.1007 / BF01651328 , MR 1062729
- Rathjen, Michael (2006), "El arte del análisis ordinal" (PDF) , Congreso Internacional de Matemáticos , II , Zürich: Eur. Matemáticas. Soc., Págs. 45–69, MR 2275588 , archivado desde el original el 22 de diciembre de 2009CS1 maint: bot: estado de URL original desconocido ( enlace )
- Rose, HE (1984), Subrecursión. Funciones y jerarquías , guías lógicas de Oxford, 9 , Oxford, Nueva York: Clarendon Press, Oxford University Press
- Schütte, Kurt (1977), Teoría de la prueba , Grundlehren der Mathematischen Wissenschaften, 225 , Berlín-Nueva York: Springer-Verlag, págs. Xii + 299, ISBN 3-540-07911-4, MR 0505313
- Setzer, Anton (2004), "Teoría de la prueba de la teoría de tipos de Martin-Löf. Una visió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, 81 (Segunda ed.), Ámsterdam: North-Holland Publishing Co., ISBN 0-444-87943-9, MR 0882549
- ^ Krajicek, Jan (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 las prueba equivalentes a las predicciones Δ 0 de las 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.