Êtes-vous un étudiant de l'EPFL à la recherche d'un projet de semestre?
Travaillez avec nous sur des projets en science des données et en visualisation, et déployez votre projet sous forme d'application sur Graph Search.
Concept
Ordinal analysis
Résumé
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 .
Source officielle
À propos de ce résultat
Cette page est générée automatiquement et peut contenir des informations qui ne sont pas correctes, complètes, à jour ou pertinentes par rapport à votre recherche. Il en va de même pour toutes les autres pages de ce site. Veillez à vérifier les informations auprès des sources officielles de l'EPFL.