Théorème de complétude (calcul des propositions)
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 <math>P</math> du calcul des propositions :
- ou bien on montre que cette formule est vraie dans tout modèle (voir ci-dessous). On dit alors que <math>P</math> est une tautologie, et on note <math>\vDash P</math>.
- ou bien on montre que cette formule est prouvable ou dérivable en utilisant un système de déduction, et on note <math>\vdash P</math>.
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 <math>\vdash P</math> est vérifié, alors <math>\vDash P</math> l'est également.
Le système de déduction sera complet, si inversement, il permet de déduire toute formule vraie. Autrement dit, si <math>\vDash P</math> est vérifié, le système de déduction doit permettre de démontrer qu'on a également <math>\vdash P</math>.
Le théorème de complétude du calcul des propositions énonce que les systèmes de déduction, décrits dans les articles calcul des propositions ou déduction naturelle ou calcul des séquents, sont complets. Il y a équivalence entre être une tautologie et être prouvable.
Le théorème de complétude du calcul des propositions classique a été démontré par Paul Bernays en 1926.
Approche classique de la véracité et de la 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 classique est leur véracité ou leur fausseté. Si on représente les propositions atomiques par des lettres, <math>p</math>, <math>q</math>, <math>r</math>, ... ; on peut les concevoir comme des variables qui peuvent recevoir deux valeurs, <math>V</math> pour vrai, et <math>F</math> pour faux.
Un modèle est défini par l’attribution de valeurs de vérité, <math>V</math> ou <math>F</math>, aux propositions atomiques. Par exemple <math>(p=V, q=F, r=V)</math> désigne le modèle <math>\mathcal M</math> dans lequel il y a trois propositions atomiques <math>p</math>, <math>q</math>, et <math>r</math>, la seconde é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 <math>\lnot</math>, et <math>\land</math>, ou <math>\lor</math>, implique <math>\to</math>. Ses axiomes sont données par les tables de vérité suivantes : Modèle:Énoncé Les règles relatives à <math>\lor</math> et <math>\to</math> s'en déduisent en posant : Modèle:Énoncé
On peut alors calculer, par exemple, que dans le modèle <math>\mathcal M</math> défini par <math>p=F</math> :
Modèle:Énoncé
On en conclut que <math>\lnot(p \land \lnot p)</math> est vraie dans le modèle <math>p=F</math>. On montre de même qu'elle est aussi vraie dans le modèle <math>p=V</math> et puisqu’elle ne contient que <math>p</math> comme proposition atomique, elle est vraie dans tous les modèles et est donc une tautologie.
Démonstration du théorème de complétude du calcul des propositions classique
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 : Modèle:Énoncé Modèle:Énoncé Modèle:Énoncé Modèle:Énoncé Modèle:Énoncé
Nous allons maintenant démontrer que, dans ces systèmes : Modèle:Théorème
Il suffit de montrer le théorème pour des modèles finis. En effet, ordonnons linéairement les propositions atomiques, nous obtenons la suite <math>p_1</math>, <math>p_2</math>, <math>p_3</math>... Un modèle initial ou bien valide <math>p_i</math> ou bien ne valide pas <math>p_i</math>, mais ne fait pas les deux. Comme une proposition <math>P</math> ne contient qu’un nombre fini de propositions atomiques, notons <math>n</math> le plus grand indice parmi ceux des propositions <math>p_n</math> qui ont une occurrence dans <math>P</math>. Si <math>P</math> est vraie dans tous les modèles initiaux de longueur <math>n</math>, alors elle est vraie dans tous les modèles, puisque les propositions <math>p_m</math> n'ont pas d'occurrence dans <math>P</math> quand <math>m>n</math>, donc la valeur de vérité de ces propositions atomiques n'a aucune incidence sur la véracité de <math>P</math>.
Démonstration d'un résultat liminaire
Pour démontrer (i), on va d’abord démontrer (ii) et (iii) ci-dessous. Soit <math>P</math> une formule propositionnelle, et <math>\mathcal M</math> un modèle. Notons <math>h(\mathcal M)</math> la conjonction de toutes les formules atomiques <math>p_n</math> telle que <math>p_n=V</math> est dans <math>\mathcal M</math> et de toutes les négations des formules atomiques <math>p_n</math> telles que <math>p_n=F</math> est dans <math>\mathcal M</math>.
On va démontrer (ii) par induction sur la complexité des formules. Celle-ci est mesurée par le nombre maximal d’opérateurs emboités. Par exemple dans <math>(\lnot p) \lor (q \land r)</math> , 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 <math>p_i</math> une proposition de complexité 0, c’est-à-dire une proposition atomique. La formule <math>p_i \to p_i</math> est dérivable, de même que toute formule du type <math>H \to p_i</math>, où <math>H</math> est n’importe quelle conjonction de propositions atomiques ou de leurs négations qui contient <math>p_i</math> parmi elles. Si <math>p_i</math> est vraie dans le modèle <math>\mathcal M</math>, <math>h(\mathcal M)</math> contient <math>p_i</math>. (ii) est donc démontrée pour les propositions de complexité 0. La démonstration de (iii) est identique.
Supposons que (ii) et (iii) soient vraies pour toutes les propositions de complexité au plus égale à <math>n</math>. Soit <math>P</math> une proposition de complexité <math>n+1</math>. Deux cas sont possibles.
a) il y a un <math>Q</math> tel que <math>P = \lnot Q</math>
- Si <math>P</math> est vraie dans le modèle <math>\mathcal M</math> alors <math>Q</math> est fausse dans <math>\mathcal M</math>. Comme <math>Q</math> est de complexité <math>n</math>, l’hypothèse d’induction donne, <math>\vdash h(\mathcal M) \to \lnot Q</math>. (ii) est donc démontrée pour <math>P</math> dans ce cas.
- Si <math>P</math> est fausse dans le modèle <math>\mathcal M</math> alors <math>Q</math> est vraie dans <math>\mathcal M</math>. On a donc par induction <math>\vdash h(\mathcal M) \to Q</math>. Par ailleurs, on sait que <math>\vdash Q \to \lnot\lnot Q</math>. On peut alors déduire que <math>\vdash h(\mathcal M) \to \lnot \lnot Q</math>. (iii) est donc démontrée pour <math>P</math> dans ce cas.
b) il y a <math>R</math> et <math>S</math> tels que <math>P = R \land S</math>
- Si <math>P</math> est vraie dans le modèle <math>\mathcal M</math> alors <math>R</math> et <math>S</math> sont toutes les deux vraies dans <math>\mathcal M</math>. On a alors par induction <math>\vdash h(\mathcal M) \to R</math> et <math>\vdash h(\mathcal M) \to S</math>. On en déduit que <math>\vdash h(\mathcal M)\to R \land S</math>. (ii) est donc démontrée pour <math>P</math> dans ce cas.
- Si <math>P</math> est fausse dans le modèle <math>\mathcal M</math> alors l’une au moins de <math>R</math> ou de <math>S</math> est fausse dans <math>\mathcal M</math>. Supposons que ce soit <math>R</math>. On a alors par induction <math>\vdash h(\mathcal M)\to \lnot R</math>. Or, de <math>\lnot R</math>, on peut déduire <math>\lnot(R \land S)</math>. (iii) est donc démontrée pour <math>P</math> dans ce cas.
Cela termine cette démonstration de (ii) et (iii).
Fin de la démonstration 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 <math>I_n</math> l’énoncé : Si <math>P</math> est vraie dans tous les modèles de longueur <math>n</math> alors <math>P</math> est dérivable. Démontrons par récurrence les énoncés <math>I_n</math>.
Prouvons d’abord <math>I_1</math>.
Supposons que <math>P</math> est vraie dans tous les modèles de longueur 1, c’est-à-dire les deux modèles <math>p_1=V</math> et <math>p_1=F</math>. On a alors, d'après (ii) <math>\vdash p_1 \to P</math> et <math>\vdash \lnot p_1 \to P</math>. Par la règle de disjonction des hypothèses, on en déduit que <math>\vdash (p_1 \lor \lnot p_1) \to P</math> mais <math>p_1 \lor \lnot p_1</math> est elle-même une formule dérivable : c’est le principe du tiers-exclu. La règle du modus ponens suffit alors pour démontrer que <math>\vdash P</math>.
Supposons que <math>I_n</math> soit vrai. Soit <math>P</math> une proposition vraie dans tous les modèles de longueur <math>n+1</math>. Soit <math>\mathcal M</math> un modèle de longueur <math>n</math>. <math>P</math> est vraie dans <math>(\mathcal M, p_{n+1}=V)</math> et dans <math>(\mathcal M, p_{n+1}=F)</math>. D'après (ii), on a alors <math>\vdash (h(\mathcal M) \land p_{n+1}) \to P</math> et <math>\vdash (h(\mathcal M) \land \lnot p_{n+1}) \to P</math>. Comme ci-dessus, on en déduit que <math>\vdash h(\mathcal M) \to P</math>. Comme <math>\mathcal M</math> un modèle quelconque de longueur <math>n</math>, l'hypothèse de récurrence <math>I_n</math> permet de conclure que <math>\vdash P</math>. <math>I_{n+1}</math> est donc vérifiée.
Cela termine cette démonstration du théorème de complétude du calcul des propositions.
