Aller au contenu
Topos Uranos
Français

Sémantique de la logique propositionnelle

Résumé

Jusqu’ici les formules ont été des chaînes de cercles et de disques, et les déductions, des manipulations de chaînes : rien n’a été dit de leur vérité. Cette leçon leur donne un sens. Une valuation assigne à chaque variable l’une des deux valeurs de vérité, 11 (vrai) et 00 (faux), et se prolonge à toutes les formules d’une seule manière, par récurrence sur leur complexité, avec une seule clause : (φ↓ψ)(\varphi \downarrow \psi) vaut 11 exactement quand φ\varphi et ψ\psi valent 00. De cette clause et des abréviations officielles on calcule, sans rien stipuler d’autre, les valeurs de la négation, de la disjonction, de la conjonction, de l’implication, de la double implication et de la disjonction exclusive. Le lemme de coïncidence, démontré par induction sur la complexité, assure que la valeur d’une formule ne dépend que des valeurs de ses variables ; il s’ensuit que la table de vérité, avec 2n2^n lignes pour nn variables, contient tout ce que les valuations, en nombre infini, peuvent dire de la formule. On définit ainsi la satisfaction, la validité, la satisfaisabilité, l’antilogie et la contingence, on fixe les formules ⊤\top et ⊥\bot, et l’on pose le problème de décider la validité, que les tables résolvent à un coût qui croît exponentiellement avec le nombre de variables.

Objectifs d’apprentissage

  1. Calculer la valeur de vérité d’une formule sous une valuation au moyen de son prolongement récursif, et déduire des abréviations officielles la valeur de chaque connecteur dérivé.
  2. Démontrer par induction sur la complexité le lemme de coïncidence, et expliquer grâce à lui pourquoi une table de vérité de 2n2^n lignes suffit pour étudier une formule à nn variables.
  3. Construire des tables de vérité colonne par colonne et classer des formules comme valides, contingentes ou antilogies, et des ensembles de formules comme satisfaisables ou insatisfaisables, sans confondre ⊭φ\not\models \varphi avec l’antilogie.
  4. Décider la validité d’une formule en cherchant une valuation qui la falsifie, et estimer le coût de la méthode des tables en fonction du nombre de variables.

Le sens des formules

L’unité sur le langage a construit, dans la leçon sur le langage de la logique propositionnelle, un ensemble de chaînes de deux symboles, et l’unité sur la déduction a appris à obtenir certaines chaînes à partir d’autres avec des axiomes et des règles. Aucune des deux n’a parlé de vérité : le système déductif transforme des symboles selon leur forme, comme une machine qui ne comprend pas ce qu’elle écrit. Or le langage a été construit pour représenter des énoncés, et la leçon sur la formalisation du langage naturel leur a attribué des lectures informelles : (φ↓ψ)(\varphi \downarrow \psi) est vraie quand φ\varphi et ψ\psi sont toutes deux fausses, et les lectures des autres connecteurs ont été déduites de celle-ci. La sémantique convertit ces lectures en définitions mathématiques.

Deux décisions la fondent. La première est la bivalence : il y a exactement deux valeurs de vérité, que l’on écrit 11 (vrai) et 00 (faux), et chaque formule, dans chaque situation, a l’une d’elles. La seconde est la vérifonctionnalité : la valeur d’une formule composée ne dépend que des valeurs de ses composantes, non de son sujet, de sorte que la vérité des variables décide de celle de toutes les formules. La leçon sur la formalisation a montré le prix de cette seconde décision (la causalité, la modalité et le temps restent en dehors) ; sa récompense est que la sémantique de tout le langage s’obtient d’une seule clause, celle du connecteur primitif.

Il convient de remarquer, en outre, que cette unité travaille entièrement dans le métalangage. Les affirmations « φ\varphi est vraie sous telle valuation » ou « φ\varphi est une tautologie » ne sont pas des formules, mais des énoncés mathématiques sur des formules, et elles se démontrent par un raisonnement ordinaire, souvent par induction sur la complexité ; ce ne sont pas des déductions dans le système du cours. La relation entre les deux mondes, à savoir que tout ce qui est déductible est vrai et que tout ce qui est vrai au sens précis de cette unité est déductible, est l’objet de l’unité sur la métathéorie.