Cohérence

En logique déductive classique , une théorie cohérente est celle qui ne conduit pas à une contradiction logique . Une théorie est cohérente s'il n'existe pas de formule telle que et sa négation soient des éléments de l'ensemble des conséquences de . Soit un ensemble de phrases fermées (officieusement « axiomes ») et l'ensemble des phrases fermées prouvables à partir d'un système déductif formel (spécifié, éventuellement implicitement). L'ensemble des axiomes est cohérent lorsqu'il n'existe pas de formule telle que et . Une théorie triviale (c'est-à-dire une théorie qui prouve chaque phrase dans le langage de la théorie) est clairement incohérente. Inversement, dans un système formel explosif (par exemple, les logiques propositionnelles ou du premier ordre classiques ou intuitionnistes), toute théorie incohérente est triviale. La cohérence d'une théorie est une notion syntaxique , dont la contrepartie sémantique est la satisfiabilité . Une théorie est satisfiable si elle possède un modèle , c'est-à-dire s'il existe une interprétation selon laquelle tous les axiomes de la théorie sont vrais. C'est ce que signifiait le terme cohérent dans la logique aristotélicienne traditionnelle , bien que dans la logique mathématique contemporaine, le terme satisfiable soit utilisé à la place.

Dans un système formel sain , toute théorie satisfaisable est cohérente, mais l'inverse n'est pas vrai. S'il existe un système déductif pour lequel ces définitions sémantiques et syntaxiques sont équivalentes pour toute théorie formulée dans une logique déductive particulière , la logique est dite complète . La complétude du calcul propositionnel a été prouvée par Paul Bernays en 1918 et Emil Post en 1921, tandis que la complétude du calcul des prédicats (du premier ordre) a été prouvée par Kurt Gödel en 1930, et des preuves de cohérence pour l'arithmétique restreinte par rapport au schéma d'axiomes d'induction ont été prouvées par Ackermann (1924), von Neumann (1927) et Herbrand (1931). Des logiques plus fortes, telles que la logique du second ordre , ne sont pas complètes.

Une preuve de cohérence est une preuve mathématique qu'une théorie particulière est cohérente. Le développement précoce de la théorie de la preuve mathématique a été motivé par le désir de fournir des preuves de cohérence finitaire pour toutes les mathématiques dans le cadre du programme de Hilbert . Le programme de Hilbert a été fortement influencé par les théorèmes d'incomplétude , qui ont montré que des théories de preuve suffisamment solides ne peuvent pas prouver leur cohérence (à condition qu'elles soient cohérentes).

Bien que la cohérence puisse être prouvée à l'aide de la théorie des modèles, elle est souvent réalisée de manière purement syntaxique, sans qu'il soit nécessaire de faire référence à un modèle de la logique. L' élimination des coupures (ou de manière équivalente la normalisation du calcul sous-jacent s'il y en a un) implique la cohérence du calcul : comme il n'y a pas de preuve de fausseté sans coupure, il n'y a pas de contradiction en général.

Dans les théories arithmétiques, comme celle de Peano , il existe une relation complexe entre la cohérence de la théorie et son exhaustivité . Une théorie est complète si, pour chaque formule φ dans son langage, au moins l'une des φ ou ¬φ est une conséquence logique de la théorie.

L'arithmétique de Presburger est un système d'axiomes pour les nombres naturels additionnés. Il est à la fois cohérent et complet.

Les théorèmes d'incomplétude de Gödel montrent qu'aucune théorie arithmétique suffisamment solide et récursivement dénombrable ne peut être à la fois complète et cohérente. Le théorème de Gödel s'applique aux théories de l'arithmétique de Peano (PA) et de l'arithmétique récursive primitive (PRA), mais pas à l'arithmétique de Presburger .

De plus, le deuxième théorème d'incomplétude de Gödel montre que la cohérence de théories arithmétiques récursivement énumérables suffisamment fortes peut être testée d'une manière particulière. Une telle théorie est cohérente si et seulement si elle ne prouve pas une phrase particulière, appelée phrase de Gödel de la théorie, qui est une déclaration formalisée de l'affirmation selon laquelle la théorie est effectivement cohérente. Ainsi, la cohérence d'une théorie arithmétique suffisamment forte, récursivement énumérable et cohérente ne peut jamais être prouvée dans ce système lui-même. Le même résultat est vrai pour les théories récursivement énumérables qui peuvent décrire un fragment d'arithmétique suffisamment fort, y compris les théories des ensembles telles que la théorie des ensembles de Zermelo-Fraenkel (ZF). Ces théories des ensembles ne peuvent pas prouver leur propre phrase de Gödel, à condition qu'elles soient cohérentes, ce qui est généralement admis.

Étant donné que la cohérence de ZF n'est pas prouvable dans ZF, la notion la plus faibleLa cohérence relative est intéressante en théorie des ensembles (et dans d'autres systèmes axiomatiques suffisamment expressifs). SiTest unethéorieetAaxiomesupplémentaire,T+Aest cohérent par rapport àT(ou simplement queAest cohérent avecT) si l'on peut prouver que siTest cohérent alorsT+Aest cohérent. SiAet ¬Asont cohérents avecT, alorsAest ditindépendantdeT.

