5 minutes Lebesgue

Mathias Rousset, Un algorithme dont l’arrêt n’est pas Peano-prouvable

Bien que très coûteux à calculer pour les machines, les suites de Goodstein forment un exemple 'simple' d'algorithme récursif arithmétique (ce sont des suites d'entiers) qui peuvent s'implémenter très facilement dans n'importe quel langage manipulant l'arithmétique. L'algorithme se termine pour toute condition initiale, mais il a été (méta-)démontré que cette propriété n'est pas prouvable à partir des axiomes de Peano. On donnera ici le schéma d'une preuve simple reposant sur la théorie des nombres ordinaux (qui nécessite les axiomes usuels de la théorie des ensembles, par exemple ZF).

IRMAR
2 April 2019
en cours d'évaluation
Mathematical field: 
algebra, logic

Partners

Irmar LMJL ENS Rennes LMBA LAREMA

Affiliation

ANR CNRS Rennes 1 Rennes 2 Nantes INSA Rennes INRIA ENSRennes UBO UBS Angers UBL