Métathéorie : synthèse et défis

Résumé

Cette leçon clôt l’unité consacrée à la métathéorie et, avec elle, le contenu du cours. Elle reconstruit la chaîne déductive qui va de la validité des axiomes à la correction du système ; des deux lemmes de la négation conjointe au lemme de Kalmár et à la complétude pour les ensembles finis ; du lemme des deux témoins au théorème de compacité et, par lui, à la complétude forte ; et de la forme clausale à la correction et à la complétude pour la réfutation de la méthode de résolution, en indiquant à chaque maillon quels résultats il utilise et dans quelle leçon il est démontré. Elle montre comment les trois parties précédentes du cours, langage, déduction et sémantique, convergent dans la coïncidence de $\vdash$ et $\models$ , et ce que chacune y apporte ; elle distingue ce que le cours a démontré de ce qu’il a supposé et de ce qu’il laisse ouvert. Elle reprend dans son évaluation de sortie les compétences de l’évaluation d’entrée et se termine par six défis, plus difficiles que les problèmes des leçons, qui demandent de combiner les outils de plusieurs d’entre elles.

Objectifs d’apprentissage

Reconstruire l’ordre logique des résultats de l’unité, en identifiant les résultats antérieurs sur lesquels chacun s’appuie et la leçon où il est démontré, et justifier l’ordre de la compacité et de la complétude forte.
Expliquer comment langage, déduction et sémantique convergent dans la coïncidence de $\vdash$ et $\models$ , et quel résultat de chaque unité du cours y est indispensable.
Distinguer ce que le cours a démontré de ce qu’il a supposé (les schémas d’axiomes, les règles primitives et l’induction) et de ce qu’il laisse ouvert (le coût de décider la satisfaisabilité, et la logique avec quantificateurs).
Résoudre des problèmes qui combinent marquages, lemme de Kalmár, substitution uniforme, compacité et résolution, en utilisant dans chaque cas le côté facile de la coïncidence.

Ce que l’unité a accompli

L’unité s’était proposé de comparer les deux relations que les unités précédentes avaient construites sur le même langage, la déductibilité $\Gamma \vdash \varphi$ et la conséquence sémantique $\Gamma \models \varphi$ , et de démontrer qu’elles coïncident. Le but est atteint sans réserves dans les énoncés : les deux relations sont la même pour tout ensemble de prémisses, fini ou infini, et la résolution offre une troisième voie, également correcte et complète, pour décider la conséquence. Les réserves sont dans les méthodes, et chacune a été déclarée à sa place : la complétude de la première leçon est constructive mais pas pratique, car elle produit des déductions aussi longues que la table ; la compacité assure qu’une valuation existe, mais n’apprend pas à la trouver ; et la résolution décide, mais son coût dans le pire des cas est une question ouverte. Avec ces réserves, le chemin parcouru se lit comme une seule chaîne déductive en quatre tronçons.

Correction

La leçon sur correction et complétude a commencé par fixer le vocabulaire : le système est correct si $\Gamma \vdash \varphi \Rightarrow \Gamma \models \varphi$ , et complet si la réciproque est vraie, en trois degrés (faible, pour les ensembles finis et forte). Elle a démonté un argument circulaire qui prétend obtenir la complétude « par la correction » en passant de $\nvdash \chi$ à $\not\models \chi$ , un pas qui est la contraposée de la complétude faible, et elle a montré que les deux propriétés sont indépendantes. Elle a ensuite démontré que toute instance de A1, A2 et A3 est valide, en supposant une valuation qui la réfuterait et en arrivant, par la ligne fausse de l’implication, à des valeurs impossibles ; et, par induction forte sur le nombre de lignes, la correction, avec un cas pour les axiomes, un autre pour les prémisses, le modus ponens sémantique et, pour la règle de remplacement de la double négation, l’équivalence $\theta \eqsem \neg\neg\theta$ avec le théorème de remplacement sémantique. La propriété transmise de ligne en ligne n’est pas la validité, mais la satisfaction par une valuation fixée qui satisfait les prémisses, et c’est pourquoi la correction vaut avec des prémisses, même infinies. Il en a découlé la cohérence de tout ensemble satisfaisable, en particulier celle du système, et la méthode qui manquait à l’unité de déduction : un contre-modèle démontre qu’une déduction n’existe pas.

Kalmár et la complétude finie

