Are you an EPFL student looking for a semester project?
Work with us on data science and visualisation projects, and deploy your project as an app on top of Graph Search.
Concept
Ordinal analysis
Summary
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.
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 ε0. See Gentzen's consistency proof.
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 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 for which there exists a notation in Kleene's sense such that proves that is an ordinal notation. Equivalently, it is the supremum of all ordinals such that there exists a recursive relation on (the set of natural numbers) that well-orders it with ordinal and such that proves transfinite induction of arithmetical statements for .
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 to "prove well-ordered", we instead construct an ordinal notation with order type . can now work with various transfinite induction principles along , 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 that is well-founded iff PA is consistent, despite having order type - including such a notation in the ordinal analysis of PA would result in the false equality .
Official source
About this result
This page is automatically generated and may contain information that is not correct, complete, up-to-date, or relevant to your search query. The same applies to every other page on this website. Please make sure to verify the information with EPFL's official sources.