Systèmes de logique basés sur des ordinaux -Systems of Logic Based on Ordinals

Systems of Logic Based on Ordinals était la thèse de doctorat du mathématicien Alan Turing .

La thèse de Turing ne porte pas sur un nouveau type de logique formelle, et il ne s'intéressait pas non plus aux systèmes dits de « logique classée » dérivés de la numérotation ordinale ou relative, dans lesquels des comparaisons peuvent être faites entre les états de vérité sur la base de la véracité relative. Au lieu de cela, Turing a étudié la possibilité de résoudre la condition d'incomplétude de Godelian en utilisant la méthode des infinis de Cantor . Cette condition peut être énoncée ainsi : dans tous les systèmes avec des ensembles finis d'axiomes, une condition de ou-exclusif s'applique au pouvoir d'expression et à la prouvabilité ; c'est-à-dire que l'on peut avoir du pouvoir et pas de preuve, ou une preuve et pas de pouvoir, mais pas les deux.

La thèse est une exploration des systèmes mathématiques formels d'après le théorème de Gödel . Gödel a montré pour cela que tout système formel S suffisamment puissant pour représenter l'arithmétique, il existe un théorème G qui est vrai mais le système est incapable de le prouver. G pourrait être ajouté comme axiome supplémentaire au système à la place d'une preuve. Cependant, cela créerait un nouveau système S' avec son propre théorème vrai non démontrable G', et ainsi de suite. La thèse de Turing examine ce qui se passe si vous répétez simplement ce processus à plusieurs reprises, générant un ensemble infini de nouveaux axiomes à ajouter à la théorie originale, et va même un peu plus loin en utilisant la récursion transfinie pour aller "au-delà de l'infini", produisant un ensemble de nouvelles théories G n , une pour chaque nombre ordinal n.

La thèse a été achevée à Princeton sous Alonzo Church et était un travail classique en mathématiques qui a introduit le concept de logique ordinale .

Martin Davis déclare que bien que l'utilisation par Turing d'un oracle informatique ne soit pas un objectif majeur de la thèse, il s'est avéré très influent en informatique théorique , par exemple dans la hiérarchie temporelle polynomiale .

Les références

Liens externes