Análise ordinal - Ordinal analysis

Na teoria da prova , a análise ordinal atribui ordinais (geralmente grandes ordinais contáveis ) a teorias matemáticas como uma medida de sua força. Se as teorias têm o mesmo ordinal da teoria da prova, elas são freqüentemente equiconsistentes , e se uma teoria tem um ordinal da teoria da prova maior do que outra, muitas vezes pode provar a consistência da segunda teoria.

História

O campo da análise ordinal foi formado quando Gerhard Gentzen em 1934 usou a eliminação de corte para provar, em termos modernos, que o ordinal da teoria da prova da aritmética de Peano é ε ₀ . Veja a prova de consistência de Gentzen .

Definição

A análise ordinal diz respeito a teorias verdadeiras e eficazes (recursivas) que podem interpretar uma parte suficiente da aritmética para fazer afirmações sobre notações ordinais.

O ordinal da teoria da prova de tal teoria é o menor ordinal (necessariamente recursivo , consulte a próxima seção) que a teoria não pode provar ser bem fundada - o supremo de todos os ordinais para os quais existe uma notação no sentido de Kleene tal que prova que é um notação ordinal . Equivalentemente, é o supremo de todos os ordinais de tal forma que existe uma relação recursiva em (o conjunto de números naturais) que o ordena bem com o ordinal e tal que prova a indução transfinita de declarações aritméticas para . ${\ displaystyle T}$${\ displaystyle \ alpha}$${\ displaystyle o}$${\ displaystyle T}$${\ displaystyle o}$${\ displaystyle \ alpha}$ ${\ displaystyle R}$${\ displaystyle \ omega}$${\ displaystyle \ alpha}$${\ displaystyle T}$${\ displaystyle R}$

Notações ordinais

Algumas teorias, como subsistemas de aritmética de segunda ordem, não têm conceituação ou maneira de argumentar sobre ordinais transfinitos. Por exemplo, para formalizar o que significa para um subsistema de Z ₂ "provar -se bem ordenado", em vez disso, construímos uma notação ordinal com tipo de pedido . agora pode trabalhar com vários princípios de indução transfinita , que substituem o raciocínio sobre ordinais da teoria dos conjuntos. ${\ displaystyle T}$${\ displaystyle \ alpha}$ ${\ displaystyle (A, {\ tilde {<}})}$${\ displaystyle \ alpha}$${\ displaystyle T}$${\ displaystyle (A, {\ tilde {<}})}$

No entanto, existem alguns sistemas de notação patológicos que são inesperadamente difíceis de trabalhar. Por exemplo, Rathjen fornece um sistema de notação recursivo primitivo que é bem fundamentado se PA for consistente, apesar de ter tipo de pedido - incluir tal notação na análise ordinal de PA resultaria na falsa igualdade . ${\ displaystyle (\ mathbb {N}, <_ {T})}$${\ displaystyle \ omega}$${\ displaystyle {\ mathsf {PTO (PA)}} = \ omega}$

Limite superior

A existência de um ordinal recursivo que a teoria falha em provar que é bem ordenado decorre do teorema delimitador, pois o conjunto de números naturais que uma teoria efetiva prova ser notações ordinais é um conjunto (ver teoria hiperaritmética ). Assim, o ordinal da teoria da prova de uma teoria será sempre um ordinal recursivo (contável) , ou seja, menor que o ordinal de Church-Kleene . ${\ displaystyle {\ Sigma ^ {1}} _ {1}}$${\ displaystyle \ Sigma _ {1} ^ {0}}$ ${\ displaystyle \ omega _ {1} ^ {\ mathrm {CK}}}$

Exemplos

Teorias com ordinal teórico da prova ω

• Q, aritmética de Robinson (embora a definição do ordinal da teoria da prova para tais teorias fracas tenha que ser ajustada).
• PA ^- , a teoria de primeira ordem da parte não negativa de um anel ordenado discretamente.

Teorias com ordinal teórico-de-prova ω ²

• RFA, aritmética de função rudimentar .
• IΔ ₀ , aritmética com indução em predicados Δ ₀ sem qualquer axioma afirmando que a exponenciação é total.

Teorias com ordinal teórico-de-prova ω ³

• EFA, aritmética de função elementar .
• IΔ ₀ + exp, aritmética com indução em Δ ₀ -predicados aumentados por um axioma que afirma que a exponenciação é total.
• RCA^*
  ₀, uma forma de segunda ordem de EFA às vezes usada na matemática reversa .
• WKL^*
  ₀, uma forma de segunda ordem de EFA às vezes usada na matemática reversa .

A grande conjectura de Friedman sugere que grande parte da matemática "comum" pode ser provada em sistemas fracos tendo isso como seu ordinal da teoria da prova.

Teorias com ordinal teórico-de-prova ω ⁿ (para n = 2, 3, ... ω)

• IΔ ₀ ou EFA aumentado por um axioma garantindo que cada elemento do n- ésimo nível da hierarquia de Grzegorczyk seja total.${\ displaystyle {\ mathcal {E}} ^ {n}}$

