Roe solver

2011-05-13T09:24:29Z

153.96.89.3: /* Quasi-linear Hyperbolic system */ F(U) instead of F

In [[proof theory]], '''ordinal analysis''' assigns [[ordinal number|ordinals]] (often [[large countable ordinals]]) to mathematical theories as a measure of their strength. The field was formed when [[Gerhard Gentzen]] in 1934 used [[cut elimination]] to prove, in modern terms, that the '''proof theoretic ordinal''' of [[Peano arithmetic]] is [[epsilon zero|ε0]].

==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 <math>T</math> is the smallest recursive ordinal that the theory cannot prove is [[Well-founded relation|well founded]] — the supremum of all ordinals <math>\alpha</math> for which there exists a [[Kleene's O|notation <math>o</math> in Kleene's sense]] such that <math>T</math> proves that <math>o</math> is an [[ordinal notation]]. Equivalently, it is the supremum of all ordinals <math>\alpha</math> such that there exists a [[Computable function|recursive relation]] <math>R</math> on <math>\omega</math> (the set of natural numbers) which [[well-order]]s it with ordinal <math>\alpha</math> and such that <math>T</math> proves [[transfinite induction]] of arithmetical statements for <math>R</math>.

The existence of any recursive ordinal which the theory fails to prove is well ordered follows from the <math>\Sigma^1_1</math> bounding theorem, as the set of natural numbers which an effective theory proves to be ordinal notations is a <math>\Sigma^0_1</math> set (see [[Hyperarithmetical theory]]). Thus the proof theoretic ordinal of a theory will always be a countable ordinal less than the [[Church-Kleene ordinal]] <math>\omega_1^{\mathrm{CK}}</math>.

In practice, the proof theoretic ordinal of a theory is a good measure of the strength of a theory. If theories have the same proof theoretic ordinal they are often [[equiconsistency|equiconsistent]], and if one theory has a larger proof theoretic ordinal than another it can often prove the consistency of the second theory.

==Examples==
===Theories with proof theoretic ordinal ω2===
*RFA, [[rudimentary function]] arithmetic.<ref name=Krajicek>{{cite book|last=Krajicek|first=Jan|title=Bounded Arithmetic, Propositional Logic and Complexity Theory|year=1995|publisher=Cambridge University Press|isbn=9780521452052|pages=18-20}} defines the rudimentary sets and rudimentary functions, and proves them equivalent to the Δ0-predicates on the naturals.  An ordinal analysis of the system can be found in {{cite book|last=Rose|first=H. E.|title=Subrecursion: functions and hierarchies|year=1984|publisher=Clarendon Press|location=University of Michigan|isbn=9780198531890}}</ref>
*IΔ0, arithmetic with induction on Δ0-predicates without any axiom asserting that exponentiation is total.

===Theories with proof theoretic ordinal ω3===
Friedman's [[grand conjecture]] suggests that much "ordinary" mathematics can be proved in weak systems having this as their proof-theoretic ordinal.
*EFA, [[elementary function arithmetic]].
*IΔ0 + exp, arithmetic with induction on Δ0-predicates augmented by an axiom asserting that exponentiation is total.
*RCA{{su|p=*|b=0}}, a second order form of EFA sometimes used in [[reverse mathematics]].
*WKL{{su|p=*|b=0}}, a second order form of EFA sometimes used in [[reverse mathematics]].

===Theories with proof theoretic ordinal ω''n''===
*IΔ0 or EFA augmented by an axiom ensuring that each element of the ''n''-th level <math>\mathcal{E}^n</math> of the [[Grzegorczyk hierarchy]] is total.

