Métathéorie : introduction

Résumé

Cette leçon ouvre la quatrième et dernière unité de contenu du cours, consacrée à la métathéorie. Elle présente ses trois leçons et le fil qui les unit : les deux unités précédentes ont construit, sur la même langue, deux notions de ce qui suit de certaines prémisses, la déduction $\Gamma \vdash \varphi$ et la conséquence sémantique $\Gamma \models \varphi$ , et cette unité démontre qu’elles coïncident, d’abord pour des prémisses en nombre fini (correction, lemme de Kalmár et complétude), ensuite pour des prémisses quelconques (théorème de compacité et complétude forte), et offre enfin une troisième manière de décider la conséquence, la méthode de résolution, dont elle démontre aussi qu’elle est correcte et complète. Elle explique pourquoi la compacité se démontre avant la complétude forte, et non l’inverse ; elle montre par deux exemples les questions auxquelles ni la recherche de déductions ni la table de vérité ne peuvent répondre à elles seules ; elle précise ce que l’on prend des trois unités précédentes et donne des conseils pour l’étudier.

Objectifs d’apprentissage

Décrire la suite des trois leçons de l’unité, expliquer quels résultats de chacune la suivante utilise et justifier que la compacité soit démontrée, par un argument sémantique, avant la complétude forte.
Distinguer les deux faces du cours, la déductibilité $\Gamma \vdash \varphi$ , existentielle et finie, et la conséquence sémantique $\Gamma \models \varphi$ , universelle sur une infinité de valuations, et énoncer la correction et la complétude dans leurs trois degrés.
Expliquer pourquoi la coïncidence des deux relations ne peut pas s’établir cas par cas, mais seulement par des métathéorèmes, et reconnaître quels instruments des unités précédentes (récurrences et inductions, raisonnement par disjonction des cas, théorèmes de déduction, lemme de coïncidence, formes conjonctives) chaque démonstration utilisera.
Lire des déductions sur les déductions et des arguments sémantiques de l’unité en distinguant à chaque pas la relation dont il est question, et organiser l’étude à partir de l’évaluation d’entrée.

Évaluation d’entrée

Avant de parcourir l’unité, il convient de mesurer le point de départ. Cette évaluation est une autoévaluation : elle n’est pas notée, et son seul but est d’orienter l’étude. Ses quinze questions sont de deux sortes. Les six premières portent sur ce que l’unité tient pour acquis des précédentes : la définition de la conséquence sémantique et sa réduction à l’insatisfaisabilité, la valeur de la négation conjointe, le lemme de coïncidence, la finitude de la déduction et le raisonnement par disjonction des cas ; qui en manque une doit revoir, avant de poursuivre, la leçon que la question nomme. Les neuf autres portent, dans l’ordre, sur les trois leçons de cette unité, trois sur chacune. Qui n’a jamais étudié la métathéorie d’un système logique ne doit pas s’attendre à les réussir, et cela n’a pas d’importance : chaque réponse, juste ou non, explique le point et nomme la leçon qui le traite. Les mêmes compétences sont mesurées de nouveau à la fin, dans la leçon de synthèse.

Évaluation d’entrée

Avant de commencer l’unité, mesurez votre point de départ. C’est une autoévaluation brève : elle n’est pas notée et son résultat n’est conservé que dans votre navigateur.

