Théorème de complétude de Gödel - Gödel's completeness theorem

La formule ( x . R ( x , x )) (∀ x y . R ( x , y )) tient dans toutes les structures (seuls les 8 plus simples sont affichés à gauche). Par le résultat de complétude de Gödel, il doit donc avoir une preuve de déduction naturelle (montrée à droite).

Le théorème de complétude de Gödel est un théorème fondamental en logique mathématique qui établit une correspondance entre la vérité sémantique et la prouvabilité syntaxique en logique du premier ordre .

Le théorème de complétude s'applique à toute théorie du premier ordre : Si T est une telle théorie, et est une phrase (dans le même langage) et tout modèle de T est un modèle de , alors il existe une preuve (du premier ordre) de en utilisant les énoncés de T comme axiomes. On dit parfois cela comme "tout ce qui est vrai est prouvable".

Elle établit un lien étroit entre la théorie des modèles qui traite de ce qui est vrai dans différents modèles et la théorie de la preuve qui étudie ce qui peut être formellement prouvé dans des systèmes formels particuliers .

Il a été prouvé pour la première fois par Kurt Gödel en 1929. Il a ensuite été simplifié en 1947, lorsque Leon Henkin a observé dans son doctorat. thèse selon laquelle la partie dure de la preuve peut être présentée comme le théorème d'existence modèle (publié en 1949). La preuve de Henkin a été simplifiée par Gisbert Hasenjaeger en 1953.

Préliminaires

