Analyse ordinale

L'analyse ordinale mesure la force d'une théorie formelle par le plus petit ordinal dont la théorie ne peut prouver qu'il est bien ordonné, en attribuant un ordinal de démontrabilité précis à chaque théorie.

Definition

L'ordinal de démontrabilité d'une théorie est le supremum des types d'ordre des bons ordres récursifs dont la théorie peut prouver la bonne fondation ; l'analyse ordinale est le programme de calcul de cet invariant et de son utilisation pour comparer et calibrer les théories.

Scope

Ce sujet aborde la preuve de cohérence de l'arithmétique de Gentzen utilisant l'induction transfinie jusqu'à l'ordinal epsilon-zéro, les systèmes de notation ordinale, l'ordinal de démontrabilité comme invariant d'une théorie, les méthodes d'élimination des coupures pour les dérivations infinies, et l'analyse des sous-systèmes de l'arithmétique et des théories prédicatives.

Core questions

• Comment un ordinal mesure-t-il la force d'une théorie arithmétique ?
• Pourquoi l'induction transfinie jusqu'à epsilon-zéro prouve-t-elle la cohérence de l'arithmétique ?
• Comment les notations ordinales sont-elles définies de manière à pouvoir être manipulées de façon finie ?
• Quels ordinaux correspondent aux sous-systèmes standards de l'arithmétique du second ordre ?

Key theories

Preuve de cohérence de Gentzen

Gentzen a prouvé la cohérence de l'arithmétique du premier ordre en attribuant des ordinaux inférieurs à epsilon-zéro aux preuves et en montrant que la réduction des coupures les diminue, ainsi l'induction transfinie jusqu'à epsilon-zéro certifie la cohérence.

Ordinal de démontrabilité

Chaque théorie suffisamment forte possède un ordinal caractéristique qui capture l'induction transfinie qu'elle peut justifier, fournissant une échelle de force logique fine et largement linéaire.

Systèmes de notation ordinale

Les grands ordinaux sont représentés par des notations syntaxiques finies, telles que les fonctions de Veblen et les fonctions d'effondrement, permettant de manipuler des ordinaux infinis au sein de théories finitaires ou arithmétiques.

Clinical relevance

L'analyse ordinale fournit la mesure la plus raffinée disponible de la force des théories mathématiques : elle détermine précisément quelles inductions transfinites une théorie nécessite, classe les fonctions récursives prouvables d'une théorie, et fournit des informations de cohérence relative complémentaires à celles obtenues à partir des grands cardinaux.

History

Les preuves de cohérence de l'arithmétique de Gentzen de 1936 et 1938 ont introduit l'analyse ordinale par l'induction transfinie jusqu'à epsilon-zéro. Schuette, Feferman et d'autres ont étendu la méthode aux théories prédicatives et à l'analyse ramifiée, et le développement des fonctions d'effondrement a ensuite poussé l'analyse ordinale vers des systèmes impredicatifs forts.

Key figures

• Gerhard Gentzen
• Kurt Schuette
• Solomon Feferman
• Wolfram Pohlers

Seminal works

• pohlers2009
• takeuti1987
• schutte1977

Frequently asked questions

Quel est l'ordinal de démontrabilité de l'arithmétique du premier ordre ?

C'est epsilon-zéro, la limite de la tour d'exponentielles oméga. L'arithmétique du premier ordre prouve l'induction transfinie jusqu'à n'importe quel ordinal inférieur à epsilon-zéro, mais pas jusqu'à epsilon-zéro lui-même, ce qui est précisément le principe que Gentzen a utilisé pour prouver sa cohérence.

Comment l'analyse ordinale est-elle liée à l'incomplétude ?

Le second théorème de Gödel stipule que l'arithmétique ne peut pas prouver sa propre cohérence. L'analyse ordinale identifie le principe additionnel, l'induction transfinie jusqu'à epsilon-zéro, qui la prouve, mesurant ainsi précisément jusqu'où il faut aller au-delà de la théorie pour établir sa cohérence.