En logique mathématique, le théorème de complétude du calcul des prédicats du premier ordre dresse une correspondance entre la sémantiqueIntuitivement la sémantique est la « signification » des objets et des prédicats du système, par exemple comme ensembles et propriétés sur ces ensembles. On interprète la véracité des propriétés par des valeurs « vrai » et « faux ». et les démonstrations d'un système de déduction en logique du premier ordre.
En termes intuitifs le théorème de complétude construit un pont entre vérité et démontrabilité formelle : tout énoncé vrai est démontrable. Plus précisément le théorème de complétude affirme que si un énoncé est conséquence sémantique d'une théorie que l'on peut décrire dans le formalisme du calcul des prédicats du premier ordre, c'est-à-dire qu'il est vrai dans tous les modèles de cette théorie, alors il est conséquence syntaxique de cette théorie : il existe une démonstration formelle qui déduit cet énoncé à partir des axiomes de la théorie en utilisant les règles d'un système de déduction comme la déduction naturelle, le calcul des séquents ou un système à la Hilbert.
Histoire Le théorème de complétude de la logique du premier ordre a été démontré pour la première fois par Kurt Gödel en 1929 dans sa thèse de doctorat, sur la complétude du calcul logiqueVoir Kurt Gödel, Collected works, vol 1 p. 44 et suivantes.. Leon Henkin a ensuite simplifié la démonstration dans sa thèse The Completeness of Formal Systems (la complétude des systèmes formels) publiée en 1949The Completeness of the First-Order Functional Calculus, Journal of Symbolic Logic 14, 1949, S. 159–166. La preuve de Henkin a ensuite été simplifiée à son tour par Gisbert Hasenjaeger en 1953 Gödel proof..
Diverses formulations équivalentes du théorème de complétude Le théorème de complétude est un méta-théorèmeautrement un théorème dans une méta-théorie à propos des théorèmes d'une théorie donnée, ici le calcul des prédicats du premier ordre qui relie deux concepts : celui de conséquence sémantique et de conséquence syntaxique dans un système de déduction logique.
Systèmes de déduction et validité Le premier concept à définir est donc celui de déduction logique, il dit qu'on peut donner un nombre fini d’axiomes, de schémas d’axiomes ou de règles d'inférence pour décrire ou formaliser la partie purement logique de la déduction, autrement dit toutes les démonstrations qui sont décrites en des étapes élémentaires de raisonnement sont obtenues à partir de ces principes.
La validité logique d’un axiome, d'un schéma d'axiomes ou d'une règle d'inférence est garantie par des modèles. Ainsi, une règle de déduction est valide lorsque tout modèle de ses prémisses est aussi un modèle de sa conclusion. Un axiome logique est valide lorsqu’il est vrai dans tous les modèles. Un schéma d’axiomes est un principe logique valide lorsque tous les axiomes produits par ce schéma sont des axiomes logiques valides. Un système de principes logiques est valide ou correct lorsque ses axiomes, ses schémas d’axiomes et ses règles de déduction sont valides. Une preuve est logiquement valide lorsqu’elle peut être formalisée dans le cadre d’un système logique valide.
Nous allons prouver que la déduction naturelle est un système complet des principes de la logique du premier ordre. Ce théorème est équivalent à celui de Gödel. Mais la preuve de Gödel est basée sur une autre formulation des principes logiques, celle des Principia Mathematica de Whitehead et Russell.
Quelques définitions Pour cela, donnons quelques définitions : celles relatives à l'utilisation de modèles (du premier ordre) : satisfaisabilité et falsifiabilité, loi logique et contradiction logique, conséquence logique, prouvabilité :
celles relatives aux systèmes de déduction (pour le calcul des prédicats du premier ordre) : cohérence et incohérence, prouvabilité :
Notons ⊥ la contradiction. Si elle ne fait pas partie du langage on peut la définir par q∧¬q pour une formule close arbitraire q. Un ensemble de formules T est cohérent dans L lorsqu'il existe une formule q qui n’est pas prouvable à partir de T dans L, ou de façon équivalente en logique classique, si la contradiction n'est pas prouvable à partir de T, ce qu'on note T⊬⊥. Un ensemble de formules T est incohérent ou contradictoire dans L lorsque toutes les formules sont prouvables à partir de T dans L, ou de façon équivalente en logique classique, si la contradiction est prouvable à partir de T, ce qu'on note T⊢⊥.
Un système de déduction correct se doit de ne pouvoir prouver, à partir de formules vraies, que des propositions vraies, en particulier, on attend que, si ⊢p alors ⊨p. Nous montrerons dans le paragraphe suivant que tel est le cas pour la déduction naturelle, ou un système équivalent, tel le calcul des séquents.
La complétude
Le théorème de complétude se préoccupe de la réciproque de la correction. Cela signifie que le système de déduction L se doit d'être suffisamment complet de façon à être capable de démontrer toute loi logique, c'est-à-dire toute formule vraie dans tout modèle. Le théorème de complétude peut être énoncé sous la forme suivante (exprimée pour une formule, une forme plus forte du théorème de complétude s'écrit pour un nombre éventuellement infini de formules) :
Il existe des systèmes de déduction logiques valides L qui satisfont aux conditions équivalentes suivantes :
pour toutes formules p et q (du calcul des prédicats du premier ordre), si q est une conséquence logique de p alors q est prouvable à partir de p dans L. Si p⊨q alors p⊢q, pour toute formule p, si p est une loi logique alors p est prouvable. Si ⊨p alors ⊢p, pour toute formule p, si p est une contradiction logique alors (non p) est prouvable. Si ⊨¬p, alors ⊢¬p, pour toute formule p, si p est une contradiction logique alors p est incohérente dans L. Si ⊨¬p, alors p⊢⊥, pour toute formule p, si p est cohérente dans L alors p est satisfaisable. Si p⊬⊥ alors ⊭¬p.
On peut enfin remarquer qu'un ensemble défini par induction avec un nombre fini de principes (axiomes, schémas d'axiomes et règles de déduction) est énumérable. Autrement dit, toutes les théories axiomatiques usuelles sont des ensembles énumérables. Le théorème de complétude dit qu'il existe des théories axiomatiques complètes de la logique du premier ordre.
Il en résulte que l'ensemble des lois logiques est énumérable.
Cela permet de relier ce théorème de complétude à la théorie de l'indécidabilité, parce qu'on peut prouver que l'ensemble des lois logiques est indécidable. Autrement dit, l'ensemble des formules falsifiables n'est pas énumérable, ou, de façon équivalente, l'ensemble des formules satisfaisables n'est pas énumérable (voir également le théorème d'incomplétude et le théorème de Tarski).
La validité du calcul des prédicats du premier ordre Un système de déduction pour le calcul des prédicats étant choisi, on montre que si une formule p est déductible, avec les règles de ce système à partir d'un ensemble T de formules (T⊢p), alors p est une conséquence sémantique de T, c’est-à-dire conséquence logique au sens de la théorie des modèles, voir ci-dessus (on note, pour distinguer de la notion précédente, T⊨p).
La preuve se fait par récurrence sur la taille des preuves, taille que l'on définit pour chaque système de déduction. Il s'agit alors de vérifier que chaque axiome logique est valide, et que chaque règle conserve la validité. La preuve est triviale, mais fastidieuse à rédiger entièrement.
Précisons un peu le cas de la déduction naturelle : il est plus commode d'utiliser une formulation de celle-ci en termes de séquents (ayant un nombre fini de prémisses et une conclusion).
Il faudrait manipuler des formules avec variables libres. Pour simplifier (l'idée est la même) faisons comme si nous étions en calcul propositionnel, c’est-à-dire que toutes les formules sont closes, il n'y a pas de quantificateurs. Un séquent est valide lorsque tout modèle de ses prémisses est aussi un modèle de sa conclusion.
Un séquent est prouvable s'il est ou bien un axiome, ou bien déduit des axiomes par un nombre fini d'applications des règles de la déduction naturelle. Les axiomes sont ici tous les séquents de la forme p⊢p où p est une formule du calcul des prédicats. Comme on a de manière évidente p⊨p, les axiomes sont valides. On peut alors montrer, à partir de la définition de la vérité des formules complexes (voir théorie des modèles), qu'en partant de séquents valides, on ne peut déduire que des séquents valides si on applique une des règles de la déduction naturelle des séquents. On montre alors par induction sur la structure des preuves (essentiellement, c'est une récurrence sur la hauteur des preuves en tant qu'arbre) que tous les séquents prouvables sont valides.
Par exemple, supposons que l'on ait prouvé T⊢p∧q par introduction du connecteur logique ∧ (et). Cela signifie qu'auparavant, on a prouvé T⊢p et T⊢q. Par induction, on a T⊨p et T⊨q. Dans tout modèle rendant les formules de T vraies, p est vrai et q est vraie. Donc p∧q est vraie, et on a bien T⊨p∧q.
En appliquant la même vérification à tous les séquents, on prouve que, si T⊢p, alors T⊨p.
Pour en déduire que les formules prouvables (⊢p) sont des lois logiques (⊨p). Il suffit de prendre T vide.
Démonstration de Henkin Dans cette section, nous donnons les idées principales de la démonstration du théorème de complétude du premier ordre par Leon Henkin. Nous démontrons la reformulation suivante du théorème de complétude : La démonstration comprend deux étapes : Nous ajoutons des formules à T afin que T soit complète (toute formule ou sa négation est dans T) et T est dite de Henkin, c'est-à-dire que si T contient une formule de la forme alors T doit aussi contenir une formule où c est une constante fraîche ; Nous construisons un modèle « syntaxique » où les éléments du domaine sont les termes.
L'existence d'un modèle sous l'hypothèse de cohérence
Nous allons prouver le théorème de complétude sous la forme suivante.
En fait nous prouverons une version renforcée de ce théorème.
Un ensemble d'axiomes est cohérent lorsqu'aucune contradiction n'est prouvable à partir d'un nombre quelconque, fini, de ces axiomes. Il est satisfaisable lorsqu'il y a un modèle dans lequel les axiomes sont tous vrais. Cette version renforcée du théorème est utile en particulier pour énoncer le paradoxe de Skolem, parce qu’elle permet d’appliquer le théorème de complétude à des systèmes infinis d’axiomes.
Commençons par montrer comment remplacer un système d’axiomes du calcul des prédicats par un système équivalent d’axiomes du calcul des propositions. Pour cela, on commence par mettre chaque axiome sous une forme prénexe.
Une formule du calcul des prédicats est toujours équivalente à une formule mise sous forme prénexe, c’est-à-dire une formule dans laquelle tous les quantificateurs universels et existentiels sont placés au début et non à l'intérieur des sous-formules. On peut toujours prouver qu'une formule est équivalente à une formule prénexe avec les règles de déduction suivante : de (∃x p)∧q déduire ∃x(p∧q), pourvu que q ne contienne pas x comme variable libre. (Si elle la contient, il suffit de substituer à x dans ∃x p une autre variable qui n'apparaît pas dans q). de (∃x p)∨q déduire ∃x(p∨q), pourvu également que q ne contienne pas x comme variable libre. deux autres règles semblables pour le quantificateur universel ∀. de ¬(∃x p) déduire ∀x(¬p). de ¬(∀x p) déduire ∃x(¬p).
Toutes ces règles sont des règles dérivées dans le système de déduction naturelle et elles font toutes passer d'une prémisse à une conclusion équivalente. Par itération elles fournissent une formule prénexe équivalente à la formule initiale.