Il existe de nombreux systèmes déductifs pour la logique du premier ordre, y compris les systèmes de déduction naturelle et les systèmes de style Hilbert . La notion de déduction formelle est commune à tous les systèmes déductifs . Il s'agit d'une séquence (ou, dans certains cas, d'un arbre fini ) de formules avec une conclusion spécialement désignée . La définition d'une déduction est telle qu'elle est finie et qu'il est possible de vérifier algorithmiquement (par un ordinateur par exemple, ou à la main) qu'une suite (ou arbre) donnée de formules est bien une déduction.

Une formule du premier ordre est dite logiquement valide si elle est vraie dans chaque structure pour le langage de la formule (c'est-à-dire pour toute affectation de valeurs aux variables de la formule). Pour énoncer formellement, puis prouver, le théorème de complétude, il faut également définir un système déductif. Un système déductif est dit complet si chaque formule logiquement valide est la conclusion d'une déduction formelle, et le théorème de complétude pour un système déductif particulier est le théorème qu'il est complet dans ce sens. Ainsi, dans un sens, il existe un théorème de complétude différent pour chaque système déductif. L'inverse de la complétude est la justesse , le fait que seules des formules logiquement valides peuvent être prouvées dans le système déductif.

Si un système déductif spécifique de la logique du premier ordre est sain et complet, alors il est « parfait » (une formule est prouvable si et seulement si elle est logiquement valide), donc équivalent à tout autre système déductif de même qualité (toute preuve dans un système peut être converti dans l'autre).

Déclaration

Nous fixons d'abord un système déductif de calcul des prédicats du premier ordre, en choisissant l'un des systèmes équivalents bien connus. La preuve originale de Gödel supposait le système de preuve Hilbert-Ackermann.

La formulation originale de Gödel

Le théorème de complétude dit que si une formule est logiquement valide alors il y a une déduction finie (une preuve formelle) de la formule.

Ainsi, le système déductif est "complet" dans le sens où aucune règle d'inférence supplémentaire n'est requise pour prouver toutes les formules logiquement valides. L'inverse de la complétude est la justesse , le fait que seules des formules logiquement valides sont prouvables dans le système déductif. Avec la solidité (dont la vérification est facile), ce théorème implique qu'une formule est logiquement valide si et seulement si elle est la conclusion d'une déduction formelle.

Forme plus générale

Le théorème peut être exprimé plus généralement en termes de conséquence logique . On dit qu'une phrase s est une conséquence syntaxique d'une théorie T , notée , si s est prouvable à partir de T dans notre système déductif. On dit que s est une conséquence sémantique de T , notée , si s est vérifiée dans tout modèle de T . Le théorème de complétude dit alors que pour toute théorie du premier ordre T avec un langage bien ordonné , et toute phrase s dans le langage de T ,

si , alors .

Puisque l'inverse (la solidité) est également vrai, il s'ensuit que si et seulement si , et donc que les conséquences syntaxiques et sémantiques sont équivalentes pour la logique du premier ordre.

Ce théorème plus général est utilisé implicitement, par exemple, lorsqu'une phrase est prouvée à partir des axiomes de la théorie des groupes en considérant un groupe arbitraire et en montrant que la phrase est satisfaite par ce groupe.

La formulation originale de Gödel se déduit en prenant le cas particulier d'une théorie sans aucun axiome.

Théorème d'existence du modèle

Le théorème de complétude peut également être compris en termes de cohérence , en conséquence du théorème d'existence du modèle de Henkin . On dit qu'une théorie T est syntaxiquement cohérente s'il n'y a pas de phrase s telle que s et sa négation ¬ s soient prouvables à partir de T dans notre système déductif. Le théorème d'existence du modèle dit que pour toute théorie du premier ordre T avec un langage bien ordonné,

si est syntaxiquement cohérent, alors a un modèle.

Une autre version, avec des liens avec le théorème de Löwenheim-Skolem , dit :

Chaque théorie du premier ordre dénombrable et cohérente sur le plan syntaxique a un modèle fini ou dénombrable.

Étant donné le théorème de Henkin, le théorème de complétude peut être prouvé comme suit : Si , alors n'a pas de modèles. Par la contraposée du théorème de Henkin, alors est syntaxiquement incohérent. Donc une contradiction ( ) est prouvable dans le système déductif. D'où , et ensuite par les propriétés du système déductif, .

Comme théorème de l'arithmétique

Le théorème d'existence du modèle et sa preuve peuvent être formalisés dans le cadre de l'arithmétique de Peano . Précisément, on peut définir systématiquement un modèle de toute théorie effective du premier ordre cohérente T en arithmétique de Peano en interprétant chaque symbole de T par une formule arithmétique dont les variables libres sont les arguments du symbole. (Dans de nombreux cas, nous devrons supposer, comme hypothèse de la construction, que T est cohérent, puisque l'arithmétique de Peano peut ne pas prouver ce fait.) Cependant, la définition exprimée par cette formule n'est pas récursive (mais est, en général , Δ 2 ).

Conséquences

Une conséquence importante du théorème de complétude est qu'il est possible d' énumérer de manière récursive les conséquences sémantiques de toute théorie efficace du premier ordre, en énumérant toutes les déductions formelles possibles à partir des axiomes de la théorie, et de les utiliser pour produire une énumération de leurs conclusions. .

Cela contraste avec le sens direct de la notion de conséquence sémantique, qui quantifie sur toutes les structures dans un langage particulier, qui n'est clairement pas une définition récursive.

Aussi, il fait du concept de "prouvabilité", et donc de "théorème", un concept clair qui ne dépend que du système d'axiomes choisi de la théorie, et non du choix d'un système de preuve.

Relation avec les théorèmes d'incomplétude

Les théorèmes d'incomplétude de Gödel montrent qu'il existe des limites inhérentes à ce qui peut être prouvé dans une théorie mathématique du premier ordre donnée. L'"incomplétude" dans leur nom fait référence à une autre signification de complet (voir la théorie des modèles - Utilisation des théorèmes de compacité et de complétude ) : Une théorie est complète (ou décidable) si chaque phrase dans la langue de est soit prouvable ( ) soit réfutable ( ) .

Le premier théorème d'incomplétude stipule que tout ce qui est cohérent , efficace et contient l' arithmétique de Robinson (" Q ") doit être incomplet dans ce sens, en construisant explicitement une phrase qui n'est manifestement ni démontrable ni réfutable à l'intérieur de . Le deuxième théorème d'incomplétude étend ce résultat en montrant que peut être choisi pour qu'il exprime la cohérence de lui - même.

Puisque ne peut pas être réfuté dans , le théorème de complétude implique l'existence d'un modèle de dans lequel est faux. En fait, est une phrase Π 1 , c'est-à-dire qu'elle déclare qu'une certaine propriété finitiste est vraie pour tous les nombres naturels ; donc s'il est faux, alors un nombre naturel est un contre-exemple. Si ce contre-exemple existait dans les nombres naturels standard, son existence serait réfutée à l' intérieur ; mais le théorème d'incomplétude a montré que cela était impossible, donc le contre-exemple ne doit pas être un nombre standard, et donc tout modèle de dans lequel est faux doit inclure des nombres non standard .

En fait, le modèle de toute théorie contenant Q obtenu par la construction systématique du théorème d'existence du modèle arithmétique, est toujours non standard avec un prédicat de provabilité non équivalent et une manière non équivalente d'interpréter sa propre construction, de sorte que cette construction est non récursif (car les définitions récursives seraient sans ambiguïté).

De plus, si est au moins légèrement plus fort que Q (par exemple s'il inclut l'induction pour les formules existentielles bornées), alors le théorème de Tennenbaum montre qu'il n'a pas de modèles non standard récursifs.

Relation avec le théorème de compacité

Le théorème de complétude et le théorème de compacité sont deux pierres angulaires de la logique du premier ordre. Bien qu'aucun de ces théorèmes ne puisse être prouvé de manière totalement efficace , chacun peut être efficacement obtenu à partir de l'autre.

Le théorème de compacité dit que si une formule φ est une conséquence logique d'un ensemble (éventuellement infini) de formules Γ alors c'est une conséquence logique d'un sous-ensemble fini de Γ. C'est une conséquence immédiate du théorème de complétude, car seul un nombre fini d'axiomes de Γ peut être mentionné dans une déduction formelle de , et la solidité du système déductif implique alors que φ est une conséquence logique de cet ensemble fini. Cette preuve du théorème de compacité est à l'origine due à Gödel.

Inversement, pour de nombreux systèmes déductifs, il est possible de prouver le théorème de complétude comme conséquence effective du théorème de compacité.

L'inefficacité du théorème de complétude peut être mesurée à la manière des mathématiques inversées . Lorsqu'ils sont considérés sur un langage dénombrable, les théorèmes de complétude et de compacité sont équivalents et équivalents à une forme de choix faible connue sous le nom de lemme de König faible , avec l'équivalence prouvable en RCA 0 (une variante du second ordre de l'arithmétique de Peano restreinte à l'induction sur Σ 0 1 formules). Le lemme de König faible est prouvable dans ZF, le système de la théorie des ensembles de Zermelo-Fraenkel sans axiome de choix, et donc les théorèmes de complétude et de compacité pour les langages dénombrables sont prouvables dans ZF. Cependant, la situation est différente lorsque le langage est de grande cardinalité arbitraire depuis lors, bien que les théorèmes de complétude et de compacité restent prouvablement équivalents dans ZF, ils sont également prouvablement équivalents à une forme faible de l' axiome de choix connu sous le nom de lemme de l'ultrafiltre . En particulier, aucune théorie étendant ZF ne peut prouver les théorèmes de complétude ou de compacité sur des langages arbitraires (éventuellement innombrables) sans prouver également le lemme de l'ultrafiltre sur un ensemble de même cardinal.

La complétude dans d'autres logiques

Le théorème de complétude est une propriété centrale de la logique du premier ordre qui ne s'applique pas à toutes les logiques. La logique du second ordre , par exemple, n'a pas de théorème de complétude pour sa sémantique standard (mais a la propriété de complétude pour la sémantique Henkin ), et l'ensemble des formules logiquement valides en logique du second ordre n'est pas récursivement énumérable. Il en est de même pour toutes les logiques d'ordre supérieur. Il est possible de produire des systèmes déductifs solides pour des logiques d'ordre supérieur, mais aucun système de ce type ne peut être complet.

Le théorème de Lindström stipule que la logique du premier ordre est la logique la plus forte (sous réserve de certaines contraintes) satisfaisant à la fois la compacité et l'exhaustivité.

Un théorème de complétude peut être prouvé pour la logique modale ou la logique intuitionniste par rapport à la sémantique de Kripke .

Preuves

La preuve originale de Gödel du théorème a procédé en réduisant le problème à un cas particulier pour les formules dans une certaine forme syntaxique, puis en traitant cette forme avec un argument ad hoc .

Dans les textes logiques modernes, le théorème de complétude de Gödel est généralement prouvé avec la preuve de Henkin , plutôt qu'avec la preuve originale de Gödel. La preuve de Henkin construit directement un modèle de terme pour toute théorie cohérente du premier ordre. James Margetson (2004) a développé une preuve formelle informatisée en utilisant le prouveur du théorème d' Isabelle . D'autres preuves sont également connues.

Voir également

Lectures complémentaires

  • Gödel, K (1929). "Über die Vollständigkeit des Logikkalküls" . Dissertation doctorale. Université de Vienne. Citer le journal nécessite |journal=( aide ) La première preuve du théorème de complétude.
  • Gödel, K (1930). "Die Vollständigkeit der Axiome des logischen Funktionenkalküls". Monatshefte für Mathematik (en allemand). 37 (1) : 349-360. doi : 10.1007/BF01696781 . JFM  56.0046.04 . S2CID  123343522 . Le même matériel que la thèse, sauf avec des preuves plus brèves, des explications plus succinctes et en omettant la longue introduction.

Liens externes