Aller au contenu
Topos Uranos
Français

Le théorème de compacité

Résumé

Une déduction est une suite finie et n’utilise qu’un nombre fini de prémisses ; la satisfaction d’un ensemble infini de formules, en revanche, exige une seule valuation qui donne la valeur 11 à une infinité de formules à la fois, et rien dans sa définition ne dit qu’il suffise d’examiner des parties finies. Le théorème de compacité affirme que cela suffit : un ensemble de formules est satisfaisable si et seulement si chacun de ses sous-ensembles finis l’est. Cette leçon le démontre par un argument sémantique direct, sans passer par la déduction : on fixe une à une les valeurs des variables v1,v2,…v_1, v_2, \ldots, en conservant à chaque pas l’invariant selon lequel tout sous-ensemble fini de l’ensemble reste satisfaisable par une valuation qui respecte ce qui est déjà fixé ; si aucun des deux choix possibles ne le conservait, la réunion des deux témoins finis de cet échec contredirait l’invariant précédent, et à la fin chaque formule est satisfaite grâce au lemme de coïncidence, parce qu’elle a un nombre fini de variables. Comme les variables sont numérotées, la construction n’a pas besoin de l’axiome du choix. De la compacité découlent ses formes équivalentes (un ensemble est insatisfaisable si et seulement si une de ses parties finies l’est ; une formule est conséquence d’un ensemble si et seulement si elle l’est d’une partie finie) et, avec la complétude pour les ensembles finis de prémisses de la leçon précédente, la complétude forte : Γ⊨φ\Gamma \models \varphi implique Γ⊢φ\Gamma \vdash \varphi pour tout ensemble Γ\Gamma, d’où il suit que la déduction et la conséquence sémantique coïncident toujours. La leçon se termine par des applications combinatoires : la coloration de graphes infinis à partir de celles de leurs parties finies, les bornes finies qui se cachent dans les énoncés infinis et les limites de ce qu’un ensemble de formules peut exprimer.

Objectifs d’apprentissage

  1. Définir les ensembles finiment satisfaisables et démontrer le théorème de compacité en fixant successivement les valeurs des variables, en expliquant le rôle de l’invariant, de l’argument des deux témoins et du lemme de coïncidence, et pourquoi la construction n’a pas besoin de l’axiome du choix.
  2. Énoncer, démontrer et appliquer les formes équivalentes de la compacité, celle de l’insatisfaisabilité et celle de la conséquence, et passer de chacune aux autres.
  3. Déduire la complétude forte de la compacité, de la complétude pour les ensembles finis de prémisses et de la monotonie, et en tirer la coïncidence de la déduction avec la conséquence sémantique et de la cohérence avec la satisfaisabilité.
  4. Coder dans des ensembles de formules des problèmes combinatoires sur des ensembles infinis (colorations, ordres, couplages) et les résoudre par la compacité, en distinguant ce que le théorème assure de ce qu’il n’assure pas.

Ce que l’on utilise des leçons précédentes

Cette leçon travaille presque entièrement dans la sémantique, et en utilise ce qui suit. Une valuation est une fonction v ⁣:V→{0,1}v\colon V \to \{0, 1\} sur l’ensemble VV des variables v1,v2,v3,…v_1, v_2, v_3, \ldots, qui se prolonge d’une seule manière à toutes les formules ; une valuation satisfait un ensemble Γ\Gamma de formules, v⊨Γv \models \Gamma, si elle donne la valeur 11 à chacune d’elles, et Γ\Gamma est satisfaisable si une valuation au moins le satisfait, et insatisfaisable dans le cas contraire. Tout cela se trouve dans la leçon sur la sémantique de la logique propositionnelle, avec l’instrument central de cette leçon, le lemme de coïncidence : si deux valuations coïncident sur les variables de φ\varphi, qui forment un ensemble fini V(φ)V(\varphi), elles donnent à φ\varphi la même valeur.

De la leçon sur la conséquence et l’équivalence sémantiques, on utilise la définition de Γ⊨φ\Gamma \models \varphi (toute valuation qui satisfait Γ\Gamma satisfait φ\varphi), ses propriétés structurelles, en particulier la monotonie (si Γ⊆Δ\Gamma \subseteq \Delta et Γ⊨φ\Gamma \models \varphi, alors Δ⊨φ\Delta \models \varphi) et la cinquième (un ensemble insatisfaisable a pour conséquence toute formule), et le théorème conséquence et insatisfaisabilité : Γ⊨φ\Gamma \models \varphi si et seulement si Γ∪{¬φ}\Gamma \cup \{\neg\varphi\} est insatisfaisable. De la leçon sur les lois généralisées de De Morgan et de distributivité, on utilise le lemme de la valeur : ⋀i=1nφi\bigwedge_{i=1}^{n} \varphi_i vaut 11 si et seulement si tous ses termes valent 11, et ⋁i=1nφi\bigvee_{i=1}^{n} \varphi_i, si et seulement si l’un d’eux vaut 11. Enfin, ⊤:=(v1→v1)\top := (v_1 \rightarrow v_1) est une tautologie et ⊥:=¬⊤\bot := \neg\top, une antilogie.

Du côté de la déduction, la leçon sur les systèmes déductifs formels a démontré la monotonie (Mon : si Γ⊆Δ\Gamma \subseteq \Delta et Γ⊢φ\Gamma \vdash \varphi, alors Δ⊢φ\Delta \vdash \varphi) et la finitude (Fin : si Γ⊢φ\Gamma \vdash \varphi, un sous-ensemble fini Γ0\Gamma_0 de Γ\Gamma vérifie Γ0⊢φ\Gamma_0 \vdash \varphi), et la leçon sur les quatre techniques de déduction a vérifié que toutes deux valent dans le système du cours (les schémas A1, A2 et A3, le modus ponens et le remplacement de la double négation, RDN), auquel renvoie désormais le symbole ⊢\vdash. Enfin, la leçon sur la correction et la complétude a démontré le théorème de correction (Γ⊢φ\Gamma \vdash \varphi implique Γ⊨φ\Gamma \models \varphi, pour tout Γ\Gamma) et la complétude pour les ensembles finis de prémisses : si {γ1,…,γk}⊨φ\{\gamma_1, \ldots, \gamma_k\} \models \varphi, alors {γ1,…,γk}⊢φ\{\gamma_1, \ldots, \gamma_k\} \vdash \varphi.