Cohérence (logique)
From Wikipedia, the free encyclopedia
Cet article est une ébauche concernant les mathématiques et la logique.
Certaines informations figurant dans cet article ou cette section devraient être mieux reliées aux sources mentionnées dans les sections « Bibliographie », « Sources » ou « Liens externes » ().
En logique mathématique, la cohérence, ou consistance, d'une théorie axiomatique peut se définir de deux façons, soit par référence à la déduction : il n'est pas possible de tout démontrer à partir des axiomes de la théorie, soit par référence à la sémantique de la théorie : celle-ci possède des réalisations qui lui donnent un sens.
La première définition est syntaxique au sens où elle utilise des déductions ou démonstrations, qui sont des objets finis. Une théorie est dite dans ce sens cohérente ou consistante quand elle n'a pas pour conséquence tous les énoncés du langage dans lequel est exprimée la théorie, ou, de façon équivalente (car d'une contradiction on déduit n'importe quoi), quand elle ne permet pas de démontrer à la fois un énoncé et sa négation. Une telle théorie est dite également non-contradictoire.
La seconde définition utilise la théorie des modèles : une théorie est cohérente quand elle possède un modèle, soit une structure mathématique dans laquelle s'interprètent les termes du langage, et qui satisfait tous les axiomes de la théorie, dit autrement il existe une structure telle que tous les axiomes de la théorie sont vrais dans cette structure.
Ces deux définitions sont équivalentes par le théorème de correction et le théorème de complétude. Le premier a pour conséquence que tous les énoncés démontrables d'une théorie sont satisfaits par une structure qui satisfait les axiomes, et donc une théorie cohérente au sens sémantique est cohérente au sens syntaxique, car une structure ne peut satisfaire à la fois un énoncé et sa négation. Le théorème de complétude indique qu'une théorie cohérente au sens syntaxique possède un modèle, c'est-à-dire qu'elle est cohérente au sens sémantique. Ces deux théorèmes se démontrent en logique classique, en calcul des prédicats du premier ordre.
L’absence de contradiction peut être abordé et définie de deux manières :
- d’un point de vue sémantique : on considère qu’une théorie est cohérente si elle possède un modèle, c’est-à-dire s’il existe une interprétation sous laquelle toutes les formules de la théorie sont vraies. C’est le sens qui lui est donné en logique classique et dans le développement du théorème de complétude, cependant la logique mathématique contemporaine utilise le terme de satisfaisable (d'une théorie pour une assignation de valeur de vérité sur sa signature) pour désigner ce concept ;
- d’un point de vue syntaxique : on considère que la théorie est cohérente s'il n’y a aucune formule P telle que P et sa négation non-P, également noté ¬P, soient toutes deux prouvables à partir des axiomes de la théorie en utilisant le système déductif qui lui est associé. C’est-à-dire qu’aucune combinaison des règles qu’on se donne ne permet, à partir des formules de départ, d’obtenir et P et non-P.
Si ces définitions sémantique et syntaxique sont équivalentes pour une logique donnée, ce système logique est dit complet.[réf. nécessaire]
Cohérence et complétude en arithmétique
Une preuve de cohérence est une preuve mathématique qu'une théorie donnée est cohérente. La théorie de la démonstration a été initiée par David Hilbert dans le but de fournir des preuves finitaires de cohérence pour les théories mathématiques dans le cadre de son programme dit programme de Hilbert. Les preuves de cohérence étudiées dans ce cadre sont syntaxiques, une démonstration sémantique de cohérence, dès qu'elle met en jeu un modèle infini, est par nature non finitaire.
Mais ce programme est remis en cause par les théorèmes d’incomplétude, en particulier le second selon lequel une théorie récursivement axiomatisable cohérente, dès qu'elle permet de faire suffisamment d'arithmétique, ne permet pas de démontrer sa propre cohérence. C'est le cas de théories comme l’arithmétique récursive primitive (en) (candidate à être une théorie pour développer les preuves finitaires), l’arithmétique de Peano, la théorie des ensembles ZFC... Il existe cependant des théories arithmétiques cohérentes faibles, comme l’arithmétique de Presburger, un système axiomatique pour les nombres entiers munis de l’addition, qui sont complètes.
