Incomplétude de Gödel et calculabilité

Les théorèmes d'incomplétude de Gödel montrent que tout système formel suffisamment puissant et cohérent contient des énoncés vrais qu'il ne peut prouver, un résultat profondément lié à l'indécidabilité découverte en théorie de la calculabilité.

Definition

Les théorèmes d'incomplétude stipulent que tout système formel cohérent capable d'exprimer l'arithmétique de base est incomplet, contenant des énoncés arithmétiques vrais qu'il ne peut prouver, et ne peut prouver sa propre cohérence ; en termes computationnels, l'ensemble des énoncés prouvables est reconnaissable mais son complément ne l'est pas, reflétant l'indécidabilité.

Scope

Ce sujet aborde les premier et second théorèmes d'incomplétude, la technique d'arithmétisation et d'autoréférence par la numérotation de Gödel, la relation étroite entre l'incomplétude et l'indécidabilité du problème de l'arrêt et de la logique du premier ordre, ainsi que les conséquences pour les limites du raisonnement formel et de la preuve automatisée.

Core questions

• Pourquoi aucun système formel cohérent et suffisamment puissant ne peut-il prouver tous les énoncés arithmétiques vrais ?
• Comment l'autoréférence via la numérotation de Gödel produit-elle une phrase vraie indémontrable ?
• Comment l'incomplétude et l'indécidabilité du problème de l'arrêt sont-elles deux facettes d'un même phénomène ?
• Qu'implique l'incomplétude pour les limites de la preuve de théorème automatisée ?

Key theories

Premier théorème d'incomplétude

Tout système formel cohérent et suffisamment puissant pour encoder l'arithmétique contient un énoncé vrai qu'il ne peut ni prouver ni réfuter, construit par une phrase qui affirme effectivement sa propre indémontrabilité.

Incomplétude via la calculabilité

L'incomplétude découle de l'indécidabilité du problème de l'arrêt : si toute vérité arithmétique était prouvable, on pourrait décider l'arrêt en cherchant des preuves, de sorte que l'existence de problèmes indécidables impose l'existence de vérités indémontrables.

Clinical relevance

L'incomplétude et son équivalent computationnel imposent des limites strictes au raisonnement automatisé : aucun algorithme ne peut décider toutes les vérités arithmétiques ou résoudre toutes les questions mathématiques, de sorte que les prouveurs de théorèmes et les systèmes de vérification doivent s'appuyer sur l'orientation humaine, des théories restreintes ou des preuves interactives plutôt que sur une décision automatique complète.

History

Gödel a prouvé les théorèmes d'incomplétude en 1931, anéantissant l'espoir de Hilbert d'une formalisation complète et auto-justificatrice des mathématiques. En l'espace de cinq ans, Church et Turing ont lié ces limites à l'indécidabilité, et l'interprétation computationnelle de l'incomplétude à travers le problème de l'arrêt est devenue un pilier de la théorie de la calculabilité.

Key figures

• Kurt Gödel
• Alan Turing
• Alonzo Church
• John Barkley Rosser

Seminal works

• godel1931
• boolos2007

Frequently asked questions

L'incomplétude signifie-t-elle que les mathématiques sont défaillantes ?

Non. Cela signifie qu'aucun système formel cohérent unique ne peut prouver toutes les vérités arithmétiques, et non que les mathématiques sont incohérentes ou peu fiables. Les mathématiciens travaillent au sein et à travers des systèmes formels, et l'incomplétude marque simplement une limite intrinsèque à ce que tout système fixe peut englober.

Comment le théorème de Gödel est-il lié au problème de l'arrêt ?

Ils sont étroitement liés. L'insolvabilité du problème de l'arrêt implique l'incomplétude : si un système formel pouvait prouver toutes les vérités concernant les programmes qui s'arrêtent, on pourrait décider l'arrêt en cherchant des preuves, ce qui contredirait le résultat de Turing. Les deux expriment, en logique et en calcul, les mêmes limites fondamentales de la méthode formelle.