Teorias com ordinal teórico da prova ω ^ω

• RCA ₀ , compreensão recursiva .
• WKL ₀ , lema de König fraco .
• PRA, aritmética recursiva primitiva .
• IΣ ₁ , aritmética com indução em Σ ₁ -predicados.

Teorias com ordinal teórico-de-prova ε ₀

• PA, aritmética de Peano ( mostrada por Gentzen usando eliminação de corte ).
• ACA ₀ , compreensão aritmética .

Teorias com ordinal teórico da prova o ordinal Feferman-Schütte Γ ₀

• ATR ₀ , recursão transfinita aritmética .
• Teoria de tipo de Martin-Löf com muitos universos de nível finito arbitrariamente.

Esse ordinal às vezes é considerado o limite superior das teorias "predicativas".

Teorias com ordinal da teoria da prova o ordinal de Bachmann-Howard

• ID ₁ , a primeira teoria de definições indutivas .
• KP, teoria dos conjuntos de Kripke-Platek com o axioma do infinito .
• CZF, teoria dos conjuntos Zermelo – Fraenkel construtiva de Aczel .
• EON, uma variante fraca do sistema matemático explícito de Feferman T ₀ .

As teorias de conjuntos de Kripke-Platek ou CZF são teorias de conjuntos fracas sem axiomas para o conjunto de poderes completo dado como conjunto de todos os subconjuntos. Em vez disso, eles tendem a ter axiomas de separação restrita e formação de novos conjuntos, ou garantem a existência de certos espaços de função (exponenciação) em vez de esculpi-los a partir de relações maiores.

Teorias com ordinais teóricos de prova maiores

• ${\ displaystyle \ Pi _ {1} ^ {1} {\ mbox {-}} {\ mathsf {CA}} _ {0}}$, Π ₁ ^uma compreensão tem uma bastante grande prova-teórico ordinal, que foi descrito por Takeuti em termos de diagramas de "ordinais", e que é delimitada por ψ ₀ (ohms _co ) em notação de Buchholz . É também o ordinal de , a teoria das definições indutivas finitamente iteradas. E também o ordinal de MLW, a teoria de tipo de Martin-Löf com Setzer W-Types indexado (2004) .${\ displaystyle ID _ {<\ omega}}$
• ID _ω , a teoria das definições indutivas iteradas por ω . Seu ordinal da teoria da prova é igual ao ordinal de Takeuti-Feferman-Buchholz .
• T ₀ , o sistema construtivo de matemática explícita de Feferman tem um ordinal teórico-de-prova maior, que também é o ordinal teórico-de-prova da teoria de conjuntos KPi, Kripke-Platek com admissíveis iterados e .${\ displaystyle \ Sigma _ {2} ^ {1} {\ mbox {-}} {\ mathsf {AC}} + {\ mathsf {BI}}}$
• KPi, uma extensão da teoria dos conjuntos de Kripke-Platek baseada em um cardinal inacessível , tem um ordinal teórico de prova muito grande , onde I é o menor inacessível, usando uma função desconhecida. Apelidado de "ordinal de Madore", em homenagem a David Madore. Esse ordinal também é o ordinal da teoria da prova de .${\ displaystyle \ psi (\ varepsilon _ {I + 1})}$${\ displaystyle \ Delta _ {2} ^ {1} {\ mbox {-}} {\ mathsf {CA}} + {\ mathsf {BI}}}$
• KPM, uma extensão da teoria dos conjuntos de Kripke-Platek baseada em um cardinal de Mahlo , tem um ordinal teórico de prova muito grande ϑ, que foi descrito por Rathjen (1990) , e apelidado de "Pequeno Ordinal de Rathjen".
• ${\ displaystyle {\ mathsf {KP}} + \ Pi _ {3} -Ref}$tem um ordinal teórico da prova igual a , onde se refere ao primeiro compacto fraco, usando a função Psi de Rathjen, apelidado de "Ordinal Rathjen Grande"${\ displaystyle \ Psi (\ varepsilon _ {K + 1})}$${\ displaystyle K}$
• ${\ displaystyle {\ mathsf {KP}} + \ Pi _ {\ omega} -Ref}$tem uma prova da teoria ordinal igual a , onde se refere ao primeiro -indescribable e = ( ; ; , , 0), utilizando a função Psi de Stegert, apelidado de "pequeno Stegert ordinal"${\ displaystyle \ Psi _ {X} ^ {\ varepsilon _ {\ Xi +1}}}$${\ displaystyle \ Xi}$${\ displaystyle \ Pi _ {0} ^ {2}}$${\ displaystyle X}$${\ displaystyle \ omega ^ {+}}$${\ displaystyle P_ {0}}$${\ displaystyle \ epsilon}$${\ displaystyle \ epsilon}$
• MLM, uma extensão da teoria de tipo de Martin-Löf por um universo de Mahlo, tem um ordinal teórico de prova ainda maior ψ _{Ω 1} (Ω _{M + ω} ).