Question 1Des unités précédentesQue signifie $\Gamma \models \varphi$ ?
Que toute valuation qui satisfait toutes les formules de $\Gamma$ satisfait $\varphi$ .
Qu’il existe une déduction de $\varphi$ à partir de $\Gamma$ .
Qu’une valuation satisfait à la fois $\Gamma$ et $\varphi$ .
Que $\varphi$ est conséquence d’une formule de $\Gamma$ prise seule.
Question 2Des unités précédentesLaquelle des affirmations suivantes équivaut à $\Gamma \models \varphi$ ?
Que $\Gamma \cup \{\neg\varphi\}$ est insatisfaisable.
Que $\Gamma \cup \{\varphi\}$ est satisfaisable.
Que $\Gamma \cup \{\neg\varphi\}$ est satisfaisable.
Que $\neg\varphi$ est insatisfaisable.
Question 3Des unités précédentesSi une valuation $v$ donne à $\alpha$ la valeur $1$ , quelle valeur donne-t-elle à $(\alpha \downarrow \beta)$ ?
$0$ , quelle que soit la valeur de $\beta$ .
Cela dépend de $\beta$ : elle vaut $1$ si $\beta$ vaut $0$ .
$1 - v(\beta)$ .
$1$ , parce que l’une des composantes est vraie.
Question 4Des unités précédentesLes variables de $\varphi$ sont $v_{2}$ et $v_{7}$ . Deux valuations $v$ et $w$ donnent les mêmes valeurs à $v_{2}$ et à $v_{7}$ , et des valeurs opposées à toutes les autres variables. Si $v(\varphi) = 1$ , que peut-on affirmer de $w(\varphi)$ ?
Que $w(\varphi) = 1$ .
Rien, parce que $v$ et $w$ diffèrent sur une infinité de variables.
Que $w(\varphi) = 0$ , parce que $w$ inverse presque toutes les valeurs de $v$ .
Que $w(\varphi) = 1$ seulement si $v$ et $w$ coïncident aussi sur $v_{1}, \ldots, v_{6}$ .
Question 5Des unités précédentesSoit $\Gamma$ un ensemble infini de formules tel que $\Gamma \vdash \varphi$ . Que peut-on affirmer ?
Qu’un sous-ensemble fini de $\Gamma$ déduit $\varphi$ .
Que $\varphi$ est un théorème.
Que la déduction utilise toutes les formules de $\Gamma$ .
Rien sans le théorème de compacité, parce que $\Gamma$ est infini.
Question 6Des unités précédentesOn sait que $\Gamma \cup \{p\} \vdash \chi$ et que $\Gamma \cup \{\neg p\} \vdash \chi$ . Que permet de conclure le raisonnement par disjonction des cas ?
Que $\Gamma \vdash \chi$ .
Rien, tant qu’on ne sait pas si $\Gamma$ déduit $p$ ou déduit $\neg p$ .
Que $\Gamma \vdash (p \leftrightarrow \chi)$ .
Seulement que $\Gamma \cup \{p, \neg p\} \vdash \chi$ .
Question 7Le système du cours est correct. Qu’affirme cette propriété ?
Que, pour tout ensemble $\Gamma$ , si $\Gamma \vdash \varphi$ , alors $\Gamma \models \varphi$ .
Que si $\Gamma \models \varphi$ , alors $\Gamma \vdash \varphi$ .
Qu’il n’existe aucune formule $\varphi$ avec $\vdash \varphi$ et $\vdash \neg\varphi$ .
Que toute formule vraie est un théorème.
Question 8Soit $v$ la valuation qui donne $1$ à $p$ et $0$ à $q$ . Qu’affirme le lemme de Kalmár, avec les variables $p$ et $q$ , pour la formule $(p \leftrightarrow q)$ ?
Que $\{p, \neg q\} \vdash \neg(p \leftrightarrow q)$ .
Que $\{p, \neg q\} \vdash (p \leftrightarrow q)$ .
Que $\{p, q\} \vdash \neg(p \leftrightarrow q)$ .
Que $\vdash \neg(p \leftrightarrow q)$ .
Question 9Un système déductif peut-il être correct sans être complet ?
Oui : le système de Łukasiewicz, sans la règle RDN, est correct et ne déduit pas la tautologie $((v_{1} \downarrow v_{2}) \rightarrow \neg v_{1})$ .
Non : la correction et la complétude se déduisent l’une de l’autre.
Non : un système dont les axiomes sont des tautologies déduit toutes les tautologies.
Oui, mais seulement si le système est incohérent.
Question 10Qu’affirme le théorème de compacité ?
Qu’un ensemble de formules est satisfaisable si et seulement si tout sous-ensemble fini de cet ensemble est satisfaisable.
Qu’un ensemble de formules est satisfaisable si et seulement si chacune de ses formules est satisfaisable.
Que tout ensemble infini de formules est satisfaisable.
Qu’un ensemble est satisfaisable si l’un de ses sous-ensembles finis l’est.
Question 11Soit $\Gamma$ un ensemble infini de formules tel que $\Gamma \models \varphi$ . Qu’assure la compacité ?
Que $\Gamma_{0} \models \varphi$ pour un certain sous-ensemble fini $\Gamma_{0}$ de $\Gamma$ .
Que $\varphi$ est conséquence d’une formule de $\Gamma$ prise seule.
Que $\varphi$ est conséquence de tout sous-ensemble fini de $\Gamma$ .
Que $\varphi$ est valide.
Question 12La première leçon démontre la complétude pour les ensembles finis de prémisses. Pourquoi la finitude de la déduction ne suffit-elle pas pour l’étendre à un ensemble infini $\Gamma$ ?
Parce que la finitude parle de $\Gamma \vdash \varphi$ , et que ce que l’on a, c’est $\Gamma \models \varphi$ : il faut que la conséquence, non la déduction, se réduise à une partie finie, et c’est la compacité.
Elle suffit : si $\Gamma \models \varphi$ , la finitude donne un $\Gamma_{0}$ fini avec $\Gamma_{0} \models \varphi$ .
Parce que le lemme de Kalmár ne vaut pas pour les formules à une infinité de variables.
Parce que la complétude est fausse pour les ensembles infinis de prémisses.
Question 13Quelle est la résolvante des clauses $\{p, \neg q, r\}$ et $\{q, s\}$ ?
$\{p, r, s\}$ .
$\{p, \neg q, r, q, s\}$ .
$\{p, r\}$ .
Elles n’ont pas de résolvante, car elles n’ont aucun littéral en commun.
Question 14Pour décider par résolution si $\{(p \vee q), \neg p\} \models q$ , quel ensemble de clauses tente-t-on de réfuter ?
$\{\{p, q\}, \{\neg p\}, \{\neg q\}\}$ .
$\{\{p, q\}, \{\neg p\}, \{q\}\}$ .
$\{\{p, q\}, \{\neg p\}\}$ .
$\{\{\neg p, \neg q\}, \{p\}, \{\neg q\}\}$ .
Question 15Peut-on dériver par résolution la clause vide $\Box$ de l’ensemble $\{\{p, q\}, \{\neg p, \neg q\}\}$ ?
Non : l’ensemble est satisfaisable, et la résolution est correcte.
Oui, en un seul pas, en éliminant à la fois les deux paires complémentaires.
Oui, en deux pas : d’abord sur $p$ , puis sur $q$ .
Non, parce qu’aucune des deux clauses n’est unitaire.