Dans le contexte suivant de la logique mathématique , le symbole du tourniquet signifie « prouvable à partir de ». Autrement dit, il se lit comme suit : b est prouvable à partir de a (dans un système formel spécifié).

• Un ensemble de formules en logique du premier ordre est cohérent (écrit ) s'il n'existe pas de formule telle que et . Sinon, il est incohérent (écrit ).
• simplement cohérent si pour aucune formule de , à la fois et la négation de sont des théorèmes de .
• absolument cohérent ou post-cohérent si au moins une formule du langage de n'est pas un théorème de .
• maximalement cohérent si est cohérent et pour toute formule , implique .
• contenir des témoins si pour toute formule de la forme il existe un terme tel que , où désigne la substitution de chaque dans par un ; voir aussi Logique du premier ordre .

1. Les éléments suivants sont équivalents :
   2. Pour tous
2. Tout ensemble de formules satisfaisable est cohérent, où un ensemble de formules est satisfaisable si et seulement s'il existe un modèle tel que .
3. Pour tous et :
   1. sinon , alors ;
   2. si et , alors ;
   3. si , alors ou .
4. Soit un ensemble de formules maximalement cohérentes et supposons qu'il contienne des témoins . Pour tout et :
   1. si , alors ,
   2. soit ou ,
   4. si et , alors ,

Soit un ensemble de symboles . Soit un ensemble de formules maximalement cohérentes contenant des témoins .

Définissez une relation d'équivalence sur l'ensemble des termes par si , où désigne l'égalité . Soit désigne la classe d'équivalence des termes contenant ; et soit où est l'ensemble des termes basés sur l'ensemble des symboles .

Définir la structure - sur , également appelée terme-structure correspondant à , par :

1. pour chaque symbole de relation -aire , définir si
2. pour chaque symbole de fonction -aire , définissez
3. pour chaque symbole constant , définissez

Définissez une affectation de variable par pour chaque variable . Soit le terme interprétation associé à .

Ensuite pour chaque -formule :

Il y a plusieurs choses à vérifier. Tout d'abord, il s'agit bien d'une relation d'équivalence. Ensuite, il faut vérifier que (1), (2) et (3) sont bien définis. Cela découle du fait qu'il s'agit d'une relation d'équivalence et nécessite également de prouver que (1) et (2) sont indépendants du choix des représentants de classe. Enfin, cela peut être vérifié par induction sur des formules.

Dans la théorie des ensembles ZFC avec la logique classique du premier ordre , une théorie incohérente est une théorie telle qu'il existe une phrase fermée telle que contient à la fois et sa négation . Une théorie cohérente est une théorie telle que les conditions logiquement équivalentes suivantes sont remplies