A maioria das teorias capazes de descrever o conjunto de potências dos números naturais tem ordinais da teoria da prova que são tão grandes que nenhuma descrição combinatória explícita foi dada ainda. Isso inclui aritmética de segunda ordem e teorias de conjuntos com conjuntos de poderes incluindo ZF e ZFC (a partir de 2019). A força do ZF intuicionista (IZF) é igual à do ZF.

Tabela de análises ordinais

Tabela de ordinais da teoria da prova

Ordinal	Aritmética de primeira ordem	Aritmética de segunda ordem	Teoria dos conjuntos de Kripke-Platek	Teoria de tipo	Teoria dos conjuntos construtivos	Matemática explícita
${\ displaystyle \ omega}$	${\ displaystyle {\ mathsf {Q}}}$, ${\ displaystyle {\ mathsf {PA}} ^ {-}}$
${\ displaystyle \ omega ^ {2}}$	${\ displaystyle {\ mathsf {RFA}}}$, ${\ displaystyle {\ mathsf {I \ Delta}} _ {0}}$
${\ displaystyle \ omega ^ {3}}$	${\ displaystyle {\ mathsf {EFA}}}$, ${\ displaystyle {\ mathsf {I \ Delta}} _ {0} ^ {\ mathsf {+}}}$	${\ displaystyle {\ mathsf {RCA}} _ {0} ^ {*}}$, ${\ displaystyle {\ mathsf {WKL}} _ {0} ^ {*}}$
${\ displaystyle \ omega ^ {n}}$	${\ displaystyle {\ mathsf {EFA}} ^ {\ mathsf {n}}}$, ${\ displaystyle {\ mathsf {I \ Delta}} _ {0} ^ {\ mathsf {n +}}}$
${\ displaystyle \ omega ^ {\ omega}}$	${\ displaystyle {\ mathsf {PRA}}}$, ${\ displaystyle {\ mathsf {I \ Sigma}} _ {1}}$	${\ displaystyle {\ mathsf {RCA}} _ {0}}$, ${\ displaystyle {\ mathsf {WKL}} _ {0}}$		${\ displaystyle {\ mathsf {CPRC}}}$
${\ displaystyle \ varepsilon _ {0}}$	${\ displaystyle {\ mathsf {PA}}}$	${\ displaystyle {\ mathsf {ACA}} _ {0}}$, ,${\ displaystyle {\ mathsf {\ Delta}} _ {1} ^ {1} {\ mathsf {-CA}} _ {0}}$${\ displaystyle {\ mathsf {\ Sigma}} _ {1} ^ {1} {\ mathsf {-AC}} _ ​​{0}}$				${\ displaystyle {\ mathsf {EM}} _ {0}}$
${\ displaystyle \ varepsilon _ {\ varepsilon _ {0}}}$		${\ displaystyle {\ mathsf {ACA}}}$
${\ displaystyle \ varphi (\ omega, 0)}$	${\ displaystyle {\ mathsf {ID}} _ {1} \ #}$	${\ displaystyle {\ mathsf {\ Delta}} _ {1} ^ {1} {\ mathsf {-CR}}}$				${\ displaystyle {\ mathsf {EM}} _ {0} {\ mathsf {+ JR}}}$
${\ displaystyle \ varphi (\ varepsilon _ {0}, 0)}$	${\ displaystyle {\ widehat {\ mathsf {ID}}} _ {1}}$	${\ displaystyle {\ mathsf {\ Delta}} _ {1} ^ {1} {\ mathsf {-CA}}}$, ${\ displaystyle {\ mathsf {\ Sigma}} _ {1} ^ {1} {\ mathsf {-AC}}}$		${\ displaystyle {\ mathsf {ML}} _ {1}}$		${\ displaystyle {\ mathsf {EM}} _ {0} {\ mathsf {+ J}}}$
${\ displaystyle \ varphi ({\ mathsf {<}} \ Omega, 0)}$	${\ displaystyle {\ mathsf {Aut (ID \ #)}}}$
${\ displaystyle \ Gamma _ {0}}$	${\ displaystyle {\ widehat {\ mathsf {ID}}} _ {<\ omega}}$, ${\ displaystyle {\ mathsf {U (PA)}}}$	${\ displaystyle {\ mathsf {ATR}} _ {0}}$, ${\ displaystyle {\ mathsf {\ Delta}} _ {1} ^ {1} {\ mathsf {-CA + BR}}}$	${\ displaystyle {\ mathsf {KPi}} ^ {0}}$	${\ displaystyle {\ mathsf {ML}} _ {<\ omega}}$, ${\ displaystyle {\ mathsf {MLU}}}$
${\ displaystyle \ Gamma _ {\ omega}}$			${\ displaystyle {\ mathsf {KPI}} ^ {0} {\ mathsf {+ \ Sigma _ {1} -I}} _ {\ omega}}$
${\ displaystyle \ Gamma _ {\ varepsilon _ {0}}}$	${\ displaystyle {\ widehat {\ mathsf {ID}}} _ {\ omega}}$	${\ displaystyle {\ mathsf {ATR}}}$	${\ displaystyle {\ mathsf {KPI}} ^ {0} {\ mathsf {+ FI}} _ {\ omega}}$
${\ displaystyle \ varphi (1, \ omega, 0)}$	${\ displaystyle {\ widehat {\ mathsf {ID}}} _ {<\ omega ^ {\ omega}}}$	${\ displaystyle {\ mathsf {ATR}} _ {0} + ({\ mathsf {\ Sigma}} _ {1} ^ {1} {\ mathsf {-DC}})}$	${\ displaystyle {\ mathsf {KPi}} ^ {0} {\ mathsf {+ \ Sigma _ {1} -I}} _ {\ omega}}$
${\ displaystyle \ varphi (1, \ varepsilon _ {0}, 0)}$	${\ displaystyle {\ widehat {\ mathsf {ID}}} _ {<\ varepsilon _ {0}}}$	${\ displaystyle {\ mathsf {ATR}} + ({\ mathsf {\ Sigma}} _ {1} ^ {1} {\ mathsf {-DC}})}$	${\ displaystyle {\ mathsf {KPi}} ^ {0} {\ mathsf {+ FI}} _ {\ omega}}$
${\ displaystyle \ varphi (1, \ Gamma _ {0}, 0)}$	${\ displaystyle {\ widehat {\ mathsf {ID}}} _ {<\ Gamma _ {0}}}$			${\ displaystyle {\ mathsf {MLS}}}$
${\ displaystyle \ varphi (2,0,0)}$	${\ displaystyle {\ mathsf {Aut ({\ widehat {ID}})}}}$		${\ displaystyle {\ mathsf {KPh}} ^ {0}}$	${\ displaystyle {\ mathsf {Aut (ML)}}}$
${\ displaystyle \ varphi (\ omega, 0,0)}$			${\ displaystyle {\ mathsf {KPM}} ^ {0}}$
${\ displaystyle \ psi _ {0} (\ Omega _ {2})}$	${\ displaystyle {\ mathsf {ID}} _ {1}}$		${\ displaystyle {\ mathsf {KP}}}$, ${\ displaystyle {\ mathsf {KP \ omega}}}$	${\ displaystyle {\ mathsf {ML}} _ {1} {\ mathsf {V}}}$	${\ displaystyle {\ mathsf {CZF}}}$	${\ displaystyle {\ mathsf {EON}}}$
${\ displaystyle \ psi _ {0} (\ Gamma _ {\ Omega +1})}$	${\ displaystyle {\ mathsf {U (ID}} _ {1} {\ mathsf {)}}}$
${\ displaystyle \ psi _ {0} (\ varphi ({\ mathsf {<}} \ Omega, 0, \ Omega +1))}$	${\ displaystyle {\ mathsf {Aut (U (ID))}}}$
${\ displaystyle \ psi _ {0} (\ Omega _ {\ omega})}$	${\ displaystyle {\ mathsf {ID}} _ {<\ omega}}$	${\ displaystyle {\ mathsf {\ Pi}} _ {1} ^ {1} {\ mathsf {-CA}} _ {0}}$, ${\ displaystyle {\ mathsf {\ Delta}} _ {2} ^ {1} {\ mathsf {-CA}} _ {0}}$		${\ displaystyle {\ mathsf {MLW}}}$
${\ displaystyle \ psi _ {0} (\ Omega _ {\ omega} \ varepsilon _ {0})}$	${\ displaystyle {\ mathsf {W-ID}} _ {\ omega}}$	${\ displaystyle {\ mathsf {\ Pi}} _ {1} ^ {1} {\ mathsf {-CA}}}$	${\ displaystyle {\ mathsf {W-KPI}}}$
${\ displaystyle \ psi _ {0} (\ Omega _ {\ omega +1})}$	${\ displaystyle {\ mathsf {ID}} _ {\ omega}}$	${\ displaystyle {\ mathsf {\ Pi}} _ {1} ^ {1} {\ mathsf {-CA + BI}}}$	${\ displaystyle {\ mathsf {KPI}}}$
${\ displaystyle \ psi _ {\ Omega} (\ varepsilon _ {K + 1})}$			${\ displaystyle {\ mathsf {KP \ Pi}} _ {3}}$
${\ displaystyle \ psi _ {0} (\ Omega _ {\ omega ^ {\ omega}})}$	${\ displaystyle {\ mathsf {ID}} _ {<\ omega ^ {\ omega}}}$	${\ displaystyle {\ mathsf {\ Delta}} _ {2} ^ {1} {\ mathsf {-CR}}}$
${\ displaystyle \ psi _ {0} (\ Omega _ {\ varepsilon _ {0}})}$	${\ displaystyle {\ mathsf {ID}} _ {<\ varepsilon _ {0}}}$	${\ displaystyle {\ mathsf {\ Delta}} _ {2} ^ {1} {\ mathsf {-CA}}}$, ${\ displaystyle {\ mathsf {\ Sigma}} _ {2} ^ {1} {\ mathsf {-AC}}}$	${\ displaystyle {\ mathsf {W-KPi}}}$
${\ displaystyle \ psi _ {0} (\ Omega _ {\ Omega})}$	${\ displaystyle {\ mathsf {Aut (ID)}}}$
${\ displaystyle \ psi (\ varepsilon _ {I + 1})}$		${\ displaystyle {\ mathsf {\ Delta}} _ {2} ^ {1} {\ mathsf {-CA + BI}}}$, ${\ displaystyle {\ mathsf {\ Sigma}} _ {2} ^ {1} {\ mathsf {-AC + BI}}}$	${\ displaystyle {\ mathsf {KPi}}}$		${\ displaystyle {\ mathsf {CZF + REA}}}$	${\ displaystyle {\ mathsf {T}} _ {0}}$
${\ displaystyle \ psi (\ varepsilon _ {I + \ varepsilon _ {0} +1})}$			${\ displaystyle {\ mathsf {KPI}} {\ mathsf {+ FI}} _ {\ omega}}$		${\ displaystyle {\ mathsf {CZF + REA + Z}} _ {2} {\ mathsf {I}}}$	${\ displaystyle {\ mathsf {T}}}$
${\ displaystyle \ psi (\ Omega _ {I + \ omega})}$				${\ displaystyle {\ mathsf {ML}} _ {1} {\ mathsf {W}}}$
${\ displaystyle \ psi (\ Omega _ {L})}$			${\ displaystyle {\ mathsf {KPh}}}$	${\ displaystyle {\ mathsf {ML}} _ {<\ omega} {\ mathsf {W}}}$
${\ displaystyle \ psi (\ Omega _ {L ^ {*}})}$				${\ displaystyle {\ mathsf {Aut (MLW)}}}$
${\ displaystyle \ psi (\ varepsilon _ {M + 1})}$		${\ displaystyle {\ mathsf {\ Delta}} _ {2} ^ {1} {\ mathsf {-CA + BI + (M)}}}$	${\ displaystyle {\ mathsf {KPM}}}$		${\ displaystyle {\ mathsf {CZFM}}}$
${\ displaystyle \ Psi (\ varepsilon _ {K + 1})}$			${\ displaystyle {\ mathsf {KP + \ Pi}} _ {3} - {\ mathsf {Ref}}}$
${\ displaystyle \ Psi _ {(\ omega ^ {+}; P_ {0}, \ epsilon, \ epsilon, 0)} ^ {\ varepsilon _ {\ Xi +1}}}$			${\ displaystyle {\ mathsf {KP + \ Pi}} _ {\ omega} - {\ mathsf {Ref}}}$
${\ displaystyle \ Psi _ {(\ omega ^ {+}; P_ {0}, \ epsilon, \ epsilon, 0)} ^ {\ varepsilon _ {Y + 1}}}$			${\ displaystyle {\ mathsf {Estabilidade}}}$
${\ displaystyle \ psi (\ Omega _ {M + \ omega})}$			${\ displaystyle {\ mathsf {KPM}} ^ {+}}$	${\ displaystyle {\ mathsf {MLM}}}$

Chave

Esta é uma lista de símbolos usados ​​nesta tabela:

• ψ representa o psi de Buchholz, a menos que indicado de outra forma.
• Ψ representa o Psi de Rathjen ou de Stegert.
• φ representa a função de Veblen.
• ω representa o primeiro ordinal transfinito.
• ε _α representa os números épsilon .
• Γ _α representa os números gama (Γ ₀ é o ordinal Feferman-Schütte )
• Ω _α representa os incontáveis ​​ordinais (Ω ₁ , abreviado Ω, é ω ₁ ).

Esta é uma lista das abreviações usadas nesta tabela:

• Aritmética de primeira ordem
  • ${\ displaystyle {\ mathsf {Q}}}$é aritmética de Robinson
  • ${\ displaystyle {\ mathsf {PA}} ^ {-}}$ é a teoria de primeira ordem da parte não negativa de um anel ordenado discretamente.
  • ${\ displaystyle {\ mathsf {RFA}}}$é a aritmética de função rudimentar .
  • ${\ displaystyle {\ mathsf {I \ Delta}} _ {0}}$é aritmética com indução em predicados Δ ₀ sem qualquer axioma afirmando que a exponenciação é total.
  • ${\ displaystyle {\ mathsf {EFA}}}$é aritmética de função elementar .
  • ${\ displaystyle {\ mathsf {I \ Delta}} _ {0} ^ {\ mathsf {+}}}$é aritmética com indução em predicados Δ ₀ aumentados por um axioma que afirma que a exponenciação é total.
  • ${\ displaystyle {\ mathsf {EFA}} ^ {\ mathsf {n}}}$é a função aritmética elementar aumentada por um axioma garantindo que cada elemento do n- ésimo nível da hierarquia de Grzegorczyk seja total.${\ displaystyle {\ mathcal {E}} ^ {n}}$
  • ${\ displaystyle {\ mathsf {I \ Delta}} _ {0} ^ {\ mathsf {n +}}}$é aumentado por um axioma garantindo que cada elemento do n- ésimo nível da hierarquia de Grzegorczyk seja total.${\ displaystyle {\ mathsf {I \ Delta}} _ {0} ^ {\ mathsf {+}}}$${\ displaystyle {\ mathcal {E}} ^ {n}}$
  • ${\ displaystyle {\ mathsf {PRA}}}$é aritmética recursiva primitiva .
  • ${\ displaystyle {\ mathsf {I \ Sigma}} _ {1}}$é aritmética com indução em predicados Σ ₁ .
  • ${\ displaystyle {\ mathsf {PA}}}$é a aritmética de Peano .
  • ${\ displaystyle {\ mathsf {ID}} _ {\ nu} \ #}$é, mas com indução apenas para fórmulas positivas.${\ displaystyle {\ widehat {\ mathsf {ID}}} _ {\ nu}}$
  • ${\ displaystyle {\ widehat {\ mathsf {ID}}} _ {\ nu}}$ estende PA por ν pontos fixos iterados de operadores monótonos.
  • ${\ displaystyle {\ mathsf {U (PA)}}}$ não é exatamente um sistema aritmético de primeira ordem, mas captura o que se pode obter pelo raciocínio predicativo baseado nos números naturais.
  • ${\ displaystyle {\ mathsf {Aut ({\ widehat {ID}})}}}$está um automorfismo ligado .${\ displaystyle {\ widehat {\ mathsf {ID}}} _ {\ nu}}$
  • ${\ displaystyle {\ mathsf {ID}} _ {\ nu}}$estende PA por ν pontos fixos mínimos iterados de operadores monótonos.
  • ${\ displaystyle {\ mathsf {U (ID}} _ {\ nu} {\ mathsf {)}}}$ não é exatamente um sistema aritmético de primeira ordem, mas captura o que se pode obter pelo raciocínio predicativo baseado em definições indutivas generalizadas iteradas ν vezes.
  • ${\ displaystyle {\ mathsf {Aut (U (ID))}}}$está um automorfismo ligado .${\ displaystyle {\ mathsf {U (ID}} _ {\ nu} {\ mathsf {)}}}$
  • ${\ displaystyle {\ mathsf {W-ID}} _ {\ nu}}$é uma versão enfraquecida do baseado em W-types.${\ displaystyle {\ mathsf {ID}} _ {\ nu}}$
• Aritmética de segunda ordem
  • ${\ displaystyle {\ mathsf {RCA}} _ {0} ^ {*}}$é uma forma de segunda ordem às vezes usada na matemática reversa .${\ displaystyle {\ mathsf {EFA}}}$
  • ${\ displaystyle {\ mathsf {WKL}} _ {0} ^ {*}}$é uma forma de segunda ordem às vezes usada na matemática reversa.${\ displaystyle {\ mathsf {EFA}}}$
  • ${\ displaystyle {\ mathsf {RCA}} _ {0}}$é a compreensão recursiva .
  • ${\ displaystyle {\ mathsf {WKL}} _ {0}}$é o lema de König fraco .
  • ${\ displaystyle {\ mathsf {ACA}} _ {0}}$é a compreensão aritmética .
  • ${\ displaystyle {\ mathsf {ACA}}}$é mais o esquema de indução de segunda ordem completo.${\ displaystyle {\ mathsf {ACA}} _ {0}}$
  • ${\ displaystyle {\ mathsf {ATR}} _ {0}}$é a recursão transfinita aritmética .
  • ${\ displaystyle {\ mathsf {ATR}}}$é mais o esquema de indução de segunda ordem completo.${\ displaystyle {\ mathsf {ATR}} _ {0}}$
  • ${\ displaystyle {\ mathsf {\ Delta}} _ {2} ^ {1} {\ mathsf {-CA + BI + (M)}}}$é mais a asserção "toda frase -verdadeira com parâmetros vale em um -modelo de ".${\ displaystyle {\ mathsf {\ Delta}} _ {2} ^ {1} {\ mathsf {-CA + BI}}}$${\ displaystyle {\ mathsf {\ Pi}} _ {3} ^ {1}}$${\ displaystyle \ beta}$${\ displaystyle {\ mathsf {\ Delta}} _ {2} ^ {1} {\ mathsf {-CA}}}$
• Teoria dos conjuntos de Kripke-Platek
  • ${\ displaystyle {\ mathsf {KP}}}$é a teoria dos conjuntos de Kripke-Platek com o axioma do infinito.
  • ${\ displaystyle {\ mathsf {KP \ omega}}}$é a teoria dos conjuntos de Kripke-Platek, cujo universo é um conjunto admissível contendo .${\ displaystyle \ omega}$
  • ${\ displaystyle {\ mathsf {W-KPI}}}$é uma versão enfraquecida do baseado em W-types.${\ displaystyle {\ mathsf {KPI}}}$
  • ${\ displaystyle {\ mathsf {KPI}}}$ afirma que o universo é um limite de conjuntos admissíveis.
  • ${\ displaystyle {\ mathsf {W-KPi}}}$é uma versão enfraquecida do baseado em W-types.${\ displaystyle {\ mathsf {KPi}}}$
  • ${\ displaystyle {\ mathsf {KPi}}}$ afirma que o universo é conjuntos inacessíveis.
  • ${\ displaystyle {\ mathsf {KPh}}}$ afirma que o universo é hiperinacessível: um conjunto inacessível e um limite de conjuntos inacessíveis.
  • ${\ displaystyle {\ mathsf {KPM}}}$ afirma que o universo é um conjunto de Mahlo.
  • ${\ displaystyle {\ mathsf {KP + \ Pi}} _ {\ mathsf {n}} - {\ mathsf {Ref}}}$é aumentado por um certo esquema de reflexão de primeira ordem.${\ displaystyle {\ mathsf {KP}}}$
  • ${\ displaystyle {\ mathsf {Estabilidade}}}$é KPi aumentado pelo axioma .${\ displaystyle \ forall \ alpha \ exists \ kappa \ geq \ alpha (L _ {\ kappa} \ preceq _ {1} L _ {\ kappa + \ alpha})}$
  • ${\ displaystyle {\ mathsf {KPM}} ^ {+}}$é o KPI aumentado pela afirmação "existe pelo menos um ordinal de Mahlo recursivamente".

Um zero sobrescrito indica que a indução foi removida (tornando a teoria significativamente mais fraca). ${\ displaystyle \ in}$

• Teoria de tipo
  • ${\ displaystyle {\ mathsf {CPRC}}}$ é o cálculo de Herbelin-Patey de construções recursivas primitivas.
  • ${\ displaystyle {\ mathsf {ML}} _ {\ mathsf {n}}}$é a teoria dos tipos sem tipos W e com universos.${\ displaystyle n}$
  • ${\ displaystyle {\ mathsf {ML}} _ {<\ omega}}$ é a teoria dos tipos sem tipos W e com muitos universos finitos.
  • ${\ displaystyle {\ mathsf {MLU}}}$ é a teoria dos tipos com um próximo operador do universo.
  • ${\ displaystyle {\ mathsf {MLS}}}$ é a teoria dos tipos sem tipos W e com um superuniverso.
  • ${\ displaystyle {\ mathsf {Aut (ML)}}}$ é um automorfismo na teoria dos tipos sem tipos-W.
  • ${\ displaystyle {\ mathsf {ML}} _ {1} {\ mathsf {V}}}$ é a teoria dos tipos com um universo e o tipo de conjuntos iterativos de Aczel.
  • ${\ displaystyle {\ mathsf {MLW}}}$ é a teoria dos tipos com tipos W indexados.
  • ${\ displaystyle {\ mathsf {ML}} _ {1} {\ mathsf {W}}}$ é a teoria dos tipos com tipos W e um universo.
  • ${\ displaystyle {\ mathsf {ML}} _ {<\ omega} {\ mathsf {W}}}$ é a teoria dos tipos com tipos W e um número finito de universos.
  • ${\ displaystyle {\ mathsf {Aut (MLW)}}}$ é um automorfismo na teoria dos tipos com W-types.
  • ${\ displaystyle {\ mathsf {MLM}}}$ é a teoria dos tipos com um universo Mahlo.
• Teoria dos conjuntos construtivos
  • ${\ displaystyle {\ mathsf {CZF}}}$ é a teoria dos conjuntos construtivos de Aczel.
  • ${\ displaystyle {\ mathsf {CZF + REA}}}$é mais o axioma de extensão regular.${\ displaystyle {\ mathsf {CZF}}}$
  • ${\ displaystyle {\ mathsf {CZF + REA + FZ}} _ {2}}$é mais o esquema de indução de segunda ordem.${\ displaystyle {\ mathsf {CZF + REA}}}$
  • ${\ displaystyle {\ mathsf {CZFM}}}$está com um universo Mahlo.${\ displaystyle {\ mathsf {CZF}}}$
• Matemática explícita
  • ${\ displaystyle {\ mathsf {EM}} _ {0}}$ é matemática básica explícita mais compreensão elementar
  • ${\ displaystyle {\ mathsf {EM}} _ {0} {\ mathsf {+ JR}}}$é mais uma regra de junção${\ displaystyle {\ mathsf {EM}} _ {0}}$
  • ${\ displaystyle {\ mathsf {EM}} _ {0} {\ mathsf {+ J}}}$é axioma plus join${\ displaystyle {\ mathsf {EM}} _ {0}}$
  • ${\ displaystyle {\ mathsf {EON}}}$é uma variante fraca dos Feferman 's .${\ displaystyle {\ mathsf {T}} _ {0}}$
  • ${\ displaystyle {\ mathsf {T}} _ {0}}$é , onde está a geração indutiva.${\ displaystyle {\ mathsf {EM}} _ {0} {\ mathsf {+ J + IG}}}$${\ displaystyle {\ mathsf {IG}}}$
  • ${\ displaystyle {\ mathsf {T}}}$é , onde está o esquema de indução de segunda ordem completo.${\ displaystyle {\ mathsf {EM}} _ {0} {\ mathsf {+ J + IG + FZ}} _ {2}}$${\ displaystyle {\ mathsf {FZ}} _ {2}}$

Veja também

• Equiconsistência
• Grande propriedade cardinal
• Feferman – Schütte ordinal
• Ordinal de Bachmann-Howard
• Classe de complexidade

Notas

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

2. ^ A função de Veblen com menos pontos fixos com iteração infinita e contável.${\ displaystyle \ varphi}$

3. ^ Também pode ser comumente escrito como no ψ de Madore.${\ displaystyle \ psi (\ varepsilon _ {\ Omega +1})}$

4. ^ Usa ψ de Madore em vez de ψ de Buchholz.

5. ^ Também pode ser comumente escrito como no ψ de Madore.${\ displaystyle \ psi (\ varepsilon _ {\ Omega _ {\ omega} +1})}$

6. ^ representa o primeiro ordinal recursivamente fracamente compacto. Usa ψ de Arai em vez de ψ de Buchholz.${\ displaystyle K}$

7. ^ Também o ordinal de prova-thetoretic de , como a quantidade de enfraquecimento dado pelos W-types não é suficiente.${\ displaystyle {\ mathsf {Aut (W-ID)}}}$

8. ^ representa o primeiro cardeal inacessível. Usa ψ de Jäger em vez de ψ de Buchholz.${\ displaystyle I}$

9. ^ representa o limite dos cardeais inacessíveis. Usa (presumivelmente) o ψ de Jäger.${\ displaystyle L}$${\ displaystyle \ omega}$

10. ^ representa o limite dos cardeais inacessíveis. Usa (presumivelmente) o ψ de Jäger.${\ displaystyle L ^ {*}}$${\ displaystyle \ Omega}$

11. ^ representa o primeiro cardeal Mahlo. Usa ψ de Rathjen em vez de ψ de Buchholz.${\ displaystyle M}$

12. ^ representa o primeiro cardeal fracamente compacto. Usa Ψ de Rathjen em vez de ψ de Buchholz.${\ displaystyle K}$

13. ^ representa o primeiro cardeal indescritível. Usa Ψ de Stegert em vez de ψ de Buchholz.${\ displaystyle \ Xi}$${\ displaystyle \ Pi _ {0} ^ {2}}$

14. ^ é o menor tal que ' é -indescritível') e ' é -indescritível '). Usa Ψ de Stegert em vez de ψ de Buchholz.${\ displaystyle Y}$${\ displaystyle \ alpha}$${\ displaystyle \ forall \ theta <Y \ existe \ kappa <Y (}$${\ displaystyle \ kappa}$${\ displaystyle \ theta}$${\ displaystyle \ forall \ theta <Y \ forall \ kappa <Y (}$${\ displaystyle \ kappa}$${\ displaystyle \ theta}$${\ displaystyle \ rightarrow \ theta <\ kappa}$

15. ^ representa o primeiro cardeal Mahlo. Usa (presumivelmente) o ψ de Rathjen.${\ displaystyle M}$

Citações

Referências

• Buchholz, W .; Feferman, S .; Pohlers, W .; Sieg, W. (1981), Iterated inductive settings and sub-systems of analysis , Lecture Notes in Math., 897 , Berlin: Springer-Verlag, doi : 10.1007 / BFb0091894 , ISBN 978-3-540-11170-2
• Pohlers, Wolfram (1989), Teoria da prova , Lecture Notes in Mathematics, 1407 , Berlin: Springer-Verlag, doi : 10.1007 / 978-3-540-46825-7 , ISBN 3-540-51842-8, MR  1026933
• Pohlers, Wolfram (1998), "Set Theory and Second Order Number Theory", Handbook of Proof Theory , Studies in Logic and the Foundations of Mathematics, 137 , Amsterdam: Elsevier Science BV, pp. 210-335, doi : 10.1016 / S0049 -237X (98) 80019-0 , ISBN 0-444-89840-9, MR  1640328
• Rathjen, Michael (1990), "Notações ordinais baseadas em um cardeal Mahlo fraco." , Arch. Matemática. Logic , 29 (4): 249-263, doi : 10.1007 / BF01651328 , MR  1062729
• Rathjen, Michael (2006), "A arte da análise ordinal" (PDF) , Congresso Internacional de Matemáticos , II , Zurique: Eur. Matemática. Soc., Pp. 45-69, MR  2275588 , arquivado do original em 22-12-2009CS1 maint: bot: status do URL original desconhecido ( link )
• Rose, HE (1984), Subrecursion. Funções e hierarquias , guias lógicos de Oxford, 9 , Oxford, Nova York: Clarendon Press, Oxford University Press
• Schütte, Kurt (1977), Teoria da prova , Grundlehren der Mathematischen Wissenschaften, 225 , Berlin-New York: Springer-Verlag, pp. Xii + 299, ISBN 3-540-07911-4, MR  0505313
• Setzer, Anton (2004), "Teoria de prova da teoria de tipo de Martin-Löf. Uma visão geral" , Mathématiques et Sciences Humaines. Matemática e Ciências Sociais (165): 59-99
• Takeuti, Gaisi (1987), Teoria da prova , Estudos em lógica e os fundamentos da matemática, 81 (segunda edição), Amsterdã: North-Holland Publishing Co., ISBN 0-444-87943-9, MR  0882549