Complétude (logique)
En logique mathématique et métalogique, un système formel est dit complet par rapport à une propriété particulière si chaque formule possédant cette propriété peut être prouvée par une démonstration formelle à l'aide de ce système, c'est-à -dire par l'un de ses théorèmes ; autrement, le système est dit incomplet. Le terme « complet » est également utilisé sans qualification, avec des significations différentes selon le contexte, la plupart du temps se référant à la propriété de la validité sémantique. Intuitivement, dans ce sens particulier, un système est dit complet si toute formule vraie y est démontrable. Kurt Gödel, Leon Henkin et Emil Leon Poster ont tous publié des preuves de complétude. (Voir la thèse de Church-Turing.)
Autres propriétés relatives à la complétude
La propriété réciproque de la complétude est appelée la correction, ou la cohérence : un système est correct par rapport à une propriété (principalement la validité sémantique) si chacun de ses théorèmes possède cette propriété.
Formes de complétudes
Complétude expressive
Un langage formel est expressivement complet s'il peut exprimer le but pour lequel il est destiné.
Complétude fonctionnelle
Un ensemble de connecteurs logiques associés à un système formel est fonctionnellement complet si elle peut exprimer toutes les fonctions propositionnelles.
Complétude sémantique
La complétude sémantique est la réciproque de la correction des systèmes formels. Un système formel est dit correct pour une sémantique quand toute formule dérivable par les règles de ce système est vraie pour toutes les interprétations possibles dans la sémantique considérée. La propriété réciproque est appelée complétude (sémantique) du système formel, à savoir :
- si ⊨ φ, alors ⊢S φ[1].
Par exemple, le théorème de complétude de Gödel établit la complétude sémantique pour la logique du premier ordre, mais il établit cette complétude également en un sens plus fort, décrit au paragraphe suivant.
Complétude sémantique forte
Un système formel S est fortement complet ou complet au sens fort, vis-à -vis d'une certaine sémantique, si pour tout ensemble de prémisses Γ (éventuellement infini), n'importe quelle formule φ qui se déduit sémantiquement de Γ (c'est-à -dire que tout modèle de Γ est modèle de φ) est dérivable à partir de formules de Γ dans le système formel considéré. À savoir :
- si Γ ⊨ φ, alors Γ ⊢S φ.
Complétude déductive
Un système formel S est dit déductivement complet si pour chaque proposition (formule close) φ du langage, soit φ soit ¬φ, est démontrable dans S. De façon la plupart du temps équivalente, un système formel est dit déductivement complet quand aucune proposition indémontrable ne peut être ajoutée à celui-ci sans introduire une incohérence. La complétude déductive est plus forte que la complétude sémantique. La logique propositionnelle et la logique des prédicats du premier ordre classiques sont sémantiquement complètes, mais pas déductivement complètes (par exemple, Si A est une variable propositionnelle, ni A, ni sa négation ne sont des théorèmes). Le théorème d'incomplétude de Gödel montre que tout système déductif récursif suffisamment puissant, comme l'arithmétique de Peano, ne peut pas être à la fois cohérent et syntaxiquement complet.
Références
- (en) Geoffrey Hunter, Metalogic: An Introduction to the Metatheory of Standard First-Order Logic, University of California Press, (1re Ă©d. 1971) (lire en ligne), p. ?.