La même leçon a démontré la réciproque en deux pas. Le premier est le lemme de Kalmár : si les variables de $\varphi$ sont parmi $u_{1}, \ldots, u_{n}$ , alors $\{u_{1}^{v}, \ldots, u_{n}^{v}\} \vdash \varphi^{v}$ pour toute valuation $v$ , où $\psi^{v}$ est $\psi$ si $v(\psi) = 1$ et $\neg\psi$ sinon ; le système déduit de chaque ligne ce que la ligne dit de la formule. Son induction sur la complexité a un seul cas composé, $(\alpha \downarrow \beta)$ , parce que la négation conjointe est le seul connecteur primitif, et à l’intérieur trois sous-cas, qui demandent deux lemmes du système, le second sous deux formes : $\vdash (\neg\alpha \rightarrow (\neg\beta \rightarrow (\alpha \downarrow \beta)))$ , déduit avec l’introduction de la conjonction, la double négation et deux applications de la règle RDN, et $\vdash (\alpha \rightarrow \neg(\alpha \downarrow \beta))$ et $\vdash (\beta \rightarrow \neg(\alpha \downarrow \beta))$ , déduits avec l’introduction de la disjonction. Le second pas élimine les prémisses : si $\varphi$ est une tautologie, elle se déduit des prémisses de chacune des $2^{n}$ lignes, et le raisonnement par disjonction des cas élimine le littéral de la dernière variable, puis celui de l’avant-dernière, jusqu’à arriver à $\vdash \varphi$ , la complétude faible. Avec le théorème de la déduction sémantique et la réciproque du syntaxique, la complétude s’est étendue aux ensembles finis de prémisses ; d’où, avec des prémisses finies, déduction et conséquence coïncident, l’équivalence prouvable coïncide avec la sémantique et la déductibilité est décidable, car la table en répond.

Compacité et complétude forte

La leçon sur le théorème de compacité a affronté le cas infini, que le lemme de Kalmár n’atteint pas, parce qu’une infinité de prémisses ne se décharge pas dans une implication. Elle a démontré, sans mentionner aucune déduction, qu’un ensemble est satisfaisable si et seulement si chacun de ses sous-ensembles finis l’est. Une suite de valeurs pour $v_{1}, \ldots, v_{n}$ est bonne si tout sous-ensemble fini de l’ensemble est satisfait par une valuation qui la prolonge ; le lemme des deux témoins assure qu’une bonne suite se prolonge en une bonne suite, car si aucun des deux prolongements n’était bon, la réunion des deux témoins finis contredirait que la suite est bonne ; et la valuation qui résulte du choix systématique de la valeur $1$ lorsque c’est possible satisfait chaque formule, par le lemme de coïncidence, car chaque formule a un nombre fini de variables. La construction n’a pas besoin de l’axiome du choix, car les variables sont numérotées et chaque pas a une règle. De la compacité ont découlé ses formes équivalentes, la forme de l’insatisfaisabilité et la forme de la conséquence ; de celle-ci, de la complétude pour les ensembles finis et de la monotonie, la complétude forte ; et de celle-ci et de la correction, la coïncidence complète : $\Gamma \vdash \varphi \Leftrightarrow \Gamma \models \varphi$ pour tout $\Gamma$ , et un ensemble est cohérent si et seulement s’il est satisfaisable. La leçon a averti que cet ordre n’est pas une affaire de préférence : obtenir la compacité d’une complétude forte encore indisponible serait circulaire. Elle s’est terminée par la coloration des graphes dénombrables, qui traduit un problème infini en un ensemble de formules dont les parties finies sont satisfaisables, et par les limites de ce qu’un ensemble de formules peut exprimer.

Résolution

