Théorème de complétude du calcul des propositions
Source: Wikipédia sous licence CC-BY-SA 3.0.
La liste des auteurs de cet article est disponible ici.

Le calcul des propositions est un calcul logique restreint. On emploie souvent le nom de proposition pour désigner une formule logique non quantifiée. Il existe deux façons de valider une formule P du calcul des propositions :

  • ou bien on montre que cette formule est vraie dans tout (Le tout compris comme ensemble de ce qui existe est souvent interprété comme le monde ou l'univers.) modèle (voir ci-dessous). On dit alors que P est une tautologie, et on note \vDash P.
  • ou bien on montre que cette formule est prouvable ou dérivable en utilisant un système de déduction, et on note \vdash P.

Un système de déduction correct doit être construit de façon que, à partir de formules vraies (tautologies), on puisse déduire d'autres formules vraies. Dans ce cas, si \vdash P est vérifié, alors \vDash P l'est également.

Le système de déduction sera complet, si inversement, il permet de déduire toute formule vraie. Autrement dit, si \vDash P est vérifié, le système de déduction doit permettre de prouver qu'on a également \vdash P.

Le théorème (Un théorème est une proposition qui peut être mathématiquement démontrée, c'est-à-dire une assertion qui peut être établie comme vraie au travers d'un...) de complétude (On parle de complétude en mathématiques dans des sens très différents. On dit d'un objet mathématiques qu'il est complet pour exprimer que rien ne...) du calcul des propositions (Le calcul des propositions ou calcul propositionnel, dont le fondateur fut le logicien allemand Frege, version moderne de la logique stoïcienne, est une théorie logique qui définit les lois formelles du raisonnement. La notion de...) énonce que les systèmes de déduction, décrits dans les articles calcul des propositions ou déduction naturelle (La déduction naturelle est une façon d'exposer les principes de la logique du premier ordre pour les rendre aussi proches que possible des façons naturelles de raisonner) ou calcul des séquents (En 1935 Gentzen a proposé la déduction naturelle, un formalisme pour décrire les preuves du calcul des prédicats, dont l'idée était de coller au plus près à la...), sont complets. Il y a équivalence entre être une tautologie et être prouvable.

Ce théorème a été prouvé par Paul Bernays en 1926.

Vérité et fausseté d'une proposition dans un modèle

Pour le calcul des propositions, il n’est pas nécessaire d’analyser la structure des formules atomiques en prédicats et objets. La seule propriété des propositions atomiques qui compte dans les calculs de la logique (La logique (du grec logikê, dérivé de logos (λόγος), terme inventé par Xénocrate signifiant...) classique est leur vérité ou leur fausseté. On peut représenter les propositions par des lettres, p, q, r, ... et les concevoir comme des variables qui peuvent recevoir deux valeurs, V pour vrai, et F pour faux.

Un modèle est défini par l’attribution de valeurs de vérité, V ou F, aux propositions atomiques. Par exemple (p = V,q = F,r = V) désigne le modèle \mathcal M dans lequel il y a trois propositions atomiques p, q, et r, la seconde ( Seconde est le féminin de l'adjectif second, qui vient immédiatement après le premier ou qui s'ajoute à quelque chose de nature identique. La seconde est une unité de mesure du temps. La seconde d'arc est une mesure d'angle...) étant fausse et les deux autres vraies.

On peut définir un calcul des vérités semblable au calcul des nombres et utilisant les connecteurs logiques non \lnot, et \land, ou \lor, implique \to. Ses axiomes sont données (Dans les technologies de l'information (TI), une donnée est une description élémentaire, souvent codée, d'une chose, d'une transaction d'affaire, d'un événement, etc.) par les tables de vérité suivantes :

\lnot V = F, \lnot F = V
V \land V= V, V \land F = F \land V = F \land F = F

Les règles relatives à \lor et \to s'en déduisent en posant :

P \lor Q = \lnot(\lnot P \land \lnot Q)
P \to Q = \lnot P \lor Q

On peut alors calculer, par exemple, que dans le modèle \mathcal M défini par p = F :

\lnot(p \land \lnot p) = \lnot(F \land \lnot F) = \lnot(F \land V) = \lnot F = V

On en conclut que \lnot(p \land \lnot p) est vraie dans le modèle p = F. On montre de même qu'elle est aussi vraie dans le modèle p = V et puisqu’elle ne contient que p comme proposition atomique, elle est vraie dans tous les modèles et est donc une tautologie.

Preuve du théorème de complétude

Systèmes de déduction

On peut montrer que les systèmes de déduction cités en préambule permettent en particulier d'effectuer les déductions suivantes :

\vdash P \to P (identité), \vdash \lnot P \lor P (principe du tiers exclu), \vdash P \to \lnot \lnot P et \vdash \lnot \lnot P \to P (simplification de la double négation ou raisonnement par l'absurde).
si \vdash P \to Q et \vdash P \to R, alors \vdash P \to Q \land R.
\vdash \lnot R \to \lnot(R \land Q)
si \vdash P \to R et \vdash Q \to R, alors \vdash P \lor Q \to R (disjonction des hypothèses).
si \vdash P et \vdash P \to Q, alors \vdash Q (modus ponens).

Nous allons maintenant prouver que, dans ces systèmes :

(i) Si une proposition est une tautologie alors elle est dérivable.

Il suffit de montrer le théorème pour des modèles finis. En effet, donnons-nous un ensemble infini (En mathématiques, un ensemble est infini s'il n'est pas fini, c'est-à-dire s'il contient un nombre infini d'éléments. En d'autres termes, si E est un ensemble...) dénombrable, ordonné par les entiers positifs, de propositions atomiques, toutes distinctes, p1, p2, p3... Un modèle initial de longueur (La longueur d’un objet est la distance entre ses deux extrémités les plus éloignées. Lorsque l’objet est filiforme ou en forme de lacet, sa longueur est...) n contient ou bien pi = V ou bien pi = F, mais pas les deux, pour 1 \le i \le n. Comme une proposition P ne contient qu’un nombre (La notion de nombre en linguistique est traitée à l’article « Nombre grammatical ».) fini de propositions atomiques, notons n le plus grand indice d'une proposition pn ayant une occurrence dans P. Si P est vraie dans tous les modèles initiaux de longueur n, alors elle est vraie dans tous les modèles où sa vérité est définie, puisque les propositions pm n'interviennent pas dans P pour m > n.

Preuve d'un résultat préliminaire

Pour prouver (i), on va d’abord prouver (ii) et (iii) ci-dessous. Soit P une formule propositionnelle, et \mathcal M un modèle. Notons h(\mathcal M) la conjonction de toutes les formules atomiques pn telle que pn = V est dans \mathcal M et de toutes les négations des formules atomiques pn telles que pn = F est dans \mathcal M.

(ii) Si P est vraie dans le modèle \mathcal M alors \vdash h(\mathcal M) \to P.
(iii) Si P est fausse dans le modèle \mathcal M alors \vdash h(\mathcal M) \to \lnot P.

On va prouver (ii) par induction sur la complexité (La complexité est une notion utilisée en philosophie, épistémologie (par exemple par Anthony Wilden ou Edgar Morin), en physique, en biologie (par exemple par Henri Atlan), en sociologie, en...) des formules. Celle-ci est mesurée par le nombre maximal d’opérateurs emboités. Par exemple dans (\lnot p) \lor (q \land r) , le ou et le non sont emboités l’un dans l’autre. Mais le non et le et ne le sont pas. Cette proposition est de complexité 2 parce qu’elle a au maximum deux opérateurs emboités.

Soit pi une proposition de complexité 0, c’est-à-dire une proposition atomique. La formule p_i \to p_i est dérivable, de même que toute formule du type H \to p_i, où H est n’importe quelle conjonction de propositions atomiques ou de leurs négations qui contient pi parmi elles. Si pi est vraie dans le modèle \mathcal M, h(\mathcal M) contient pi. (ii) est donc prouvée pour les propositions de complexité 0. La preuve de (iii) est identique.

Supposons que (ii) et (iii) soient vraies pour toutes les propositions de complexité au plus égale à n. Soit P une proposition de complexité n + 1. Deux cas sont possibles.

a) il y a un Q tel que P = \lnot Q

  • Si P est vraie dans le modèle \mathcal M alors Q est fausse dans \mathcal M. Comme Q est de complexité n, l’hypothèse d’induction donne, \vdash h(\mathcal M) \to \lnot Q. (ii) est donc prouvée pour P dans ce cas.
  • Si P est fausse dans le modèle \mathcal M alors Q est vraie dans \mathcal M. On a donc par induction \vdash h(\mathcal M) \to Q. Par ailleurs, on sait que \vdash Q \to \lnot\lnot Q. On peut alors déduire que \vdash h(\mathcal M) \to \lnot \lnot Q. (iii) est donc prouvée pour P dans ce cas.

b) il y a R et S tels que P = R \land S

  • Si P est vraie dans le modèle \mathcal M alors R et S sont toutes les deux vraies dans \mathcal M. On a alors par induction \vdash h(\mathcal M) \to R et \vdash h(\mathcal M) \to S. On en déduit que \vdash h(\mathcal M)\to R \land S. (ii) est donc prouvée pour P dans ce cas.
  • Si P est fausse dans le modèle \mathcal M alors l’une au moins de R ou de S est fausse dans \mathcal M. Supposons que ce soit R. On a alors par induction \vdash h(\mathcal M)\to \lnot R. Or, de \lnot R, on peut déduire \lnot(R \land S). (iii) est donc prouvée pour P dans ce cas.

Cela termine cette preuve de (ii) et (iii).

Fin de la démonstration (En mathématiques, une démonstration permet d'établir une proposition à partir de propositions initiales, ou précédemment démontrées à partir de propositions initiales, en s'appuyant sur...) du théorème de complétude

Prouvons maintenant (i), le théorème de complétude, par induction sur la longueur des modèles. Soit In l’énoncé : Si P est vraie dans tous les modèles de longueur n alors P est dérivable. Démontrons par récurrence les énoncés In.

Prouvons d’abord I1. Supposons que P est vraie dans tous les modèles de longueur 1, c’est-à-dire les deux modèles p1 = V et p1 = F. On a alors, d'après (ii) \vdash p_1 \to P et \vdash \lnot p_1 \to P. Par la règle de disjonction des hypothèses, on en déduit que \vdash (p_1 \lor \lnot p_1) \to P mais p_1 \lor \lnot p_1 est elle-même une formule dérivable : c’est le principe du tiers-exclu. La règle du modus ponens suffit alors pour prouver que \vdash P.

Supposons que In soit vrai. Soit P une proposition vraie dans tous les modèles de longueur n + 1. Soit \mathcal M un modèle de longueur n. P est vraie dans (\mathcal M, p_{n+1}=V) et dans (\mathcal M, p_{n+1}=F). D'après (ii), on a alors \vdash (h(\mathcal M) \land p_{n+1}) \to P et \vdash (h(\mathcal M) \land \lnot p_{n+1}) \to P. Comme ci-dessus, on en déduit que \vdash h(\mathcal M) \to P. Comme \mathcal M un modèle quelconque de longueur n, l'hypothèse de récurrence In permet de conclure que \vdash P. In + 1 est donc vérifiée.

Cela termine cette preuve du théorème de complétude du calcul des propositions.

Page générée en 0.199 seconde(s) - site hébergé chez Amen
Ce site fait l'objet d'une déclaration à la CNIL sous le numéro de dossier 1037632
Ce site est édité par Techno-Science.net - A propos - Informations légales
Partenaire: HD-Numérique