En logique déductive , une théorie cohérente est une théorie qui ne conduit pas à une contradiction logique . Une théorie est cohérente s'il n'existe aucune formule telle que et...
Worldlex WikiContenu en francaisLecture gratuite
logique déductive , une théorie cohérente est une théorie qui ne conduit pas à une contradiction logique . Une théorie est cohérente s'il n'existe aucune formule telle que et sa négation appartiennent toutes deux à l'ensemble des conséquences de . Soit un ensemble de propositions closes (appelées informellement « axiomes ») et l'ensemble des propositions closes démontrables à partir de sous un système déductif formel (spécifié, éventuellement implicitement). L'ensemble des axiomes est cohérent lorsqu'il n'existe aucune formule telle que et . Une théorie triviale (c'est-à-dire une théorie qui démontre chaque proposition dans le langage de la théorie) est clairement incohérente. Réciproquement, dans un système formel explosif (par exemple, les logiques propositionnelles classiques ou intuitionnistes, ou les logiques du premier ordre), toute théorie incohérente est triviale. La cohérence d'une théorie est une notion syntaxique , dont le pendant sémantique est la satisfaisabilité . Une théorie est satisfiable si elle possède un modèle , c'est-à-dire s'il existe une interprétation sous laquelle tous les axiomes de la théorie sont vrais. C'est ce que signifiait la cohérence dans la logique aristotélicienne traditionnelle, bien que la logique mathématique contemporaine utilise plutôt le terme satisfiable .
Dans un système formel correct , toute théorie satisfiable est cohérente, mais la réciproque est fausse. 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 , cette logique est dite complète . La complétude du calcul propositionnel a été démontrée par Paul Bernays en 1918 et Emil Post en 1921 , tandis que celle du calcul des prédicats (du premier ordre) a été démontrée par Kurt Gödel en 1930 Les preuves de cohérence pour l'arithmétique restreinte au schéma d'axiomes d'induction ont été démontré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 démonstration mathématique de la cohérence d'une théorie particulière. Les premiers développements de la théorie mathématique de la démonstration ont été motivés par le désir de fournir des preuves de cohérence finitaires pour l'ensemble des mathématiques, dans le cadre du programme de Hilbert . Ce programme a été fortement influencé par les théorèmes d'incomplétude , qui ont montré que des théories de la démonstration suffisamment fortes ne peuvent prouver leur cohérence (à condition qu'elles soient cohérentes).
Bien que la cohérence puisse être démontrée à l'aide de la théorie des modèles, cela 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 façon équivalente, la normalisation du calcul sous-jacent , s'il existe) implique la cohérence du calcul : puisqu'il n'existe aucune preuve de fausseté sans coupure, il n'y a pas de contradiction en général.
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 toute formule φ de son langage, au moins φ 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 muni de l'addition. Elle est à la fois cohérente et complète.
De plus, le second théorème d'incomplétude de Gödel montre que la cohérence des 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 proposition particulière, appelée proposition de Gödel de la théorie, qui formalise l'affirmation que 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 suffisamment fort de l'arithmétique — y compris les théories ensemblistes telles que la théorie des ensembles de Zermelo-Fraenkel (ZF). Ces théories ensemblistes ne peuvent pas prouver leur propre proposition de Gödel — pourvu qu'elles soient cohérentes, ce qui est généralement admis.
Comme la cohérence de ZF n'est pas prouvable dans ZF, la notion plus faibleLa cohérence relative est un concept intéressant en théorie des ensembles (et dans d'autres systèmes axiomatiques suffisamment expressifs). SiTest unethéorieetAaxiomesupplémentaire,on dit queT+AT(ou simplement queAest cohérent avecT) s'il est possible de démontrer que siT,alorsT+AAet ¬Asonttous deuxcohérents avecT, alorsAest ditindépendantdeT.
Logique du premier ordre
logique mathématique , le symbole du tourniquet signifie « démontrable à partir de ». Autrement dit, cela se lit : b est démontrable à partir de a (dans un système formel spécifié).
Définition
Un ensemble de formules en logique du premier ordre est cohérent (noté ) s'il n'existe aucune formule telle que et . Sinon, il est incohérent (noté ).
On dit qu'une formule est simplement cohérente si, pour aucune formule de , et la négation de sont des théorèmes de .On dit qu'un système est absolument cohérent ou post-cohérent si au moins une formule de son langage n'est pas un théorème de ce système .
On dit qu'une formule est maximalement cohérente si elle est cohérente et si, pour toute formule , elle implique .
On dit que contient des témoins si, pour chaque 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 .
Pour tous
Tout ensemble de formules satisfaisables est cohérent, où un ensemble de formules est satisfaisable si et seulement s'il existe un modèle tel que .
Pour tous et :
sinon , alors ;
si et , alors ;
si , alors ou .
Soit un ensemble de formules maximalement cohérent et supposons qu'il contienne des témoins . Pour tout et :
si , alors
soit , soit ,
si et seulement si ou ,
si et , alors
si et seulement s'il existe un terme tel que .ensemble de symboles . Soit un ensemble de -formules maximalement cohérent contenant des témoins .
Définissons une relation d'équivalence sur l'ensemble des termes par si , où désigne l'égalité . Soit la classe d'équivalence des termes contenant ; et soit où est l'ensemble des termes basés sur l'ensemble des symboles .
Définissons la structure - sur , également appelée structure de terme correspondant à , par :
pour chaque symbole de relation -aire , définir si
pour chaque symbole de fonction -aire , définir
pour chaque symbole constant , définir
Définissons une affectation de variable par pour chaque variable . Soit l' interprétation du terme associée à .
Ensuite, pour chaque formule :
si et seulement si
Esquisse de preuve
Plusieurs points sont à vérifier. Premièrement, il faut s'assurer qu'il s'agit bien d'une relation d'équivalence. Ensuite, il est nécessaire de vérifier que (1), (2) et (3) sont bien définies. Ceci découle du fait qu'il s'agit d'une relation d'équivalence et requiert également de démontrer que (1) et (2) sont indépendantes du choix des représentants de classe. Enfin, on peut le vérifier par récurrence sur les formules.
Worldlex Wiki