Cohérence (logique)

Un article de Wikipédia, l'encyclopédie libre.
Aller à : navigation, rechercher

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 à un système de déduction, soit par référence à la sémantique du langage de la théorie.

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é la théorie, de façon équivalente par le principe d'explosion quand la théorie n'a pas de contradiction : à 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, qui interprète les termes du langage dans lequel la théorie est exprimé, et dans laquelle tous les énoncés de la théorie sont « satisfaits », c'est-à-dire « vrais » dans cette structure.

Le théorème de correction lie ces deux définition en indiquant qu'une théorie cohérente au sens sémantique est cohérente au sens syntaxique : 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 calcul des prédicats du premier ordre en logique classique.

Approches syntaxiques et sémantiques[modifier | modifier le code]

L’absence de contradiction peut être abordé et définie de deux manières :

  1. 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 signature pour une assignation de valeur de vérité) pour désigner ce concept.
  2. 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 permettent, à 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.[citation nécessaire]

Cohérence et complétude en arithmétique[modifier | modifier le code]

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.

Cohérence et complétude[modifier | modifier le code]

Définitions[modifier | modifier le code]

Une théorie du premier ordre est vue dans ce qui suit comme un ensemble de formules logiques closes d'un certain langage L de la logique du premier ordre. Une définition très générale de la cohérence (ou consistance), au sens de la déduction, la définition dite « syntaxique » de la cohérence, est la suivante :

  • une théorie dans le langage L est cohérente (cohérente au sens de Post[réf. nécessaire] ou absolument cohérente[réf. nécessaire]) quand il existe une formule du langage L qui n'est pas conséquence de la théorie.

Si le langage possède une négation et si la logique admet pour principe que d'une contradiction (une formule et sa négation) on peut déduire n'importe quelle formule (c'est le cas en logique classique, en logique intuitionniste, ...), alors cette définiton équivaut à la suivante :

  • une théorie dans le langage L est cohérente quand il n'existe aucune formule du langage L telle qu'elle même et sa négation soient toutes deux conséquences de la théorie.

Une théorie qui n'est pas cohérente est dite incohérente ou contradictoire.

Il est par contre tout à fait possible étant donnés une théorie cohérente T et une formule F dans le même langage, que T n'ait pour conséquence ni la formule F ni sa négation.

Saturation[modifier | modifier le code]

Dans le cadre de la démonstration du théorème de complétude de la logique du premier ordre (classique), c'est-à-dire le fait qu'une théorie cohérente (au sens de la déduction) possède un modèle, il peut être commode d'introduire les définitions suivantes.

  • Une théorie T du langage L est maximalement cohérente, quand l'ajout à la théorie T d'une formule close quelconque de L qui n'est pas dans T conduit à une théorie T ∪ {F} incohérente.
  • Une théorie T admet des témoins de Henkin, ou est saturée par témoins de Henkin, quand pour toute formule à une variable libre F de L, il existe une constance c du langage L (le témoin de Henkin associé à F) telle que, en notant x la variable libre dans F, la théorie T a pour conséquence la formule ∃x FF[c/x] (où F[c/x] désigne la formule obtenue à partir de F en substituant la constante c à la variable x).

Complétude[modifier | modifier le code]

Le théorème de complétude peut alors se démontrer en deux temps :

  • une théorie T dans un langage L est contenue dans une théorie T' d'un langage L', qui est maximalement cohérente et saturée par témoins de Henkin ;
  • une théorie maximalement cohérente et saturée par témoins de Henkin est complète.

Pour la première partie, le langage L' s'obtient en ajoutant au langage L « suffisamment » de nouvelles constantes (un ensemble dénombrable de constantes si le langage d'origine est de signature finie ou dénombrable), les constantes étant associées bijectivement aux formules à une variable libre du langage d'arrivée L'. Ces constantes sont les témoins de Henkin des formules correspondante, la théorie est d'abord augmentée des axiomes correspondant, puis saturée pour donner une extension maximalement cohérente (dans le cas le plus général, le lemme de Zorn est utile, dans le cas dénombrable, on peut utiliser une définition par induction). Il est également possible de saturer epar témoins de Henkin en même temps que de construire l'extension maximalement cohérente, l'important étant que pour toute formule ∃x F démontrable, on dispose d'un témoin c et que F[c/x] soit conséquence de la théorie obtenue (ou de façon équivalente, pour toute formule universelle ∀x F non démontrable on dispose d'un témoin c et que la négation ¬ F[c/x] soit conséquence de la théorie obtenue).

La seconde partie se démontre, dans le cas d'un langage du premier ordre sans égalité, en prenant pour ensemble de base du modèle les termes clos du langage (langage qui a été augmenté des témoins de Henkin dans la première étape). Pour un langage égalitaire, il est nécessaire de quotienter l'ensemble des termes par les relations d'égalité entre termes clos qui se déduisent de la théorie.

Voir aussi[modifier | modifier le code]

Notes et références[modifier | modifier le code]


Références[modifier | modifier le code]