Complétude (logique)
Cet article ne cite pas suffisamment ses sources ().
Si vous disposez d'ouvrages ou d'articles de référence ou si vous connaissez des sites web de qualité traitant du thème abordé ici, merci de compléter l'article en donnant les références utiles à sa vérifiabilité et en les liant à la section « Notes et références ».
En pratique : Quelles sources sont attendues ? Comment ajouter mes sources ?
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
[modifier | modifier le code]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
[modifier | modifier le code]Complétude expressive
[modifier | modifier le code]Un langage formel est expressivement complet s'il peut exprimer le but pour lequel il est destiné.
Complétude fonctionnelle
[modifier | modifier le code]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
[modifier | modifier le code]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
[modifier | modifier le code]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
[modifier | modifier le code]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.
Complétude structurelle
[modifier | modifier le code]Une logique propositionnelle super-intuitionniste (en) ou modale, est dite structurellement complète quand chaque règle admissible (en) est dérivable.
Références
[modifier | modifier le code]- (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. ?[réf. incomplète].