===Theories with proof theoretic ordinal ωω===
*RCA0, [[second-order arithmetic#Recursive comprehension|recursive comprehension]].
*WKL0, [[weak König's lemma]].
*PRA, [[primitive recursive arithmetic]].
*IΣ1, arithmetic with induction on Σ1-predicates.

===Theories with proof theoretic ordinal ε0===
*PA, [[Peano arithmetic]] ([[Gentzen's consistency proof|shown]] by [[Gentzen]] using [[cut elimination]]).
*ACA0, [[arithmetical comprehension]].

===Theories with proof theoretic ordinal the Feferman-Schütte ordinal Γ0===
This ordinal is sometimes considered to be the upper limit for "predicative" theories.

*ATR0, [[arithmetical transfinite recursion]].
*[[Martin-Löf type theory]] with arbitrarily many finite level universes.

===Theories with proof theoretic ordinal the Bachmann-Howard ordinal===
* ID1, the theory of inductive definitions.
* KP, [[Kripke-Platek set theory]] with the [[axiom of infinity]].
* CZF, Aczel's [[constructive set theory#Aczel's constructive Zermelo–Fraenkel|constructive Zermelo-Fraenkel set theory]].
* MLW, Martin-Löf Type Theory with indexed W-Types
* EON, a weak variant of the [[Solomon_Feferman|Fefferman]]'s explicit mathematics system T0.

===Theories with larger proof theoretic ordinals===
*<math>\Pi^1_1\mbox{-}\mathsf{CA}_0</math>, [[second order arithmetic|Π11 comprehension]] has a rather large proof theoretic ordinal, which was described by Takeuti in terms of "ordinal diagrams", and which is bounded by [[Psi0(Omega omega)|ψ0(Ωω)]] in [[Buchholz's notation]]. It is also the ordinal of <math>ID_{<\omega}</math>, the theory of finitely iterated inductive definitions.
*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 <math>\Sigma^1_2\mbox{-}\mathsf{AC} + \mathsf{BI}</math>.
*KPM, an extension of [[Kripke-Platek set theory]] based on a [[Mahlo cardinal]], has a very large proof theoretic ordinal ϑ, which was described by {{harvtxt|Rathjen|1990}}.
*MLM, an extension of Martin-Löf type theory by one Mahlo-universe, has an even larger proof theoretic ordinal ψΩ1(ΩM + ω).

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 ({{asof|2008|lc=1}}) been given. This includes [[second order arithmetic]] and set theories with powersets. (The CZF and Kripke-Platek set theories mentioned above are weak set theories without powersets.)

==See also==
*[[Equiconsistency]]
*[[Large cardinal property]]
*[[Feferman–Schütte ordinal]]
*[[Bachmann–Howard ordinal]]

==References==
*{{citation|last=Buchholz|first= W.|last2= Feferman|first2= S.|last3= Pohlers|first3= W.|last4= Sieg|first4= W. |title=Iterated inductive definitions and sub-systems of analysis|series= Lecture Notes in Math.|volume= 897|publisher= Springer-Verlag|place= Berlin |year=1981|doi=10.1007/BFb0091894
|isbn =978-3-540-11170-2}}
*{{citation|last=Pohlers|first=Wolfram |title=Proof theory|mr=1026933
|series= Lecture Notes in Mathematics|volume= 1407|publisher= Springer-Verlag|place= Berlin|year= 1989|isbn= 3-540-51842-8 }}
*{{citation|last=Pohlers|first=Wolfram | title=Handbook of Proof Theory|chapter=Set Theory and Second Order Number Theory| pages=210–335| series= Studies in Logic and the Foundations of Mathematics|volume= 137|publisher= Elsevier Science B. V.|place= Amsterdam|year= 1998|mr=1640328|isbn= 0-444-89840-9
|work = Handbook of Proof Theory }}
*{{citation|mr=1062729
|last=Rathjen|first= Michael
|title=Ordinal notations based on a weakly Mahlo cardinal.
|journal=Arch. Math. Logic|volume= 29 |year=1990|issue= 4|pages=249–263|doi=10.1007/BF01651328}}
*{{citation|url=http://www.icm2006.org/proceedings/Vol_II/contents/ICM_Vol_2_03.pdf|chapter=The art of ordinal analysis
|first=Michael|last= Rathjen
|mr=2275588
|title=International Congress of Mathematicians|volume= II|pages= 45–69|publisher= Eur. Math. Soc.|place= Zürich, |year=2006}}
*{{citation| first=H.E. | last= Rose
|title=Subrecursion. Functions and Hierarchies |series= Oxford logic guides |volume = 9
|publisher= Clarendon Press, Oxford University Press|place= Oxford, New York |year=1984}}
*{{citation|mr=0505313|last= Schütte|first= Kurt |title=Proof theory|series= Grundlehren der Mathematischen Wissenschaften|volume= 225|publisher= Springer-Verlag|place= Berlin-New York|year= 1977|pages= xii+299 | isbn= 3-540-07911-4}}
*{{citation|mr=0882549|last= Takeuti|first= Gaisi |title=Proof theory|edition= Second |series= Studies in Logic and the Foundations of Mathematics|volume= 81|publisher= North-Holland Publishing Co.|place= Amsterdam|year=1987| isbn= 0-444-87943-9}}
<references/>

[[Category:Proof theory]]
[[Category:Ordinal numbers]]

formulasearchengine - User contributions [en]

Roe solver