Ordinal analysis

In proof theory, ordinal analysis assigns ordinals (often large countable ordinals) to mathematical theories as a measure of their strength. If theories have the same proof-theoretic ordinal they are often equiconsistent, and if one theory has a larger proof-theoretic ordinal than another it can often prove the consistency of the second theory.

In addition to obtaining the proof-theoretic ordinal of a theory, in practice ordinal analysis usually also yields various other pieces of information about the theory being analyzed, for example characterizations of the classes of provably recursive, hyperarithmetical, or ${\displaystyle \Delta _{2}^{1}}$ functions of the theory.^[1]

History

The field of ordinal analysis was formed when Gerhard Gentzen in 1934 used cut elimination to prove, in modern terms, that the proof-theoretic ordinal of Peano arithmetic is ε₀. See Gentzen's consistency proof.

Definition

Ordinal analysis concerns true, effective (recursive) theories that can interpret a sufficient portion of arithmetic to make statements about ordinal notations.

The proof-theoretic ordinal of such a theory ${\displaystyle T}$  is the supremum of the order types of all ordinal notations (necessarily recursive, see next section) that the theory can prove are well founded—the supremum of all ordinals ${\displaystyle \alpha }$  for which there exists a notation ${\displaystyle o}$  in Kleene's sense such that ${\displaystyle T}$  proves that ${\displaystyle o}$  is an ordinal notation. Equivalently, it is the supremum of all ordinals ${\displaystyle \alpha }$  such that there exists a recursive relation ${\displaystyle R}$  on ${\displaystyle \omega }$  (the set of natural numbers) that well-orders it with ordinal ${\displaystyle \alpha }$  and such that ${\displaystyle T}$  proves transfinite induction of arithmetical statements for ${\displaystyle R}$ .

Ordinal notations

Some theories, such as subsystems of second-order arithmetic, have no conceptualization of or way to make arguments about transfinite ordinals. For example, to formalize what it means for a subsystem of Z₂ ${\displaystyle T}$  to "prove ${\displaystyle \alpha }$  well-ordered", we instead construct an ordinal notation ${\displaystyle (A,{\tilde {<}})}$  with order type ${\displaystyle \alpha }$ . ${\displaystyle T}$  can now work with various transfinite induction principles along ${\displaystyle (A,{\tilde {<}})}$ , which substitute for reasoning about set-theoretic ordinals.

However, some pathological notation systems exist that are unexpectedly difficult to work with. For example, Rathjen gives a primitive recursive notation system ${\displaystyle (\mathbb {N} ,<_{T})}$  that is well-founded iff PA is consistent,^{[2]p. 3} despite having order type ${\displaystyle \omega }$  - including such a notation in the ordinal analysis of PA would result in the false equality ${\displaystyle {\mathsf {PTO(PA)}}=\omega }$ .

Upper bound

For any theory that's both ${\displaystyle \Sigma _{1}^{1}}$ -axiomatizable and ${\displaystyle \Pi _{1}^{1}}$ -sound, the existence of a recursive ordering that the theory fails to prove is well-ordered follows from the ${\displaystyle \Sigma _{1}^{1}}$  bounding theorem, and said provably well-founded ordinal notations are in fact well-founded by ${\displaystyle \Pi _{1}^{1}}$ -soundness. Thus the proof-theoretic ordinal of a ${\displaystyle \Pi _{1}^{1}}$ -sound theory that has a ${\displaystyle \Sigma _{1}^{1}}$  axiomatization will always be a (countable) recursive ordinal, that is, less than the Church–Kleene ordinal ${\displaystyle \omega _{1}^{\mathrm {CK} }}$ . ^{[2]Theorem 2.21}

Examples

Theories with proof-theoretic ordinal ω

• Q, Robinson arithmetic (although the definition of the proof-theoretic ordinal for such weak theories has to be tweaked)^{[citation needed]}.
• PA^–, the first-order theory of the nonnegative part of a discretely ordered ring.

Theories with proof-theoretic ordinal ω²

• RFA, rudimentary function arithmetic.^[3]
• IΔ₀, arithmetic with induction on Δ₀-predicates without any axiom asserting that exponentiation is total.

Theories with proof-theoretic ordinal ω³

• EFA, elementary function arithmetic.
• IΔ₀ + exp, arithmetic with induction on Δ₀-predicates augmented by an axiom asserting that exponentiation is total.
• RCA^*
  ₀, a second order form of EFA sometimes used in reverse mathematics.
• WKL^*
  ₀, a second order form of EFA sometimes used in reverse mathematics.

Friedman's grand conjecture suggests that much "ordinary" mathematics can be proved in weak systems having this as their proof-theoretic ordinal.

Theories with proof-theoretic ordinal ωⁿ (for n = 2, 3, ... ω)

• IΔ₀ or EFA augmented by an axiom ensuring that each element of the n-th level ${\displaystyle {\mathcal {E}}^{n}}$  of the Grzegorczyk hierarchy is total.

Theories with proof-theoretic ordinal ω^ω

• RCA₀, recursive comprehension.
• WKL₀, weak Kőnig's lemma.
• PRA, primitive recursive arithmetic.
• IΣ₁, arithmetic with induction on Σ₁-predicates.

Theories with proof-theoretic ordinal ε₀

• PA, Peano arithmetic (shown by Gentzen using cut elimination).
• ACA₀, arithmetical comprehension.

Theories with proof-theoretic ordinal the Feferman–Schütte ordinal Γ₀

• ATR₀, arithmetical transfinite recursion.
• Martin-Löf type theory with arbitrarily many finite level universes.

This ordinal is sometimes considered to be the upper limit for "predicative" theories.

Theories with proof-theoretic ordinal the Bachmann–Howard ordinal

• ID₁, the first theory of inductive definitions.
• KP, Kripke–Platek set theory with the axiom of infinity.
• CZF, Aczel's constructive Zermelo–Fraenkel set theory.
• EON, a weak variant of the Feferman's explicit mathematics system T₀.

The Kripke-Platek or CZF set theories are weak set theories without axioms for the full powerset given as set of all subsets. Instead, they tend to either have axioms of restricted separation and formation of new sets, or they grant existence of certain function spaces (exponentiation) instead of carving them out from bigger relations.

Theories with larger proof-theoretic ordinals

Unsolved problem in mathematics:

What is the proof-theoretic ordinal of full second-order arithmetic?^[4]

(more unsolved problems in mathematics)

• ${\displaystyle \Pi _{1}^{1}{\mbox{-}}{\mathsf {CA}}_{0}}$ , Π₁¹ comprehension has a rather large proof-theoretic ordinal, which was described by Takeuti in terms of "ordinal diagrams",^{[5]p. 13} and which is bounded by ψ₀(Ω_ω) in Buchholz's notation. It is also the ordinal of ${\displaystyle ID_{<\omega }}$ , the theory of finitely iterated inductive definitions. And also the ordinal of MLW, Martin-Löf type theory with indexed W-Types Setzer (2004).
• ID_ω, the theory of ω-iterated inductive definitions. Its proof-theoretic ordinal is equal to the Takeuti-Feferman-Buchholz ordinal.
• T₀, Feferman's constructive system of explicit mathematics has a larger proof-theoretic ordinal, which is also the proof-theoretic ordinal of the KPi, Kripke–Platek set theory with iterated admissibles and ${\displaystyle \Sigma _{2}^{1}{\mbox{-}}{\mathsf {AC}}+{\mathsf {BI}}}$ .
• KPi, an extension of Kripke–Platek set theory based on a recursively inaccessible ordinal, has a very large proof-theoretic ordinal ${\displaystyle \psi (\varepsilon _{I+1})}$  described in a 1983 paper of Jäger and Pohlers, where I is the smallest inaccessible.^[6] This ordinal is also the proof-theoretic ordinal of ${\displaystyle \Delta _{2}^{1}{\mbox{-}}{\mathsf {CA}}+{\mathsf {BI}}}$ .
• KPM, an extension of Kripke–Platek set theory based on a recursively Mahlo ordinal, has a very large proof-theoretic ordinal θ, which was described by Rathjen (1990).
• MLM, an extension of Martin-Löf type theory by one Mahlo-universe, has an even larger proof-theoretic ordinal ψ_Ω1(Ω_{M + ω}).
• ${\displaystyle {\mathsf {KP}}+\Pi _{3}-Ref}$  has a proof-theoretic ordinal equal to ${\displaystyle \Psi (\varepsilon _{K+1})}$ , where ${\displaystyle K}$  refers to the first weakly compact, due to (Rathjen 1993)
• ${\displaystyle {\mathsf {KP}}+\Pi _{\omega }-Ref}$  has a proof-theoretic ordinal equal to ${\displaystyle \Psi _{X}^{\varepsilon _{\Xi +1}}}$ , where ${\displaystyle \Xi }$  refers to the first ${\displaystyle \Pi _{0}^{2}}$ -indescribable and ${\displaystyle \mathbb {X} =(\omega ^{+};P_{0};\epsilon ,\epsilon ,0)}$ , due to (Stegert 2010).
• ${\displaystyle {\mathsf {Stability}}}$  has a proof-theoretic ordinal equal to ${\displaystyle \Psi _{\mathbb {X} }^{\varepsilon _{\Upsilon +1}}}$  where ${\displaystyle \Upsilon }$  is a cardinal analogue of the least ordinal ${\displaystyle \alpha }$  which is ${\displaystyle \alpha +\beta }$ -stable for all ${\displaystyle \beta <\alpha }$  and ${\displaystyle \mathbb {X} =(\omega ^{+};P_{0};\epsilon ,\epsilon ,0)}$ , due to (Stegert 2010).

