Cohérence - Consistency

Dans la logique déductive classique , une théorie cohérente est celle qui ne conduit pas à une contradiction logique . L'absence de contradiction peut être définie en termes sémantiques ou syntaxiques . La définition sémantique déclare qu'une théorie est cohérente si elle a un modèle , c'est-à-dire qu'il existe une interprétation selon laquelle toutes les formules de la théorie sont vraies. C'est le sens utilisé dans la logique aristotélicienne traditionnelle , bien que dans la logique mathématique contemporaine le terme satisfiable soit utilisé à la place. La définition syntaxique déclare qu'une théorie est cohérente s'il n'y a pas de formule telle que les deux et sa négation soient des éléments de l'ensemble des conséquences de . Soit un ensemble de phrases fermées (officiellement « axiomes ») et l'ensemble de phrases fermées prouvables à partir d' un système déductif formel (spécifié, peut-être implicitement). L'ensemble des axiomes est cohérent lorsqu'il n'y a pas de formule .

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 . L'exhaustivité du calcul des propositions a été prouvée par Paul Bernays en 1918 et Emil Post en 1921, tandis que l'exhaustivité du calcul des prédicats a été prouvée par Kurt Gödel en 1930, et les preuves de cohérence pour l'arithmétique restreinte par rapport au schéma d'axiome d'induction ont été prouvées par Ackermann (1924), von Neumann (1927) et Herbrand (1931). Les 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 finie pour toutes les mathématiques dans le cadre du programme de Hilbert . Le programme de Hilbert a été fortement impacté par les théorèmes d'incomplétude , qui ont montré que des théories de preuve suffisamment fortes ne peuvent pas prouver leur propre cohérence (à condition qu'elles soient en fait cohérentes).

Bien que la cohérence puisse être prouvée au moyen de la théorie des modèles, elle se fait souvent 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 : puisqu'il n'y a pas de preuve de fausseté sans coupure, il n'y a pas de contradiction en général.

Cohérence et complétude en arithmétique et en théorie des ensembles

Dans les théories de l'arithmétique, telles que l'arithmétique de Peano , il existe une relation complexe entre la cohérence de la théorie et sa complétude . Une théorie est complète si, pour chaque formule φ dans son langage, au moins un de φ ou ¬φ est une conséquence logique de la théorie.

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

Les théorèmes d'incomplétude de Gödel montrent qu'une théorie de l'arithmétique suffisamment forte et récursivement énumérable ne peut pas ê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 de l'arithmétique suffisamment fortes et récursivement énumérables 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 la phrase de Gödel de la théorie, qui est un énoncé formalisé de l'affirmation selon laquelle la théorie est effectivement cohérente. Ainsi, la cohérence d'une théorie de l'arithmétique suffisamment forte, récursivement dénombrable 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 suffisamment fort de l'arithmétique, 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.

Parce que la cohérence de ZF n'est pas prouvable dans ZF, la notion la plus faible la cohérence relative est intéressante en théorie des ensembles (et dans d'autres systèmes axiomatiques suffisamment expressifs). SiTest unethéorieetAest unaxiomesupplémentaire,T+Aest dit cohérent par rapport àT(ou simplement queAest cohérent avecT) s'il peut être prouvé que siTest cohérent alorsT+Aest cohérent. SiAetAsont cohérents avecT, alorsAest ditindépendantdeT.

Logique du premier ordre

Notation

(symbole du tourniquet) dans le contexte suivant de la logique mathématique , signifie "prouvable à partir de". C'est-à-dire, lit : b est prouvable à partir de a (dans un système formel spécifié). Voir Liste des symboles logiques . Dans d'autres cas, le symbole du tourniquet peut signifier implique ; permet la dérivation de. Voir : Liste des symboles mathématiques .

Définition

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

Résultats de base

  1. Les éléments suivants sont équivalents :
    1. Pour tous
  2. Tout ensemble satisfiable de formules est cohérent, où un ensemble de formules est satisfiable 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 au maximum cohérent et supposons qu'il contienne des témoins . Pour tous et :
    1. si , alors ,
    2. soit ou ,
    3. si et seulement si ou ,
    4. si et , alors ,
    5. si et seulement s'il existe un terme tel que .

Le théorème de Henkin

Soit un ensemble de symboles . Soit un ensemble de formules au maximum cohérent contenant des témoins .

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

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

  1. pour chaque symbole de relation -aire , définissez 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é à .

Alors pour chaque -formule :

si et seulement si

Esquisse de la preuve

Il y a plusieurs choses à vérifier. Premièrement, il s'agit en fait 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 une preuve que (1) et (2) sont indépendants du choix des représentants de classe. Enfin, peut être vérifié par induction sur des formules.

Théorie des modèles

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

Voir également

Notes de bas de page

Les références

Liens externes