La leçon sur la méthode de résolution a remplacé les ensembles de formules par des ensembles de clauses, chacune un ensemble fini de littéraux, avec deux représentations : la forme clausale, qui a les mêmes modèles, et la forme définitionnelle, qui introduit une variable nouvelle pour chaque sous-écriture composée, ne conserve que la satisfaisabilité et croît comme la formule, non comme une puissance de deux. Une seule règle agit sur les clauses : de $C$ et $D$ , avec $\ell \in C$ et $\ell^{*} \in D$ , on infère $(C \setminus \{\ell\}) \cup (D \setminus \{\ell^{*}\})$ , et une réfutation est une dérivation qui arrive à $\Box$ . La correction a été démontrée comme celle du système, par induction sur la dérivation et avec la résolvante comme conséquence de ses prémisses ; la complétude pour la réfutation, par induction sur le nombre de variables, avec l’élimination d’une variable, qui conserve la satisfaisabilité et dont la démonstration construit un modèle ; et pour les ensembles infinis, de nouveau avec la compacité. Il s’en est suivi que $\Gamma \models \varphi$ si et seulement si une forme clausale de $\Gamma \cup \{\neg\varphi\}$ a une réfutation, et que la saturation, finie parce qu’avec $n$ variables il n’y a pas plus de $4^{n}$ clauses, décide la satisfaisabilité sans tables. La leçon a présenté le problème de la satisfaisabilité, dont personne ne connaît le coût dans le pire des cas, et deux cas qui se décident rapidement, les clauses de Horn et celles de deux littéraux.

La figure suivante réunit les quatre tronçons en une seule chaîne. Chaque nœud de la colonne est un résultat, numéroté selon l’ordre logique et relié par un arc aux maillons antérieurs qu’utilise sa démonstration ; autour flottent les appuis, c’est-à-dire les principes et les outils auxquels la chaîne recourt sans cesse, chacun relié par un trait plein aux maillons qui s’appuient sur lui et par un pointillé au maillon où il est établi, sauf ceux qui viennent des unités précédentes, qui sont dessinés comme des anneaux. Cliquer sur un appui met en évidence tous les maillons qui l’utilisent, et chaque maillon renvoie à la leçon où il est démontré. On remarquera que la correction et la compacité, établies l’une dans le premier tronçon et l’autre dans le troisième, réapparaissent dans les tronçons suivants, et que l’appui le plus visité de l’unité est celui des valuations et coïncidence, suivi de l’induction, sous ses trois formes : sur les lignes d’une déduction, sur la complexité d’une formule et sur le nombre de variables d’un ensemble de clauses.

Appuis de la chaîne

AInduction et récurrence. Induction forte sur les entiers naturels, induction sur la complexité des formules, avec le seul cas composé $(\alpha \downarrow \beta)$ , et définition par récurrence. Elles ont été démontrées dans la première unité. Admis sans démonstration dans cette unité.
BSystème du cours. A1, A2 et A3, le modus ponens et la règle RDN ; réflexivité, monotonie, modus ponens entre déductions, finitude et $\Gamma \cup \{\varphi\} \vdash \psi \Leftrightarrow \Gamma \vdash (\varphi \rightarrow \psi)$ . Ils ont été établis dans la deuxième unité. Admis sans démonstration dans cette unité.
CTechniques dérivées. Double négation, de la leçon sur les quatre techniques ; introduction de la conjonction et de la disjonction et raisonnement par disjonction des cas (si $\Gamma \cup \{\psi\} \vdash \chi$ et $\Gamma \cup \{\neg\psi\} \vdash \chi$ , alors $\Gamma \vdash \chi$ ), de la leçon sur les techniques de la logique classique. Elles ont été démontrées dans la deuxième unité. Admis sans démonstration dans cette unité.
DValuations et coïncidence. $v((\alpha \downarrow \beta)) = (1 - v(\alpha))(1 - v(\beta))$ ; si deux valuations coïncident sur $V(\varphi)$ , elles donnent à $\varphi$ la même valeur ; la validité se décide avec $2^{n}$ lignes. Elles ont été démontrées dans la troisième unité. Admis sans démonstration dans cette unité.
EConséquence sémantique. Ligne fausse de l’implication, monotonie, $\Gamma \cup \{\varphi\} \models \psi \Leftrightarrow \Gamma \models (\varphi \rightarrow \psi)$ , $\Gamma \models \varphi$ si et seulement si $\Gamma \cup \{\neg\varphi\}$ est insatisfaisable, et le théorème de remplacement sémantique. Ils ont été démontrés dans la troisième unité. Admis sans démonstration dans cette unité.
FFormes conjonctives. Lemme de la valeur ; toute formule équivaut à une forme normale conjonctive, qui peut nécessiter $2^{n}$ clauses ; une disjonction de littéraux est valide si et seulement si elle contient une paire complémentaire. Ils ont été démontrés dans la troisième unité. Admis sans démonstration dans cette unité.
GCorrection. Si $\Gamma \vdash \varphi$ , alors $\Gamma \models \varphi$ , pour tout ensemble $\Gamma$ ; un contre-modèle démontre qu’une déduction n’existe pas. Établi dans: 2. Correction.
HCompacité. Un ensemble de formules est satisfaisable si et seulement si chacun de ses sous-ensembles finis est satisfaisable ; d’où ce qui est insatisfaisable l’est déjà dans une partie finie. Établi dans: 11. Théorème de compacité.

Tronçon 1 Correction
- Vérifier que toute instance des schémas est valide sans construire sa table.
- Démontrer la correction par induction forte sur le nombre de lignes, avec le cas de la règle de remplacement de la double négation.
- Démontrer par un contre-modèle qu’une formule ne se déduit pas, et obtenir la cohérence à partir de la correction.
1. Validité des axiomes. Toute instance de A1, A2 et A3 est valide : une valuation qui la réfuterait exigerait, par la ligne fausse de l’implication, des valeurs impossibles.
  Repose sur: E (Conséquence sémantique). Démontré dans: Correction et complétude.
2. Correction. Si $\Gamma \vdash \varphi$ , alors $\Gamma \models \varphi$ , pour tout $\Gamma$ : par induction forte sur le nombre de lignes, avec un cas pour les axiomes, un autre pour les prémisses, le modus ponens sémantique et, pour la règle RDN, $\theta \eqsem \neg\neg\theta$ avec le remplacement sémantique.
  Utilise: 1. Validité des axiomes. Repose sur: A (Induction et récurrence), B (Système du cours), E (Conséquence sémantique). Démontré dans: Correction et complétude.
3. Cohérence et contre-modèles. Tout ensemble satisfaisable est cohérent ; le système est cohérent et $\nvdash v_{1}$ ; si une valuation satisfait $\Gamma$ et réfute $\varphi$ , alors $\Gamma \nvdash \varphi$ , et la table certifie que ce qui n’est pas valide n’est pas un théorème.
  Repose sur: G (Correction), D (Valuations et coïncidence). Démontré dans: Correction et complétude.
Tronçon 2 Kalmár et la complétude finie
- Déduire dans le système les deux lemmes de la négation conjointe, avec la règle de remplacement de la double négation là où il le faut.
- Démontrer le lemme de Kalmár par induction sur la complexité, avec un seul cas composé.
- Éliminer par le raisonnement par disjonction des cas les prémisses des lignes, et décharger des prémisses finies avec les deux théorèmes de la déduction.
- Décider avec la table la déductibilité, l’équivalence prouvable et la cohérence à partir de prémisses finies.
1. Introduction de la négation conjointe. $\{\neg\alpha, \neg\beta\} \vdash (\alpha \downarrow \beta)$ et $\vdash (\neg\alpha \rightarrow (\neg\beta \rightarrow (\alpha \downarrow \beta)))$ : la conjonction des négations est $\neg\neg(\neg\neg\alpha \downarrow \neg\neg\beta)$ ; la double négation retire l’extérieure, et la règle RDN les deux intérieures.
  Repose sur: B (Système du cours), C (Techniques dérivées). Démontré dans: Correction et complétude.
2. Négation de la négation conjointe. $\vdash (\alpha \rightarrow \neg(\alpha \downarrow \beta))$ et $\vdash (\beta \rightarrow \neg(\alpha \downarrow \beta))$ , car $\neg(\alpha \downarrow \beta)$ est $(\alpha \vee \beta)$ et l’introduction de la disjonction suffit.
  Repose sur: B (Système du cours), C (Techniques dérivées). Démontré dans: Correction et complétude.
3. Lemme de Kalmár. Si $V(\varphi) \subseteq \{u_{1}, \ldots, u_{n}\}$ , alors $\{u_{1}^{v}, \ldots, u_{n}^{v}\} \vdash \varphi^{v}$ pour toute valuation $v$ ; le pas inductif a un seul cas, $(\alpha \downarrow \beta)$ , avec trois sous-cas selon les valeurs de $\alpha$ et de $\beta$ .
  Utilise: 4. Introduction de la négation conjointe, 5. Négation de la négation conjointe. Repose sur: A (Induction et récurrence), D (Valuations et coïncidence), B (Système du cours). Démontré dans: Correction et complétude.
4. Complétude faible. Si $\models \varphi$ , alors $\vdash \varphi$ : le lemme de Kalmár déduit $\varphi$ de chaque ligne, et le raisonnement par disjonction des cas élimine les littéraux de la dernière variable à la première, avec $2^{n}$ usages du lemme et $2^{n} - 1$ du raisonnement par disjonction des cas.
  Utilise: 6. Lemme de Kalmár. Repose sur: C (Techniques dérivées). Démontré dans: Correction et complétude.
5. Complétude pour les ensembles finis. $\{\gamma_{1}, \ldots, \gamma_{k}\} \models \varphi \Rightarrow \{\gamma_{1}, \ldots, \gamma_{k}\} \vdash \varphi$ : le théorème de la déduction sémantique conduit à une tautologie, la complétude faible la déduit et la réciproque du théorème de la déduction rend les prémisses.
  Utilise: 7. Complétude faible. Repose sur: E (Conséquence sémantique), B (Système du cours). Démontré dans: Correction et complétude.
6. Coïncidence finie et décision. Pour $\Gamma$ fini, $\Gamma \vdash \varphi \Leftrightarrow \Gamma \models \varphi$ , et $\varphi \dashv\vdash \psi \Leftrightarrow \varphi \eqsem \psi$ ; d’où la déductibilité à partir de prémisses finies est décidable, par la table.
  Utilise: 8. Complétude pour les ensembles finis. Repose sur: G (Correction), D (Valuations et coïncidence). Démontré dans: Correction et complétude.
Tronçon 3 Compacité et complétude forte
- Démontrer la compacité en fixant une à une les valeurs des variables, avec l’invariant des bonnes suites et l’argument des deux témoins.
- Passer entre la forme de la satisfaisabilité, celle de l’insatisfaisabilité et celle de la conséquence.
- Obtenir la complétude forte à partir de la compacité, sans circularité, et d’elle la coïncidence de la cohérence avec la satisfaisabilité.
- Coder dans des ensembles de formules des problèmes sur des objets infinis et les résoudre par la compacité.
1. Lemme des deux témoins. Si la suite $s$ de valeurs fixées est bonne (tout sous-ensemble fini de l’ensemble est satisfait par une valuation qui la prolonge), alors $(s, 1)$ ou $(s, 0)$ l’est aussi : si aucune ne l’était, la réunion des deux témoins finis contredirait que $s$ est bonne.
  Repose sur: D (Valuations et coïncidence). Démontré dans: Le théorème de compacité.
2. Théorème de compacité. $\Gamma$ est satisfaisable si et seulement si tout sous-ensemble fini l’est : on fixe $v_{n + 1}$ à $1$ si $(s_{n}, 1)$ est bonne et à $0$ sinon, et la valuation résultante satisfait chaque formule par le lemme de coïncidence. L’axiome du choix n’est pas nécessaire, car les variables sont numérotées.
  Utilise: 10. Lemme des deux témoins. Repose sur: A (Induction et récurrence), D (Valuations et coïncidence). Démontré dans: Le théorème de compacité.
3. Formes équivalentes. $\Gamma$ est insatisfaisable si et seulement si une partie finie l’est ; $\Gamma \models \varphi$ si et seulement si $\Gamma_{0} \models \varphi$ pour un certain $\Gamma_{0} \subseteq \Gamma$ fini ; et cette dernière forme implique à son tour le théorème.
  Utilise: 11. Théorème de compacité. Repose sur: E (Conséquence sémantique). Démontré dans: Le théorème de compacité.
4. Complétude forte. Si $\Gamma \models \varphi$ , alors $\Gamma \vdash \varphi$ , pour tout $\Gamma$ : la forme de la conséquence donne un $\Gamma_{0}$ fini, la complétude pour les ensembles finis donne $\Gamma_{0} \vdash \varphi$ , et la monotonie $\Gamma \vdash \varphi$ .
  Utilise: 8. Complétude pour les ensembles finis, 12. Formes équivalentes. Repose sur: B (Système du cours). Démontré dans: Le théorème de compacité.
5. La déduction est la conséquence. $\Gamma \vdash \varphi \Leftrightarrow \Gamma \models \varphi$ pour tout $\Gamma$ ; les théorèmes sont exactement les tautologies, et un ensemble est cohérent si et seulement s’il est satisfaisable.
  Utilise: 13. Complétude forte. Repose sur: G (Correction). Démontré dans: Le théorème de compacité.
6. Coloration des graphes dénombrables. Avec une variable $x_{i,c}$ pour chaque sommet et chaque couleur, et des formules disant que chaque sommet a une couleur et une seule et que les voisins diffèrent, un graphe dénombrable admet une coloration à $k$ couleurs si tout sous-graphe fini en admet une.
  Repose sur: H (Compacité), F (Formes conjonctives). Démontré dans: Le théorème de compacité.
Tronçon 4 Résolution
- Représenter un ensemble de formules comme un ensemble de clauses, par la forme conjonctive ou par la forme définitionnelle.
- Construire des réfutations sans éliminer deux paires complémentaires en un seul pas.
- Démontrer la correction et la complétude pour la réfutation de la résolution, pour les ensembles finis et, avec la compacité, pour des ensembles quelconques.
- Décider des conséquences par saturation et reconnaître les cas qui se décident rapidement.
1. Forme clausale. Une clause est un ensemble fini de littéraux, satisfaite si un littéral prend la valeur $1$ , et $\Box$ est insatisfaisable ; une forme clausale de $\Gamma$ a les mêmes modèles, et $\Gamma \models \varphi$ si et seulement si une forme clausale de $\Gamma \cup \{\neg\varphi\}$ est insatisfaisable.
  Repose sur: F (Formes conjonctives), E (Conséquence sémantique). Démontré dans: La méthode de résolution.
2. Forme clausale définitionnelle. Avec une variable nouvelle par sous-écriture et ses clauses de définition, $T(\varphi)$ est équisatisfaisable avec $\varphi$ et a au plus $4k + 1$ clauses d’au plus trois littéraux ; les formes définitionnelles décident la conséquence à partir de prémisses finies.
  Utilise: 16. Forme clausale. Repose sur: A (Induction et récurrence), D (Valuations et coïncidence). Démontré dans: La méthode de résolution.
3. Correction de la résolution. $\{C, D\} \models R_{\ell}(C, D)$ , par cas sur la valeur de $\ell$ ; par induction forte sur la dérivation, $S \models C$ pour toute clause $C$ dérivée de $S$ , et si $S$ a une réfutation, il est insatisfaisable.
  Utilise: 16. Forme clausale. Repose sur: A (Induction et récurrence). Démontré dans: La méthode de résolution.
4. Élimination d’une variable. $E_{p}(S)$ , qui conserve les clauses sans $p$ ni $\neg p$ et ajoute les résolvantes sur $p$ , ne contient pas $p$ et est équisatisfaisable avec $S$ ; d’un modèle de celui-ci on obtient un modèle de $S$ en choisissant la valeur de $p$ .
  Utilise: 18. Correction de la résolution. Repose sur: D (Valuations et coïncidence). Démontré dans: La méthode de résolution.
5. Complétude pour la réfutation, cas fini. Tout ensemble fini insatisfaisable de clauses a une réfutation, par induction sur le nombre de variables : on élimine la dernière et on insère les prémisses de chaque résolvante.
  Utilise: 19. Élimination d’une variable. Repose sur: A (Induction et récurrence). Démontré dans: La méthode de résolution.
6. Complétude pour la réfutation. Un ensemble de clauses, fini ou infini, est insatisfaisable si et seulement s’il a une réfutation ; d’où $\Gamma \models \varphi$ si et seulement si une forme clausale de $\Gamma \cup \{\neg\varphi\}$ a une réfutation.
  Utilise: 16. Forme clausale, 18. Correction de la résolution, 20. Complétude pour la réfutation, cas fini. Repose sur: H (Compacité). Démontré dans: La méthode de résolution.
7. La saturation décide. Avec $n$ variables, l’ensemble des clauses dérivées a au plus $4^{n}$ éléments ; la saturation termine et décide la satisfaisabilité sans tables, mais pas toujours plus vite qu’elles.
  Utilise: 18. Correction de la résolution, 20. Complétude pour la réfutation, cas fini. Démontré dans: La méthode de résolution.

La fin du cours. La chaîne se termine là où les deux faces du cours se reconnaissent comme une seule relation et où l’on dispose d’une méthode pour la décider. Ce qui reste ouvert n’est plus une question sur la logique propositionnelle, mais sur son coût et sur son extension aux quantificateurs.