Most theories capable of describing the power set of the natural numbers have proof-theoretic ordinals that are so large that no explicit combinatorial description has yet been given. This includes ${\displaystyle \Pi _{2}^{1}-CA_{0}}$ , full second-order arithmetic (${\displaystyle \Pi _{\infty }^{1}-CA_{0}}$ ) and set theories with powersets including ZF and ZFC. The strength of intuitionistic ZF (IZF) equals that of ZF.

Table of ordinal analyses

Table of proof-theoretic ordinals

Ordinal	First-order arithmetic	Second-order arithmetic	Kripke-Platek set theory	Type theory	Constructive set theory	Explicit mathematics
${\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}}$ ^[1]	${\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 \omega ^{\omega ^{\omega ^{\omega }}}}$		${\displaystyle {\mathsf {RCA}}_{0}+(\Pi _{2}^{0})^{-}{\mathsf {-IND}}}$ ^[7]^: 40
${\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 {\text{R-}}{\widehat {\mathbf {E} {\boldsymbol {\Omega }}}}}$ ^[8]^p. 8	${\displaystyle \mathrm {KPu} ^{r}}$ ^[9]^p. 869			${\displaystyle {\mathsf {EM}}_{0}}$
${\displaystyle \varepsilon _{\omega }}$		${\displaystyle {\mathsf {ACA}}_{0}+{\mathsf {iRT}}}$ ,^[10] ${\displaystyle {\mathsf {RCA}}_{0}+\forall Y\forall n\exists X({\textrm {TJ}}(n,X,Y))}$ ^[11]^: 8
${\displaystyle \varepsilon _{\varepsilon _{0}}}$		${\displaystyle {\mathsf {ACA}}}$ ^[12]^p. 959
${\displaystyle \zeta _{0}}$		${\displaystyle {\mathsf {ACA}}_{0}+\forall X\exists Y({\textrm {TJ}}(\omega ,X,Y))}$ ,^[13]^[11] ${\displaystyle {\mathsf {p}}_{1}({\mathsf {ACA}}_{0})}$ ,^[14]^: 7 ${\displaystyle {\mathsf {RFN}}_{0}}$ ^[13]^p. 17, ${\displaystyle {\mathsf {ACA}}_{0}+({\mathsf {BR}})}$ ^[13]^p. 5
${\displaystyle \varphi (2,\varepsilon _{0})}$		${\displaystyle {\mathsf {RFN}}}$ , ${\displaystyle {\mathsf {ACA}}+\forall X\exists Y({\textrm {TJ}}(\omega ,X,Y))}$ ^[13]^p. 52
${\displaystyle \varphi (\omega ,0)}$	${\displaystyle {\mathsf {ID}}_{1}\#}$	${\displaystyle {\mathsf {\Delta }}_{1}^{1}{\mathsf {-CR}}}$ , ${\displaystyle \Sigma _{1}^{1}{\mathsf {-DC}}_{0}}$ ^[15]				${\displaystyle {\mathsf {EM}}_{0}{\mathsf {+JR}}}$
${\displaystyle \varphi (\varepsilon _{0},0)}$	${\displaystyle {\widehat {\mathsf {ID}}}_{1}}$ , ${\displaystyle {\mathsf {KFL}}}$ ^[16]^p. 17, ${\displaystyle {\mathsf {KF}}}$ ^[16]^p. 17	${\displaystyle {\mathsf {\Delta }}_{1}^{1}{\mathsf {-CA}}}$ ^[17]^p. 140, ${\displaystyle {\mathsf {\Sigma }}_{1}^{1}{\mathsf {-AC}}}$ ^[17]^p. 140, ${\displaystyle {\mathsf {\Sigma }}_{1}^{1}{\mathsf {-DC}}}$ ^[17]^p. 140, ${\displaystyle {\text{W-}}{\widehat {\mathbf {E} {\boldsymbol {\Omega }}}}}$ ^[8]^p. 8	${\displaystyle \mathrm {KPu} ^{r}+(\mathrm {IND} _{N})}$ ^[9]^p. 870	${\displaystyle {\mathsf {ML}}_{1}}$		${\displaystyle {\mathsf {EM}}_{0}{\mathsf {+J}}}$
${\displaystyle \varphi (\varepsilon _{\varepsilon _{0}},0)}$		${\displaystyle {\widehat {\mathbf {E} {\boldsymbol {\Omega }}}}}$ ^[8]^p. 27, ${\displaystyle {\widehat {\mathbf {EID} }}_{\boldsymbol {1}}}$ ^[8]^p. 27
${\displaystyle \varphi (\varphi (\omega ,0),0)}$	${\displaystyle \mathrm {PRS} \omega }$ ^[18]^p.9
${\displaystyle \varphi ({\mathsf {<}}\Omega ,0)}$ ^[2]	${\displaystyle {\mathsf {Aut(ID\#)}}}$
${\displaystyle \Gamma _{0}}$	${\displaystyle {\widehat {\mathsf {ID}}}_{<\omega }}$ ,^[19] ${\displaystyle {\mathsf {U(PA)}}}$ , ${\displaystyle \mathbf {KFL} ^{*}}$ ^[16]^p. 22, ${\displaystyle \mathbf {KF} ^{*}}$ ^[16]^p. 22, ${\displaystyle {\mathcal {U}}(\mathrm {NFA} )}$ ^[20]	${\displaystyle {\mathsf {ATR}}_{0}}$ , ${\displaystyle {\mathsf {\Delta }}_{1}^{1}{\mathsf {-CA+BR}}}$ , ${\displaystyle \Delta _{1}^{1}\mathrm {-CA} _{0}+\mathrm {(SUB)} }$ ,^[21] ${\displaystyle \mathrm {FP} _{0}}$ ^[22]^p. 26	${\displaystyle {\mathsf {KPi}}^{0}}$ ^[9]^p. 878, ${\displaystyle {\mathsf {KPu}}^{0}+(\mathrm {BR} )}$ ^[9]^p. 878	${\displaystyle {\mathsf {ML}}_{<\omega }}$ , ${\displaystyle {\mathsf {MLU}}}$
${\displaystyle \Gamma _{\omega ^{\omega }}}$			${\displaystyle {\mathsf {KPI}}^{0}+({\mathsf {\Sigma _{1}-I}}_{\omega })}$ ^[23]^p.13
${\displaystyle \Gamma _{\varepsilon _{0}}}$	${\displaystyle {\widehat {\mathsf {ID}}}_{\omega }}$	${\displaystyle {\mathsf {ATR}}}$ ^[24]	${\displaystyle {\mathsf {KPI}}^{0}{\mathsf {+F-I}}_{\omega }}$
${\displaystyle \varphi (1,\omega ,0)}$	${\displaystyle {\widehat {\mathsf {ID}}}_{<\omega ^{\omega }}}$	${\displaystyle {\mathsf {ATR}}_{0}+({\mathsf {\Sigma }}_{1}^{1}{\mathsf {-DC}})}$ ^[14]^: 7	${\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}})}$ ^[14]^: 7	${\displaystyle {\mathsf {KPi}}^{0}{\mathsf {+F-I}}_{\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 {FTR}}_{0}}$ ^[25]	${\displaystyle Ax_{\Sigma _{1}^{1}{\mathsf {-AC}}}{\mathsf {TR}}_{0}}$ ^[26]^p.1167, ${\displaystyle Ax_{{\mathsf {ATR}}+\Sigma _{1}^{1}{\mathsf {-DC}}}{\mathsf {RFN}}_{0}}$ ^[26]^p.1167	${\displaystyle {\mathsf {KPh}}^{0}}$	${\displaystyle {\mathsf {Aut(ML)}}}$
${\displaystyle \varphi (2,0,\varepsilon _{0})}$	${\displaystyle {\mathsf {FTR}}}$ ^[25]	${\displaystyle Ax_{\Sigma _{1}^{1}{\mathsf {-AC}}}{\mathsf {TR}}}$ ^[26]^p.1167, ${\displaystyle Ax_{{\mathsf {ATR}}+\Sigma _{1}^{1}{\mathsf {-DC}}}{\mathsf {RFN}}}$ ^[26]^p.1167
${\displaystyle \varphi (2,\varepsilon _{0},0)}$			${\displaystyle {\mathsf {KPh}}_{0}+({\mathsf {F-I}}_{\omega })}$ ^[25]^: 11
${\displaystyle \varphi (\omega ,0,0)}$		${\displaystyle (\Pi _{2}^{1}{\mathsf {-RFN}})_{0}^{\Sigma _{1}^{1}{\mathsf {-DC}}}}$ ^[27]^p.233, ${\displaystyle \Sigma _{1}^{1}{\mathsf {-TDC}}_{0}}$ ^[27]^p.233	${\displaystyle {\mathsf {KPm}}^{0}}$ ^[28]^p.276	${\displaystyle {\mathsf {EMA}}}$ ^[28]^p.276
${\displaystyle \varphi (\varepsilon _{0},0,0)}$		${\displaystyle (\Pi _{2}^{1}{\mathsf {-RFN}})^{\Sigma _{1}^{1}{\mathsf {-DC}}}}$ ^[27]^p.233, ${\displaystyle \Sigma _{1}^{1}{\mathsf {-TDC}}}$ ^[14]	${\displaystyle {\mathsf {KPm}}^{0}+({\mathcal {L}}^{*}{\mathsf {-I}}_{\mathsf {N}})}$ ^[28]^p.277	${\displaystyle {\mathsf {EMA}}+(\mathbb {L} {\mathsf {-I}}_{\mathsf {N}})}$ ^[28]^p.277
${\displaystyle \varphi (1,0,0,0)}$		${\displaystyle {\mathsf {p}}_{1}(\Sigma _{1}^{1}{\mathsf {-TDC}}_{0})}$ ^[14]^: 7
${\displaystyle \psi _{\Omega _{1}}(\Omega ^{\Omega ^{\omega }})}$		${\displaystyle {\mathsf {RCA}}_{0}^{*}+\Pi _{1}^{1}{\mathsf {-CA}}^{-}}$ ,^[29] ${\displaystyle {\mathsf {p}}_{3}({\mathsf {ACA}}_{0})}$ ^[14]^: 7
${\displaystyle \vartheta (\Omega ^{\Omega })}$		${\displaystyle {\mathsf {p}}_{1}({\mathsf {p}}_{3}({\mathsf {ACA}}_{0}))}$ ^[14]^: 7
${\displaystyle \psi _{0}(\varepsilon _{\Omega +1})}$ ^[3]	${\displaystyle {\mathsf {ID}}_{1}}$	${\displaystyle {\text{W-}}{\widetilde {\mathbf {E} {\boldsymbol {\Omega }}}}}$ ^[8]^p. 8	${\displaystyle {\mathsf {KP}}}$ ,^[2] ${\displaystyle {\mathsf {KP\omega }}}$ , ${\displaystyle \mathrm {KPu} }$ ^[9]^p. 869	${\displaystyle {\mathsf {ML}}_{1}{\mathsf {V}}}$	${\displaystyle {\mathsf {CZF}}}$	${\displaystyle {\mathsf {EON}}}$
${\displaystyle \psi (\varepsilon _{\Omega +\varepsilon _{0}})}$		${\displaystyle {\widetilde {\mathbf {E} {\boldsymbol {\Omega }}}}}$ ^[8]^p. 31, ${\displaystyle {\widetilde {\mathbf {EID} }}_{\boldsymbol {1}}}$ ^[8]^p. 31, ${\displaystyle \mathbf {ACA} +(\Pi _{1}^{1}{\text{-CA}})^{-}}$ ^[8]^p. 31
${\displaystyle \psi (\varepsilon _{\Omega +\Omega })}$		${\displaystyle ({\mathsf {ID}}_{1}^{2})_{0}+{\mathsf {BR}}}$ ^[30]
${\displaystyle \psi (\varepsilon _{\varepsilon _{\Omega +1}})}$		${\displaystyle \mathbf {E} {\boldsymbol {\Omega }}}$ ^[8]^p. 33, ${\displaystyle \mathbf {EID} _{\boldsymbol {1}}}$ ^[8]^p. 33, ${\displaystyle \mathbf {ACA} +(\Pi _{1}^{1}{\text{-CA}})^{-}+(\mathrm {BI} _{\mathrm {PR} })^{-}}$ ^[8]^p. 33
${\displaystyle \psi _{0}(\Gamma _{\Omega +1})}$ ^[4]	${\displaystyle {\mathsf {U(ID}}_{1}{\mathsf {)}}}$ , ${\displaystyle {\widehat {\mathsf {ID}}}_{<\omega }^{\bullet }}$ ^[22]^p. 26, ${\displaystyle \Sigma _{1}^{1}{\mathsf {-DC}}_{0}^{\bullet }+({\mathsf {SUB}}^{\bullet })}$ ^[22]^p. 26, ${\displaystyle {\mathsf {ATR}}_{0}^{\bullet }}$ ^[22]^p. 26, ${\displaystyle \Sigma _{1}^{1}{\mathsf {-AC}}_{0}^{\bullet }+({\mathsf {SUB}}^{\bullet })}$ ^[22]^p. 26, ${\displaystyle {\mathcal {U}}({\mathsf {ID}}_{1})}$ ^[22]^p. 26	${\displaystyle {\mathsf {FP}}_{0}^{\bullet }}$ ^[22]^p. 26, ${\displaystyle {\mathsf {ATR}}_{0}^{\bullet }}$ ^[22]^p. 26
${\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 }\omega ^{\omega })}$	${\displaystyle \Pi _{1}^{1}{\mathsf {-CA}}_{0}+\Pi _{2}^{1}{\mathsf {-IND}}}$ ^[31]
${\displaystyle \psi _{0}(\Omega _{\omega }\varepsilon _{0})}$	${\displaystyle {\mathsf {W-ID}}_{\omega }}$	${\displaystyle {\mathsf {\Pi }}_{1}^{1}{\mathsf {-CA}}}$ ^[32]^p. 14	${\displaystyle {\mathsf {W-KPI}}}$
${\displaystyle \psi _{0}(\Omega _{\omega }\Omega )}$		${\displaystyle \Pi _{1}^{1}{\mathsf {-CA+BR}}}$ ^[33]
${\displaystyle \psi _{0}(\Omega _{\omega }^{\omega })}$		${\displaystyle \Pi _{1}^{1}{\mathsf {-CA}}_{0}+\Pi _{2}^{1}{\mathsf {-BI}}}$ ^[31]
${\displaystyle \psi _{0}(\Omega _{\omega }^{\omega ^{\omega }})}$		${\displaystyle \Pi _{1}^{1}{\mathsf {-CA}}_{0}+\Pi _{2}^{1}{\mathsf {-BI}}+\Pi _{3}^{1}{\mathsf {-IND}}}$ ^[31]
${\displaystyle \psi _{0}(\varepsilon _{\Omega _{\omega }+1})}$ ^[5]	${\displaystyle {\mathsf {ID}}_{\omega }}$	${\displaystyle {\mathsf {\Pi }}_{1}^{1}{\mathsf {-CA+BI}}}$	${\displaystyle {\mathsf {KPI}}}$
${\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)}}}$ ^[6]
${\displaystyle \psi _{\Omega _{1}}(\varepsilon _{\Omega _{\Omega }+1})}$	${\displaystyle {\mathsf {ID}}_{\prec ^{*}}}$ , ${\displaystyle {\mathsf {BID}}^{2*}}$ , ${\displaystyle {\mathsf {ID}}^{2*}+{\mathsf {BI}}}$ ^[34]		${\displaystyle {\mathsf {KPl}}^{*}}$ , ${\displaystyle {\mathsf {KPl}}_{\Omega }^{r}}$
${\displaystyle \psi _{0}(\Phi _{1}(0))}$		${\displaystyle \Pi _{1}^{1}{\mathsf {-TR}}_{0}}$ , ${\displaystyle \Pi _{1}^{1}{\mathsf {-TR}}_{0}+\Delta _{2}^{1}{\mathsf {-CA}}_{0}}$ , ${\displaystyle \Delta _{2}^{1}{\mathsf {-CA+BI(impl-}}\Sigma _{2}^{1})}$ ,${\displaystyle \Delta _{2}^{1}{\mathsf {-CA+BR(impl-}}\Sigma _{2}^{1})}$ , ${\displaystyle \mathbf {AUT-ID} _{0}^{pos}}$ , ${\displaystyle \mathbf {AUT-ID} _{0}^{mon}}$ ^[34]^: 72	${\displaystyle {\mathsf {KPi}}^{w}+{\mathsf {FOUNDR}}({\mathsf {impl-}})\Sigma )}$ ,^[34]^: 72 ${\displaystyle {\mathsf {KPi}}^{w}+{\mathsf {FOUND}}({\mathsf {impl-}})\Sigma )}$ ^[34]^: 72	${\displaystyle \mathbf {AUT-KPl} ^{r}}$ , ${\displaystyle \mathbf {AUT-KPl} ^{r}+\mathbf {KPi} ^{r}}$ ^[34]^: 72
${\displaystyle \psi _{0}(\Phi _{1}(0)\varepsilon _{0})}$		${\displaystyle \Pi _{1}^{1}{\mathsf {-TR}}}$ , ${\displaystyle \mathbf {AUT-ID} ^{pos}}$ , ${\displaystyle \mathbf {AUT-ID} ^{mon}}$ ^[34]^: 72	${\displaystyle \mathbf {AUT-KPl} ^{w}}$ ^[34]^: 72
${\displaystyle \psi _{0}(\varepsilon _{\Phi _{1}(0)+1})}$		${\displaystyle (\Pi _{1}^{1}{\mathsf {-TR}}+({\mathsf {BI}})}$ , ${\displaystyle \mathbf {AUT-ID} _{2}^{pos}}$ , ${\displaystyle \mathbf {AUT-ID} _{2}^{mon}}$ ^[34]^: 72	${\displaystyle \mathbf {AUT-KPl} }$ ^[34]^: 72
${\displaystyle \psi _{0}(\Phi _{1}(\varepsilon _{0}))}$		${\displaystyle \Pi _{1}^{1}{\mathsf {-TR}}+\Delta _{2}^{1}{\mathsf {-CA}}}$ , ${\displaystyle \Pi _{1}^{1}{\mathsf {-TR}}+\Sigma _{2}^{1}{\mathsf {-AC}}}$ , ${\displaystyle \mathbf {AUT-KPl} ^{w}+\mathbf {KPi} ^{w}}$ ^[34]^: 72
${\displaystyle \psi _{0}(\Phi _{\omega }(0))}$		${\displaystyle \Delta _{2}^{1}{\mathsf {-TR}}_{0}}$ , ${\displaystyle \Sigma _{2}^{1}{\mathsf {-TRDC}}_{0}}$ , ${\displaystyle \Delta _{2}^{1}{\mathsf {-CA}}_{0}+(\Sigma _{2}^{1}{\mathsf {-BI}})}$ ^[34]^: 72	${\displaystyle \mathbf {KPi} ^{r}+(\Sigma {\mathsf {-FOUND}})}$ , ${\displaystyle \mathbf {KPi} ^{r}+(\Sigma {\mathsf {-REC}})}$ ^[34]^: 72
${\displaystyle \psi _{0}(\Phi _{\varepsilon _{0}}(0))}$		${\displaystyle \Delta _{2}^{1}{\mathsf {-TR}}}$ , ${\displaystyle \Sigma _{2}^{1}{\mathsf {-TRDC}}}$ , ${\displaystyle \Delta _{2}^{1}{\mathsf {-CA}}+(\Sigma _{2}^{1}{\mathsf {-BI}})}$ ^[34]^: 72	${\displaystyle \mathbf {KPi} ^{w}+(\Sigma {\mathsf {-FOUND}})}$ , ${\displaystyle \mathbf {KPi} ^{w}+(\Sigma {\mathsf {-REC}})}$ ^[34]^: 72
${\displaystyle \psi (\varepsilon _{I+1})}$ ^[7]		${\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 (\Omega _{I+\omega })}$				${\displaystyle {\mathsf {ML}}_{1}{\mathsf {W}}}$ ^[35]^: 38
${\displaystyle \psi (\Omega _{L})}$ ^[8]			${\displaystyle {\mathsf {KPh}}}$	${\displaystyle {\mathsf {ML}}_{<\omega }{\mathsf {W}}}$
${\displaystyle \psi (\Omega _{L^{*}})}$ ^[9]				${\displaystyle {\mathsf {Aut(MLW)}}}$
${\displaystyle \psi _{\Omega }(\chi _{\varepsilon _{M+1}}(0))}$ ^[10]		${\displaystyle {\mathsf {\Delta }}_{2}^{1}{\mathsf {-CA+BI+(M)}}}$	${\displaystyle {\mathsf {KPM}}}$		${\displaystyle {\mathsf {CZFM}}}$
${\displaystyle \psi (\Omega _{M+\omega })}$ ^[11]			${\displaystyle {\mathsf {KPM}}^{+}}$	${\displaystyle {\mathsf {MLM}}}$
${\displaystyle \Psi _{\Omega }^{0}(\varepsilon _{K+1})}$ ^[12]			${\displaystyle {\mathsf {KP+\Pi }}_{3}-{\mathsf {Ref}}}$ ^[36]
${\displaystyle \Psi _{(\omega ^{+};P_{0},\epsilon ,\epsilon ,0)}^{\varepsilon _{\Xi +1}}}$ ^[13]			${\displaystyle {\mathsf {KP+\Pi }}_{\omega }-{\mathsf {Ref}}}$
${\displaystyle \Psi _{(\omega ^{+};P_{0},\epsilon ,\epsilon ,0)}^{\varepsilon _{\Upsilon +1}}}$ ^[14]			${\displaystyle {\mathsf {Stability}}}$
${\displaystyle \psi _{\omega _{1}^{CK}}(\varepsilon _{\mathbb {I} +1})}$ ^[37]		${\displaystyle \Sigma _{3}^{1}{\mathsf {-DC+BI}}}$	${\displaystyle {\mathsf {KP+\Pi }}_{1}{\mathsf {-collection}}}$ January 01, 1970 Latest articles January 07, 2023 Warrow, South Australia January 07, 2023 Warrap, South Sudan January 10, 2023 Warrego River January 06, 2023 Warren, Pembrokeshire January 14, 2023 Warren Maher January 07, 2023 Warren A. Bechtel January 15, 2023 Warren Beatty January 10, 2023 Warren Cowan January 06, 2023 Warren Delabere Barnes January 07, 2023 Warren East Most Read January 07, 2023 Hàm Nghi December 27, 2022 Háromszék County January 06, 2023 HârnWorld January 09, 2023 Hålogaland Court of Appeal December 26, 2022 Héctor Canavery ordinal, analysis, this, article, includes, list, general, references, lacks, sufficient, corresponding, inline, citations, please, help, improve, this, article, introducing, more, precise, citations, september, 2021, learn, when, remove, this, message, proof,. This article includes a list of general references but it lacks sufficient corresponding inline citations Please help to improve this article by introducing more precise citations September 2021 Learn how and when to remove this message In proof theory ordinal analysis assigns ordinals often large countable ordinals to mathematical theories as a measure of their strength If theories have the same proof theoretic ordinal they are often equiconsistent and if one theory has a larger proof theoretic ordinal than another it can often prove the consistency of the second theory In addition to obtaining the proof theoretic ordinal of a theory in practice ordinal analysis usually also yields various other pieces of information about the theory being analyzed for example characterizations of the classes of provably recursive hyperarithmetical or D 2 1 displaystyle Delta 2 1 functions of the theory 1 Contents 1 History 2 Definition 2 1 Ordinal notations 3 Upper bound 4 Examples 4 1 Theories with proof theoretic ordinal w 4 2 Theories with proof theoretic ordinal w2 4 3 Theories with proof theoretic ordinal w3 4 4 Theories with proof theoretic ordinal wn for n 2 3 w 4 5 Theories with proof theoretic ordinal ww 4 6 Theories with proof theoretic ordinal e0 4 7 Theories with proof theoretic ordinal the Feferman Schutte ordinal G0 4 8 Theories with proof theoretic ordinal the Bachmann Howard ordinal 4 9 Theories with larger proof theoretic ordinals 5 Table of ordinal analyses 5 1 Key 6 See also 7 Notes 8 Citations 9 ReferencesHistory editThe field of ordinal analysis was formed when Gerhard Gentzen in 1934 used cut elimination to prove in modern terms that the proof theoretic ordinal of Peano arithmetic is e0 See Gentzen s consistency proof Definition editOrdinal analysis concerns true effective recursive theories that can interpret a sufficient portion of arithmetic to make statements about ordinal notations The proof theoretic ordinal of such a theory T displaystyle T nbsp is the supremum of the order types of all ordinal notations necessarily recursive see next section that the theory can prove are well founded the supremum of all ordinals a displaystyle alpha nbsp for which there exists a notation o displaystyle o nbsp in Kleene s sense such that T displaystyle T nbsp proves that o displaystyle o nbsp is an ordinal notation Equivalently it is the supremum of all ordinals a displaystyle alpha nbsp such that there exists a recursive relation R displaystyle R nbsp on w displaystyle omega nbsp the set of natural numbers that well orders it with ordinal a displaystyle alpha nbsp and such that T displaystyle T nbsp proves transfinite induction of arithmetical statements for R displaystyle R nbsp Ordinal notations edit Some theories such as subsystems of second order arithmetic have no conceptualization of or way to make arguments about transfinite ordinals For example to formalize what it means for a subsystem of Z2 T displaystyle T nbsp to prove a displaystyle alpha nbsp well ordered we instead construct an ordinal notation A lt displaystyle A tilde lt nbsp with order type a displaystyle alpha nbsp T displaystyle T nbsp can now work with various transfinite induction principles along A lt displaystyle A tilde lt nbsp which substitute for reasoning about set theoretic ordinals However some pathological notation systems exist that are unexpectedly difficult to work with For example Rathjen gives a primitive recursive notation system N lt T displaystyle mathbb N lt T nbsp that is well founded iff PA is consistent 2 p 3 despite having order type w displaystyle omega nbsp including such a notation in the ordinal analysis of PA would result in the false equality P T O P A w displaystyle mathsf PTO PA omega nbsp Upper bound editFor any theory that s both S 1 1 displaystyle Sigma 1 1 nbsp axiomatizable and P 1 1 displaystyle Pi 1 1 nbsp sound the existence of a recursive ordering that the theory fails to prove is well ordered follows from the S 1 1 displaystyle Sigma 1 1 nbsp bounding theorem and said provably well founded ordinal notations are in fact well founded by P 1 1 displaystyle Pi 1 1 nbsp soundness Thus the proof theoretic ordinal of a P 1 1 displaystyle Pi 1 1 nbsp sound theory that has a S 1 1 displaystyle Sigma 1 1 nbsp axiomatization will always be a countable recursive ordinal that is less than the Church Kleene ordinal w 1 C K displaystyle omega 1 mathrm CK nbsp 2 Theorem 2 21Examples editTheories with proof theoretic ordinal w edit Q Robinson arithmetic although the definition of the proof theoretic ordinal for such weak theories has to be tweaked citation needed PA the first order theory of the nonnegative part of a discretely ordered ring Theories with proof theoretic ordinal w2 edit RFA rudimentary function arithmetic 3 ID0 arithmetic with induction on D0 predicates without any axiom asserting that exponentiation is total Theories with proof theoretic ordinal w3 edit EFA elementary function arithmetic ID0 exp arithmetic with induction on D0 predicates augmented by an axiom asserting that exponentiation is total RCA 0 a second order form of EFA sometimes used in reverse mathematics WKL 0 a second order form of EFA sometimes used in reverse mathematics Friedman s grand conjecture suggests that much ordinary mathematics can be proved in weak systems having this as their proof theoretic ordinal Theories with proof theoretic ordinal wn for n 2 3 w edit ID0 or EFA augmented by an axiom ensuring that each element of the n th level E n displaystyle mathcal E n nbsp of the Grzegorczyk hierarchy is total Theories with proof theoretic ordinal ww edit RCA0 recursive comprehension WKL0 weak Konig s lemma PRA primitive recursive arithmetic IS1 arithmetic with induction on S1 predicates Theories with proof theoretic ordinal e0 edit PA Peano arithmetic shown by Gentzen using cut elimination ACA0 arithmetical comprehension Theories with proof theoretic ordinal the Feferman Schutte ordinal G0 edit ATR0 arithmetical transfinite recursion Martin Lof type theory with arbitrarily many finite level universes This ordinal is sometimes considered to be the upper limit for predicative theories Theories with proof theoretic ordinal the Bachmann Howard ordinal edit ID1 the first theory of inductive definitions KP Kripke Platek set theory with the axiom of infinity CZF Aczel s constructive Zermelo Fraenkel set theory EON a weak variant of the Feferman s explicit mathematics system T0 The Kripke Platek or CZF set theories are weak set theories without axioms for the full powerset given as set of all subsets Instead they tend to either have axioms of restricted separation and formation of new sets or they grant existence of certain function spaces exponentiation instead of carving them out from bigger relations Theories with larger proof theoretic ordinals edit Unsolved problem in mathematics What is the proof theoretic ordinal of full second order arithmetic 4 more unsolved problems in mathematics P 1 1 C A 0 displaystyle Pi 1 1 mbox mathsf CA 0 nbsp P11 comprehension has a rather large proof theoretic ordinal which was described by Takeuti in terms of ordinal diagrams 5 p 13 and which is bounded by ps0 Ww in Buchholz s notation It is also the ordinal of I D lt w displaystyle ID lt omega nbsp the theory of finitely iterated inductive definitions And also the ordinal of MLW Martin Lof type theory with indexed W Types Setzer 2004 IDw the theory of w iterated inductive definitions Its proof theoretic ordinal is equal to the Takeuti Feferman Buchholz ordinal T0 Feferman s constructive system of explicit mathematics has a larger proof theoretic ordinal which is also the proof theoretic ordinal of the KPi Kripke Platek set theory with iterated admissibles and S 2 1 A C B I displaystyle Sigma 2 1 mbox mathsf AC mathsf BI nbsp KPi an extension of Kripke Platek set theory based on a recursively inaccessible ordinal has a very large proof theoretic ordinal ps e I 1 displaystyle psi varepsilon I 1 nbsp described in a 1983 paper of Jager and Pohlers where I is the smallest inaccessible 6 This ordinal is also the proof theoretic ordinal of D 2 1 C A B I displaystyle Delta 2 1 mbox mathsf CA mathsf BI nbsp KPM an extension of Kripke Platek set theory based on a recursively Mahlo ordinal has a very large proof theoretic ordinal 8 which was described by Rathjen 1990 MLM an extension of Martin Lof type theory by one Mahlo universe has an even larger proof theoretic ordinal psW1 WM w K P P 3 R e f displaystyle mathsf KP Pi 3 Ref nbsp has a proof theoretic ordinal equal to PS e K 1 displaystyle Psi varepsilon K 1 nbsp where K displaystyle K nbsp refers to the first weakly compact due to Rathjen 1993 K P P w R e f displaystyle mathsf KP Pi omega Ref nbsp has a proof theoretic ordinal equal to PS X e 3 1 displaystyle Psi X varepsilon Xi 1 nbsp where 3 displaystyle Xi nbsp refers to the first P 0 2 displaystyle Pi 0 2 nbsp indescribable and X w P 0 ϵ ϵ 0 displaystyle mathbb X omega P 0 epsilon epsilon 0 nbsp due to Stegert 2010 S t a b i l i t y displaystyle mathsf Stability nbsp has a proof theoretic ordinal equal to PS X e Y 1 displaystyle Psi mathbb X varepsilon Upsilon 1 nbsp where Y displaystyle Upsilon nbsp is a cardinal analogue of the least ordinal a displaystyle alpha nbsp which is a b displaystyle alpha beta nbsp stable for all b lt a displaystyle beta lt alpha nbsp and X w P 0 ϵ ϵ 0 displaystyle mathbb X omega P 0 epsilon epsilon 0 nbsp due to Stegert 2010 Most theories capable of describing the power set of the natural numbers have proof theoretic ordinals that are so large that no explicit combinatorial description has yet been given This includes P 2 1 C A 0 displaystyle Pi 2 1 CA 0 nbsp full second order arithmetic P 1 C A 0 displaystyle Pi infty 1 CA 0 nbsp and set theories with powersets including ZF and ZFC The strength of intuitionistic ZF IZF equals that of ZF Table of ordinal analyses editTable of proof theoretic ordinals Ordinal First order arithmetic Second order arithmetic Kripke Platek set theory Type theory Constructive set theory Explicit mathematics w displaystyle omega nbsp Q displaystyle mathsf Q nbsp P A displaystyle mathsf PA nbsp w 2 displaystyle omega 2 nbsp R F A displaystyle mathsf RFA nbsp I D 0 displaystyle mathsf I Delta 0 nbsp w 3 displaystyle omega 3 nbsp E F A displaystyle mathsf EFA nbsp I D 0 displaystyle mathsf I Delta 0 mathsf nbsp R C A 0 displaystyle mathsf RCA 0 nbsp W K L 0 displaystyle mathsf WKL 0 nbsp w n displaystyle omega n nbsp 1 E F A n displaystyle mathsf EFA mathsf n nbsp I D 0 n displaystyle mathsf I Delta 0 mathsf n nbsp w w displaystyle omega omega nbsp P R A displaystyle mathsf PRA nbsp I S 1 displaystyle mathsf I Sigma 1 nbsp R C A 0 displaystyle mathsf RCA 0 nbsp W K L 0 displaystyle mathsf WKL 0 nbsp C P R C displaystyle mathsf CPRC nbsp w w w w displaystyle omega omega omega omega nbsp R C A 0 P 2 0 I N D displaystyle mathsf RCA 0 Pi 2 0 mathsf IND nbsp 7 40 e 0 displaystyle varepsilon 0 nbsp P A displaystyle mathsf PA nbsp A C A 0 displaystyle mathsf ACA 0 nbsp D 1 1 C A 0 displaystyle mathsf Delta 1 1 mathsf CA 0 nbsp S 1 1 A C 0 displaystyle mathsf Sigma 1 1 mathsf AC 0 nbsp R E W displaystyle text R widehat mathbf E boldsymbol Omega nbsp 8 p 8 K P u r displaystyle mathrm KPu r nbsp 9 p 869 E M 0 displaystyle mathsf EM 0 nbsp e w displaystyle varepsilon omega nbsp A C A 0 i R T displaystyle mathsf ACA 0 mathsf iRT nbsp 10 R C A 0 Y n X TJ n X Y displaystyle mathsf RCA 0 forall Y forall n exists X textrm TJ n X Y nbsp 11 8 e e 0 displaystyle varepsilon varepsilon 0 nbsp A C A displaystyle mathsf ACA nbsp 12 p 959 z 0 displaystyle zeta 0 nbsp A C A 0 X Y TJ w X Y displaystyle mathsf ACA 0 forall X exists Y textrm TJ omega X Y nbsp 13 11 p 1 A C A 0 displaystyle mathsf p 1 mathsf ACA 0 nbsp 14 7 R F N 0 displaystyle mathsf RFN 0 nbsp 13 p 17 A C A 0 B R displaystyle mathsf ACA 0 mathsf BR nbsp 13 p 5 f 2 e 0 displaystyle varphi 2 varepsilon 0 nbsp R F N displaystyle mathsf RFN nbsp A C A X Y TJ w X Y displaystyle mathsf ACA forall X exists Y textrm TJ omega X Y nbsp 13 p 52 f w 0 displaystyle varphi omega 0 nbsp I D 1 displaystyle mathsf ID 1 nbsp D 1 1 C R displaystyle mathsf Delta 1 1 mathsf CR nbsp S 1 1 D C 0 displaystyle Sigma 1 1 mathsf DC 0 nbsp 15 E M 0 J R displaystyle mathsf EM 0 mathsf JR nbsp f e 0 0 displaystyle varphi varepsilon 0 0 nbsp I D 1 displaystyle widehat mathsf ID 1 nbsp K F L displaystyle mathsf KFL nbsp 16 p 17 K F displaystyle mathsf KF nbsp 16 p 17 D 1 1 C A displaystyle mathsf Delta 1 1 mathsf CA nbsp 17 p 140 S 1 1 A C displaystyle mathsf Sigma 1 1 mathsf AC nbsp 17 p 140 S 1 1 D C displaystyle mathsf Sigma 1 1 mathsf DC nbsp 17 p 140 W E W displaystyle text W widehat mathbf E boldsymbol Omega nbsp 8 p 8 K P u r I N D N displaystyle mathrm KPu r mathrm IND N nbsp 9 p 870 M L 1 displaystyle mathsf ML 1 nbsp E M 0 J displaystyle mathsf EM 0 mathsf J nbsp f e e 0 0 displaystyle varphi varepsilon varepsilon 0 0 nbsp E W displaystyle widehat mathbf E boldsymbol Omega nbsp 8 p 27 E I D 1 displaystyle widehat mathbf EID boldsymbol 1 nbsp 8 p 27 f f w 0 0 displaystyle varphi varphi omega 0 0 nbsp P R S w displaystyle mathrm PRS omega nbsp 18 p 9 f lt W 0 displaystyle varphi mathsf lt Omega 0 nbsp 2 A u t I D displaystyle mathsf Aut ID nbsp G 0 displaystyle Gamma 0 nbsp I D lt w displaystyle widehat mathsf ID lt omega nbsp 19 U P A displaystyle mathsf U PA nbsp K F L displaystyle mathbf KFL nbsp 16 p 22 K F displaystyle mathbf KF nbsp 16 p 22 U N F A displaystyle mathcal U mathrm NFA nbsp 20 A T R 0 displaystyle mathsf ATR 0 nbsp D 1 1 C A B R displaystyle mathsf Delta 1 1 mathsf CA BR nbsp D 1 1 C A 0 S U B displaystyle Delta 1 1 mathrm CA 0 mathrm SUB nbsp 21 F P 0 displaystyle mathrm FP 0 nbsp 22 p 26 K P i 0 displaystyle mathsf KPi 0 nbsp 9 p 878 K P u 0 B R displaystyle mathsf KPu 0 mathrm BR nbsp 9 p 878 M L lt w displaystyle mathsf ML lt omega nbsp M L U displaystyle mathsf MLU nbsp G w w displaystyle Gamma omega omega nbsp K P I 0 S 1 I w displaystyle mathsf KPI 0 mathsf Sigma 1 I omega nbsp 23 p 13 G e 0 displaystyle Gamma varepsilon 0 nbsp I D w displaystyle widehat mathsf ID omega nbsp A T R displaystyle mathsf ATR nbsp 24 K P I 0 F I w displaystyle mathsf KPI 0 mathsf F I omega nbsp f 1 w 0 displaystyle varphi 1 omega 0 nbsp I D lt w w displaystyle widehat mathsf ID lt omega omega nbsp A T R 0 S 1 1 D C displaystyle mathsf ATR 0 mathsf Sigma 1 1 mathsf DC nbsp 14 7 K P i 0 S 1 I w displaystyle mathsf KPi 0 mathsf Sigma 1 I omega nbsp f 1 e 0 0 displaystyle varphi 1 varepsilon 0 0 nbsp I D lt e 0 displaystyle widehat mathsf ID lt varepsilon 0 nbsp A T R S 1 1 D C displaystyle mathsf ATR mathsf Sigma 1 1 mathsf DC nbsp 14 7 K P i 0 F I w displaystyle mathsf KPi 0 mathsf F I omega nbsp f 1 G 0 0 displaystyle varphi 1 Gamma 0 0 nbsp I D lt G 0 displaystyle widehat mathsf ID lt Gamma 0 nbsp M L S displaystyle mathsf MLS nbsp f 2 0 0 displaystyle varphi 2 0 0 nbsp A u t I D displaystyle mathsf Aut widehat ID nbsp F T R 0 displaystyle mathsf FTR 0 nbsp 25 A x S 1 1 A C T R 0 displaystyle Ax Sigma 1 1 mathsf AC mathsf TR 0 nbsp 26 p 1167 A x A T R S 1 1 D C R F N 0 displaystyle Ax mathsf ATR Sigma 1 1 mathsf DC mathsf RFN 0 nbsp 26 p 1167 K P h 0 displaystyle mathsf KPh 0 nbsp A u t M L displaystyle mathsf Aut ML nbsp f 2 0 e 0 displaystyle varphi 2 0 varepsilon 0 nbsp F T R displaystyle mathsf FTR nbsp 25 A x S 1 1 A C T R displaystyle Ax Sigma 1 1 mathsf AC mathsf TR nbsp 26 p 1167 A x A T R S 1 1 D C R F N displaystyle Ax mathsf ATR Sigma 1 1 mathsf DC mathsf RFN nbsp 26 p 1167 f 2 e 0 0 displaystyle varphi 2 varepsilon 0 0 nbsp K P h 0 F I w displaystyle mathsf KPh 0 mathsf F I omega nbsp 25 11 f w 0 0 displaystyle varphi omega 0 0 nbsp P 2 1 R F N 0 S 1 1 D C displaystyle Pi 2 1 mathsf RFN 0 Sigma 1 1 mathsf DC nbsp 27 p 233 S 1 1 T D C 0 displaystyle Sigma 1 1 mathsf TDC 0 nbsp 27 p 233 K P m 0 displaystyle mathsf KPm 0 nbsp 28 p 276 E M A displaystyle mathsf EMA nbsp 28 p 276 f e 0 0 0 displaystyle varphi varepsilon 0 0 0 nbsp P 2 1 R F N S 1 1 D C displaystyle Pi 2 1 mathsf RFN Sigma 1 1 mathsf DC nbsp 27 p 233 S 1 1 T D C displaystyle Sigma 1 1 mathsf TDC nbsp 14 K P m 0 L I N displaystyle mathsf KPm 0 mathcal L mathsf I mathsf N nbsp 28 p 277 E M A L I N displaystyle mathsf EMA mathbb L mathsf I mathsf N nbsp 28 p 277 f 1 0 0 0 displaystyle varphi 1 0 0 0 nbsp p 1 S 1 1 T D C 0 displaystyle mathsf p 1 Sigma 1 1 mathsf TDC 0 nbsp 14 7 ps W 1 W W w displaystyle psi Omega 1 Omega Omega omega nbsp R C A 0 P 1 1 C A displaystyle mathsf RCA 0 Pi 1 1 mathsf CA nbsp 29 p 3 A C A 0 displaystyle mathsf p 3 mathsf ACA 0 nbsp 14 7 ϑ W W displaystyle vartheta Omega Omega nbsp p 1 p 3 A C A 0 displaystyle mathsf p 1 mathsf p 3 mathsf ACA 0 nbsp 14 7 ps 0 e W 1 displaystyle psi 0 varepsilon Omega 1 nbsp 3 I D 1 displaystyle mathsf ID 1 nbsp W E W displaystyle text W widetilde mathbf E boldsymbol Omega nbsp 8 p 8 K P displaystyle mathsf KP nbsp 2 K P w displaystyle mathsf KP omega nbsp K P u displaystyle mathrm KPu nbsp 9 p 869 M L 1 V displaystyle mathsf ML 1 mathsf V nbsp C Z F displaystyle mathsf CZF nbsp E O N displaystyle mathsf EON nbsp ps e W e 0 displaystyle psi varepsilon Omega varepsilon 0 nbsp E W displaystyle widetilde mathbf E boldsymbol Omega nbsp 8 p 31 E I D 1 displaystyle widetilde mathbf EID boldsymbol 1 nbsp 8 p 31 A C A P 1 1 CA displaystyle mathbf ACA Pi 1 1 text CA nbsp 8 p 31 ps e W W displaystyle psi varepsilon Omega Omega nbsp I D 1 2 0 B R displaystyle mathsf ID 1 2 0 mathsf BR nbsp 30 ps e e W 1 displaystyle psi varepsilon varepsilon Omega 1 nbsp E W displaystyle mathbf E boldsymbol Omega nbsp 8 p 33 E I D 1 displaystyle mathbf EID boldsymbol 1 nbsp 8 p 33 A C A P 1 1 CA B I P R displaystyle mathbf ACA Pi 1 1 text CA mathrm BI mathrm PR nbsp 8 p 33 ps 0 G W 1 displaystyle psi 0 Gamma Omega 1 nbsp 4 U I D 1 displaystyle mathsf U ID 1 mathsf nbsp I D lt w displaystyle widehat mathsf ID lt omega bullet nbsp 22 p 26 S 1 1 D C 0 S U B displaystyle Sigma 1 1 mathsf DC 0 bullet mathsf SUB bullet nbsp 22 p 26 A T R 0 displaystyle mathsf ATR 0 bullet nbsp 22 p 26 S 1 1 A C 0 S U B displaystyle Sigma 1 1 mathsf AC 0 bullet mathsf SUB bullet nbsp 22 p 26 U I D 1 displaystyle mathcal U mathsf ID 1 nbsp 22 p 26 F P 0 displaystyle mathsf FP 0 bullet nbsp 22 p 26 A T R 0 displaystyle mathsf ATR 0 bullet nbsp 22 p 26 ps 0 f lt W 0 W 1 displaystyle psi 0 varphi mathsf lt Omega 0 Omega 1 nbsp A u t U I D displaystyle mathsf Aut U ID nbsp ps 0 W w displaystyle psi 0 Omega omega nbsp I D lt w displaystyle mathsf ID lt omega nbsp P 1 1 C A 0 displaystyle mathsf Pi 1 1 mathsf CA 0 nbsp D 2 1 C A 0 displaystyle mathsf Delta 2 1 mathsf CA 0 nbsp M L W displaystyle mathsf MLW nbsp ps 0 W w w w displaystyle psi 0 Omega omega omega omega nbsp P 1 1 C A 0 P 2 1 I N D displaystyle Pi 1 1 mathsf CA 0 Pi 2 1 mathsf IND nbsp 31 ps 0 W w e 0 displaystyle psi 0 Omega omega varepsilon 0 nbsp W I D w displaystyle mathsf W ID omega nbsp P 1 1 C A displaystyle mathsf Pi 1 1 mathsf CA nbsp 32 p 14 W K P I displaystyle mathsf W KPI nbsp ps 0 W w W displaystyle psi 0 Omega omega Omega nbsp P 1 1 C A B R displaystyle Pi 1 1 mathsf CA BR nbsp 33 ps 0 W w w displaystyle psi 0 Omega omega omega nbsp P 1 1 C A 0 P 2 1 B I displaystyle Pi 1 1 mathsf CA 0 Pi 2 1 mathsf BI nbsp 31 ps 0 W w w w displaystyle psi 0 Omega omega omega omega nbsp P 1 1 C A 0 P 2 1 B I P 3 1 I N D displaystyle Pi 1 1 mathsf CA 0 Pi 2 1 mathsf BI Pi 3 1 mathsf IND nbsp 31 ps 0 e W w 1 displaystyle psi 0 varepsilon Omega omega 1 nbsp 5 I D w displaystyle mathsf ID omega nbsp P 1 1 C A B I displaystyle mathsf Pi 1 1 mathsf CA BI nbsp K P I displaystyle mathsf KPI nbsp ps 0 W w w displaystyle psi 0 Omega omega omega nbsp I D lt w w displaystyle mathsf ID lt omega omega nbsp D 2 1 C R displaystyle mathsf Delta 2 1 mathsf CR nbsp ps 0 W e 0 displaystyle psi 0 Omega varepsilon 0 nbsp I D lt e 0 displaystyle mathsf ID lt varepsilon 0 nbsp D 2 1 C A displaystyle mathsf Delta 2 1 mathsf CA nbsp S 2 1 A C displaystyle mathsf Sigma 2 1 mathsf AC nbsp W K P i displaystyle mathsf W KPi nbsp ps 0 W W displaystyle psi 0 Omega Omega nbsp A u t I D displaystyle mathsf Aut ID nbsp 6 ps W 1 e W W 1 displaystyle psi Omega 1 varepsilon Omega Omega 1 nbsp I D displaystyle mathsf ID prec nbsp B I D 2 displaystyle mathsf BID 2 nbsp I D 2 B I displaystyle mathsf ID 2 mathsf BI nbsp 34 K P l displaystyle mathsf KPl nbsp K P l W r displaystyle mathsf KPl Omega r nbsp ps 0 F 1 0 displaystyle psi 0 Phi 1 0 nbsp P 1 1 T R 0 displaystyle Pi 1 1 mathsf TR 0 nbsp P 1 1 T R 0 D 2 1 C A 0 displaystyle Pi 1 1 mathsf TR 0 Delta 2 1 mathsf CA 0 nbsp D 2 1 C A B I i m p l S 2 1 displaystyle Delta 2 1 mathsf CA BI impl Sigma 2 1 nbsp D 2 1 C A B R i m p l S 2 1 displaystyle Delta 2 1 mathsf CA BR impl Sigma 2 1 nbsp A U T I D 0 p o s displaystyle mathbf AUT ID 0 pos nbsp A U T I D 0 m o n displaystyle mathbf AUT ID 0 mon nbsp 34 72 K P i w F O U N D R i m p l S displaystyle mathsf KPi w mathsf FOUNDR mathsf impl Sigma nbsp 34 72 K P i w F O U N D i m p l S displaystyle mathsf KPi w mathsf FOUND mathsf impl Sigma nbsp 34 72 A U T K P l r displaystyle mathbf AUT KPl r nbsp A U T K P l r K P i r displaystyle mathbf AUT KPl r mathbf KPi r nbsp 34 72 ps 0 F 1 0 e 0 displaystyle psi 0 Phi 1 0 varepsilon 0 nbsp P 1 1 T R displaystyle Pi 1 1 mathsf TR nbsp A U T I D p o s displaystyle mathbf AUT ID pos nbsp A U T I D m o n displaystyle mathbf AUT ID mon nbsp 34 72 A U T K P l w displaystyle mathbf AUT KPl w nbsp 34 72 ps 0 e F 1 0 1 displaystyle psi 0 varepsilon Phi 1 0 1 nbsp P 1 1 T R B I displaystyle Pi 1 1 mathsf TR mathsf BI nbsp A U T I D 2 p o s displaystyle mathbf AUT ID 2 pos nbsp A U T I D 2 m o n displaystyle mathbf AUT ID 2 mon nbsp 34 72 A U T K P l displaystyle mathbf AUT KPl nbsp 34 72 ps 0 F 1 e 0 displaystyle psi 0 Phi 1 varepsilon 0 nbsp P 1 1 T R D 2 1 C A displaystyle Pi 1 1 mathsf TR Delta 2 1 mathsf CA nbsp P 1 1 T R S 2 1 A C displaystyle Pi 1 1 mathsf TR Sigma 2 1 mathsf AC nbsp A U T K P l w K P i w displaystyle mathbf AUT KPl w mathbf KPi w nbsp 34 72 ps 0 F w 0 displaystyle psi 0 Phi omega 0 nbsp D 2 1 T R 0 displaystyle Delta 2 1 mathsf TR 0 nbsp S 2 1 T R D C 0 displaystyle Sigma 2 1 mathsf TRDC 0 nbsp D 2 1 C A 0 S 2 1 B I displaystyle Delta 2 1 mathsf CA 0 Sigma 2 1 mathsf BI nbsp 34 72 K P i r S F O U N D displaystyle mathbf KPi r Sigma mathsf FOUND nbsp K P i r S R E C displaystyle mathbf KPi r Sigma mathsf REC nbsp 34 72 ps 0 F e 0 0 displaystyle psi 0 Phi varepsilon 0 0 nbsp D 2 1 T R displaystyle Delta 2 1 mathsf TR nbsp S 2 1 T R D C displaystyle Sigma 2 1 mathsf TRDC nbsp D 2 1 C A S 2 1 B I displaystyle Delta 2 1 mathsf CA Sigma 2 1 mathsf BI nbsp 34 72 K P i w S F O U N D displaystyle mathbf KPi w Sigma mathsf FOUND nbsp K P i w S R E C displaystyle mathbf KPi w Sigma mathsf REC nbsp 34 72 ps e I 1 displaystyle psi varepsilon I 1 nbsp 7 D 2 1 C A B I displaystyle mathsf Delta 2 1 mathsf CA BI nbsp S 2 1 A C B I displaystyle mathsf Sigma 2 1 mathsf AC BI nbsp K P i displaystyle mathsf KPi nbsp C Z F R E A displaystyle mathsf CZF REA nbsp T 0 displaystyle mathsf T 0 nbsp ps W I w displaystyle psi Omega I omega nbsp M L 1 W displaystyle mathsf ML 1 mathsf W nbsp 35 38 ps W L displaystyle psi Omega L nbsp 8 K P h displaystyle mathsf KPh nbsp M L lt w W displaystyle mathsf ML lt omega mathsf W nbsp ps W L displaystyle psi Omega L nbsp 9 A u t M L W displaystyle mathsf Aut MLW nbsp ps W x e M 1 0 displaystyle psi Omega chi varepsilon M 1 0 nbsp 10 D 2 1 C A B I M displaystyle mathsf Delta 2 1 mathsf CA BI M nbsp K P M displaystyle mathsf KPM nbsp C Z F M displaystyle mathsf CZFM nbsp ps W M w displaystyle psi Omega M omega nbsp 11 K P M displaystyle mathsf KPM nbsp M L M displaystyle mathsf MLM nbsp PS W 0 e K 1 displaystyle Psi Omega 0 varepsilon K 1 nbsp 12 K P P 3 R e f displaystyle mathsf KP Pi 3 mathsf Ref nbsp 36 PS w P 0 ϵ ϵ 0 e 3 1 displaystyle Psi omega P 0 epsilon epsilon 0 varepsilon Xi 1 nbsp 13 K P P w R e f displaystyle mathsf KP Pi omega mathsf Ref nbsp PS w P 0 ϵ ϵ 0 e Y 1 displaystyle Psi omega P 0 epsilon epsilon 0 varepsilon Upsilon 1 nbsp 14 S t a b i l i t y displaystyle mathsf Stability nbsp ps w 1 C K e I 1 displaystyle psi omega 1 CK varepsilon mathbb I 1 nbsp 37 S 3 1 D C B I displaystyle Sigma 3 1 mathsf DC BI nbsp K P P 1 c o l l e c t i o n displaystyle mathsf KP Pi 1 mathsf collection span, wikipedia, wiki, book, books, library, article , read, download, free, free download, mp3, video, mp4, 3gp, jpg, jpeg, gif, png, picture, music, song, movie, book, game, games. © Copyright 2021, All Rights Reserved  |   www.wiki3.en-us.nina.az Rss Feed SiteMap Ping DMCA Contact Us HomePage Closed Call: