From d326bf649c0867d99d5fd4463d71d0a6f11cdc53 Mon Sep 17 00:00:00 2001 From: jsboige Date: Wed, 23 Sep 2026 10:07:45 +0200 Subject: [PATCH] =?UTF-8?q?feat(lean,#15062):=20FairBot=20par=20le=20th?= =?UTF-8?q?=C3=A9or=C3=A8me=20de=20L=C3=B6b=20prouv=C3=A9=20=E2=80=94=20Fo?= =?UTF-8?q?rmalLogic.FairBotLoeb=20(L3)?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Module consommateur L3 de l'EPIC #15062 dans le lake formal_logic_lean : la coopération FairBot x FairBot est déduite du théorème de Löb que FFL prouve (ProvabilityAbstraction.löb_theorem), sans champ postulé. - section abstraite : tout prédicat de prouvabilité D1-D3 sur une théorie diagonalisable — auto-coopération, coopération mutuelle, non-exploitabilité (Kreisel), CooperateBot, DefectBot, défection non prouvable (Gödel II), ContrarianBot indépendant ; - instanciation arithmétique : prouvabilité standard de PA, paire de FairBots de codes distincts (exclusiveMultifixedpoint), défection vraie dans le modèle standard (SoundOn). Build local du lake complet : 1403 jobs, 0 warning FormalLogic ; distinct_code_sorry 0 -> 0 ; axiomes propext / Classical.choice / Quot.sound. README : audit fichier entier (dépendance ModalLogic, pin LeanTypst 2158f3de, entrées FolBridge / ModalBridge / FairBotLoeb). See #15062 See #15066 Co-Authored-By: Claude Opus 5 (1M context) --- .../Lean/formal_logic_lean/FormalLogic.lean | 5 + .../FormalLogic/FairBotLoeb.lean | 249 ++++++++++++++++++ .../Lean/formal_logic_lean/README.md | 55 +++- 3 files changed, 300 insertions(+), 9 deletions(-) create mode 100644 MyIA.AI.Notebooks/SymbolicAI/Lean/formal_logic_lean/FormalLogic/FairBotLoeb.lean diff --git a/MyIA.AI.Notebooks/SymbolicAI/Lean/formal_logic_lean/FormalLogic.lean b/MyIA.AI.Notebooks/SymbolicAI/Lean/formal_logic_lean/FormalLogic.lean index befda0aa31..5277633ceb 100644 --- a/MyIA.AI.Notebooks/SymbolicAI/Lean/formal_logic_lean/FormalLogic.lean +++ b/MyIA.AI.Notebooks/SymbolicAI/Lean/formal_logic_lean/FormalLogic.lean @@ -20,9 +20,14 @@ Modules consommateurs : `ModalLogic` (fork compat 4.33.1) — `K` valide sur tout cadre, contre-modèles finis de `T`/`4`/`5` sur cadres témoins génériques, duaux diamant de `T`/`4` sur les cadres S4 de Fin74. +- `FormalLogic.FairBotLoeb` — niveau L3 de l'EPIC #15062 : FairBot × FairBot + déduit du théorème de Löb **prouvé** par FFL (`ProvabilityAbstraction.löb_theorem`), + sans champ postulé, instancié sur la prouvabilité standard de `𝗣𝗔` ; paire de + FairBots de codes distincts par `exclusiveMultifixedpoint`. -/ import FormalLogic.Bridge import FormalLogic.FolBridge import FormalLogic.GLBridge import FormalLogic.ModalBridge +import FormalLogic.FairBotLoeb diff --git a/MyIA.AI.Notebooks/SymbolicAI/Lean/formal_logic_lean/FormalLogic/FairBotLoeb.lean b/MyIA.AI.Notebooks/SymbolicAI/Lean/formal_logic_lean/FormalLogic/FairBotLoeb.lean new file mode 100644 index 0000000000..e93ab7c281 --- /dev/null +++ b/MyIA.AI.Notebooks/SymbolicAI/Lean/formal_logic_lean/FormalLogic/FairBotLoeb.lean @@ -0,0 +1,249 @@ +import Foundation.FirstOrder.Incompleteness.Löb +import Foundation.FirstOrder.Incompleteness.Definability + +/-! +# FairBot par le théorème de Löb *prouvé* (L3, EPIC #15062) + +Troisième niveau de l'équilibre en programmes pour le Dilemme du Prisonnier. +Le niveau L2 (`game_theory_lean/ProgramGames/FairBot.lean`) raisonne sur une +interface `ModalProvability box` dont le schéma de Löb est un **champ postulé** : +ses quatre champs sont `nec` (D1), `dist` (D2), `posIntros` (D3) et `loeb`. La +modalité témoin `bump` de L2 montre que ce champ n'est pas redondant : D1, D2 et +D3 seules ne donnent pas Löb. + +Ce module consomme directement la bibliothèque *Formalized Formal Logic* (FFL, +paquet `Foundation` épinglé par le lakefile), où le théorème de Löb n'est plus +un champ mais un **théorème** : `ProvabilityAbstraction.löb_theorem`, démontré +par le point fixe de Kreisel. Correspondance champ par champ avec L2 : + +| L2 (`ModalProvability`) | L3 (FFL) | Statut dans ce module | +|---|---|---| +| `nec` (D1) | `Provability.bew_def` / `Provability.D1` | champ de la structure `Provability` | +| `dist` (D2) | classe `Provability.HBL2` | hypothèse de classe | +| `posIntros` (D3) | classe `Provability.HBL3` | hypothèse de classe | +| `loeb` | `ProvabilityAbstraction.löb_theorem` | **théorème**, aucun champ | + +L'ingrédient qui manque à L2 n'est donc pas une quatrième condition de +dérivabilité : c'est le **lemme diagonal** (classe `Diagonalization T₀`), qui +fournit les phrases autoréférentielles. La modalité `bump` de L2 n'en possède +pas, et c'est exactement pour cela que Löb y échoue. + +## Contenu + +* **Section abstraite**, pour toute théorie `T` munie d'un prédicat de + prouvabilité `𝔅` satisfaisant les conditions de Hilbert–Bernays–Löb + relativement à une théorie de base diagonalisante `T₀` : + - `fairBot_self_cooperation` : FairBot contre sa propre copie coopère ; + - `fairBot_mutual_cooperation` : deux FairBots **quelconques**, décrits par + des équations croisées `p ↔ 𝔅 q` et `q ↔ 𝔅 p`, coopèrent — aucune identité + syntaxique n'est requise ; + - `fairBot_unexploitable` : sous la condition de Kreisel, la coopération + prouvée de FairBot entraîne celle de l'adversaire ; + - `fairBot_vs_cooperateBot`, `fairBot_vs_defectBot` et + `fairBot_vs_defectBot_defection_unprovable` : la défection contre + DefectBot est vraie mais **indémontrable dans `T`**, lecture ludique du + second théorème d'incomplétude ; + - `contrarianBot_independent` : contrôle négatif — même diagonale, signe + inversé, destin opposé (phrase de Gödel, indépendante). +* **Section arithmétique**, instanciée sur la prouvabilité standard de FFL + (`Theory.standardProvability`, base `𝗜𝚺₁`) : + - `pa_fairBot_self_cooperation` : `𝗣𝗔` prouve la coopération de FairBot avec + lui-même, sans aucune hypothèse restante ; + - `fairBotA` / `fairBotB` : une paire de FairBots de **codes distincts** + (`fairBotA_ne_fairBotB`), obtenue par `exclusiveMultifixedpoint`, dont + `pa_fairBot_pair_cooperation` établit la coopération mutuelle ; + - `pa_fairBot_vs_defectBot` et `pa_fairBot_defects_in_standard_model` : contre + DefectBot, `𝗣𝗔` ne prouve ni la coopération ni la défection de FairBot, + alors que la défection est vraie dans `ℕ`. + +Références : + - Barasz, Christiano, Fallenstein, Herreshoff, LaVictor, Yudkowsky (2014), + « Robust Cooperation in the Prisoner's Dilemma: Program Equilibrium via + Provability Logic », arXiv:1401.5577 ; + - Critch (2016), « Parametric Bounded Löb's Theorem and Robust Cooperation + of Bounded Agents », arXiv:1602.04184 ; + - pont GL du même lake : `FormalLogic.GLBridge` (#15923), niveau L2 : + `ProgramGames.FairBot` (#16414). +-/ + +open FFL FFL.Entailment FFL.FirstOrder + +namespace FormalLogic.FairBotLoeb + +/-! ## Section abstraite : toute prouvabilité de Hilbert–Bernays–Löb -/ + +section Abstract + +open ProvabilityAbstraction Diagonalization Provability + +variable {L : Language} [L.ReferenceableBy L] [L.DecidableEq] + {T₀ T : Theory L} [Diagonalization T₀] [T₀ ⪯ T] + +/-- FairBot face à sa propre copie : la phrase `F` telle que `F ↔ 𝔅 F` +(« je coopère ssi ma coopération est prouvable »). C'est la phrase de Henkin, +obtenue par le lemme diagonal de la théorie de base `T₀`. -/ +def fairBotSelf (𝔅 : Provability T₀ T) : Sentence L := + fixedpoint T₀ “x. !𝔅.prov x” + +variable {𝔅 : Provability T₀ T} + +omit [L.DecidableEq] [T₀ ⪯ T] in +/-- Clause de FairBot face à lui-même, prouvée dans la théorie de base. -/ +lemma fairBotSelf_spec : T₀ ⊢ fairBotSelf 𝔅 🡘 𝔅 (fairBotSelf 𝔅) := by + simpa [fairBotSelf, Provability.pr] using diag (T := T₀) “x. !𝔅.prov x” + +/-- FairBot × FairBot (même code) : la coopération est prouvable dans `T`. +Une seule application de Löb suffit, sur la moitié `𝔅 F 🡒 F` de la clause. -/ +theorem fairBot_self_cooperation [𝔅.HBL] : T ⊢ fairBotSelf 𝔅 := + ProvabilityAbstraction.löb_theorem (WeakerThan.pbl (K_right fairBotSelf_spec)) + +/-- Coopération mutuelle de deux FairBots arbitraires, dérivation de +Barasz et al. (2014). Les phrases `p` et `q` ne sont soumises qu'aux clauses +croisées `p ↔ 𝔅 q` et `q ↔ 𝔅 p` : deux programmes syntaxiquement distincts +mais prouvablement équivalents à FairBot coopèrent. Löb s'applique à la +conjonction `p ⋏ q`, en distribuant `𝔅` sur la conjonction (D2). -/ +theorem fairBot_mutual_cooperation [𝔅.HBL] {p q : Sentence L} + (hp : T₀ ⊢ p 🡘 𝔅 q) (hq : T₀ ⊢ q 🡘 𝔅 p) : T ⊢ p ⋏ q := by + apply ProvabilityAbstraction.löb_theorem (𝔅 := 𝔅) + have hd : T₀ ⊢ 𝔅 (p ⋏ q) 🡒 𝔅 p ⋏ 𝔅 q := bew_distribute_and + have h : T₀ ⊢ 𝔅 (p ⋏ q) 🡒 p ⋏ q := by cl_prover [hd, hp, hq] + exact WeakerThan.pbl h + +omit [L.DecidableEq] [Diagonalization T₀] in +/-- Inexploitabilité : si `T` prouve que FairBot coopère, `T` prouve que +l'adversaire coopère. L'hypothèse de Kreisel (`T ⊢ 𝔅 σ → T ⊢ σ`) est la +contrepartie syntaxique de la fiabilité locale `box r → r` de L2 ; pour la +prouvabilité standard, elle découle de la correction de `T` sur les énoncés +𝚺₁. -/ +theorem fairBot_unexploitable [𝔅.Kreisel] {p q : Sentence L} + (hp : T₀ ⊢ p 🡘 𝔅 q) (h : T ⊢ p) : T ⊢ q := + 𝔅.KR ((WeakerThan.pbl (K_left hp)) ⨀ h) + +omit [L.DecidableEq] [Diagonalization T₀] in +/-- FairBot contre CooperateBot (la phrase `⊤`) : coopération sans hypothèse, +par nécessitation (D1) appliquée à `⊤`. -/ +theorem fairBot_vs_cooperateBot {p : Sentence L} (hp : T₀ ⊢ p 🡘 𝔅 ⊤) : T ⊢ p := + WeakerThan.pbl ((K_right hp) ⨀ (D1 (by simp))) + +omit [L.DecidableEq] [Diagonalization T₀] in +/-- FairBot contre DefectBot (la phrase `⊥`) : si `T` est cohérente et +satisfait Kreisel, `T` ne prouve pas que FairBot coopère. -/ +theorem fairBot_vs_defectBot [Consistent T] [𝔅.Kreisel] {p : Sentence L} + (hp : T₀ ⊢ p 🡘 𝔅 ⊥) : T ⊬ p := by + intro h + have hbot : T ⊢ ⊥ := fairBot_unexploitable hp h + have : ¬Consistent T := + not_consistent_iff_inconsistent.mpr <| inconsistent_iff_provable_bot.mpr hbot + contradiction + +/-- … mais `T` ne prouve pas non plus que FairBot **dévie** : la défection +équivaut à `∼𝔅 ⊥`, c'est-à-dire à la cohérence `𝔅.con`, que `T` ne prouve pas +(second théorème d'incomplétude, `con_unprovable`). Pour `𝗣𝗔`, la défection +est pourtant l'issue réelle : voir `pa_fairBot_defects_in_standard_model`. -/ +theorem fairBot_vs_defectBot_defection_unprovable [Consistent T] [𝔅.HBL] + {p : Sentence L} (hp : T₀ ⊢ p 🡘 𝔅 ⊥) : T ⊬ ∼p := by + intro h + have hp' : T ⊢ p 🡘 𝔅 ⊥ := WeakerThan.pbl hp + have hcon : T ⊢ ∼𝔅 ⊥ := by cl_prover [h, hp'] + exact con_unprovable (𝔅 := 𝔅) hcon + +/-- Contrôle négatif : le « bot contrariant », qui coopère ssi sa coopération +n'est **pas** prouvable, est exactement la phrase de Gödel `gödel 𝔅` +(`G ↔ ∼𝔅 G`). Même lemme diagonal que `fairBotSelf`, signe inversé : là où +FairBot coopère prouvablement, le contrariant est indépendant de `T`. -/ +theorem contrarianBot_independent [Consistent T] [𝔅.Kreisel] : + Independent T (gödel 𝔅) := + gödel_independent + +end Abstract + +/-! ## Section arithmétique : prouvabilité standard de FFL -/ + +section Arithmetic + +open Arithmetic ProvabilityAbstraction + +variable (T : ArithmeticTheory) [T.Δ₁] [𝗜𝚺₁ ⪯ T] + +/-- FairBot contre lui-même pour la prouvabilité standard de `T`, base `𝗜𝚺₁`. -/ +theorem standard_fairBot_self_cooperation : + T ⊢ fairBotSelf T.standardProvability := + fairBot_self_cooperation + +/-- Corollaire sans hypothèse restante : `𝗣𝗔` prouve la coopération de +FairBot avec sa propre copie. -/ +theorem pa_fairBot_self_cooperation : + 𝗣𝗔 ⊢ fairBotSelf 𝗣𝗔.standardProvability := + standard_fairBot_self_cooperation 𝗣𝗔 + +/-- Corps des deux FairBots de la paire : le bot `0` coopère ssi la +coopération du bot `1` est prouvable (`#1`), et réciproquement (`#0`). -/ +noncomputable def fairBotPairBody : Fin 2 → ArithmeticSemisentence 2 := + ![T.standardProvability.prov/[#1], T.standardProvability.prov/[#0]] + +/-- Premier FairBot de la paire, point fixe multiple exclusif d'indice `0`. -/ +noncomputable def fairBotA : ArithmeticSentence := + exclusiveMultifixedpoint (fairBotPairBody T) 0 + +/-- Second FairBot de la paire, point fixe multiple exclusif d'indice `1`. -/ +noncomputable def fairBotB : ArithmeticSentence := + exclusiveMultifixedpoint (fairBotPairBody T) 1 + +omit [𝗜𝚺₁ ⪯ T] in +/-- Les deux FairBots ont des codes distincts : la coopération mutuelle +ci-dessous ne repose sur aucune identité syntaxique entre les programmes. -/ +theorem fairBotA_ne_fairBotB : fairBotA T ≠ fairBotB T := by + simp [fairBotA, fairBotB] + +omit [𝗜𝚺₁ ⪯ T] in +/-- Clause du premier FairBot : il coopère ssi le second coopère +prouvablement. -/ +lemma fairBotA_spec : + 𝗜𝚺₁ ⊢ fairBotA T 🡘 T.standardProvability (fairBotB T) := by + simpa [fairBotA, fairBotB, fairBotPairBody, Provability.pr, + Rew.subst_comp_subst, ← TransitiveRewriting.comp_app, + Matrix.comp_vecCons', Matrix.constant_eq_singleton] using! + exclusiveMultidiagonal (T := 𝗜𝚺₁) (fairBotPairBody T) (i := 0) + +omit [𝗜𝚺₁ ⪯ T] in +/-- Clause du second FairBot, symétrique. -/ +lemma fairBotB_spec : + 𝗜𝚺₁ ⊢ fairBotB T 🡘 T.standardProvability (fairBotA T) := by + simpa [fairBotA, fairBotB, fairBotPairBody, Provability.pr, + Rew.subst_comp_subst, ← TransitiveRewriting.comp_app, + Matrix.comp_vecCons', Matrix.constant_eq_singleton] using! + exclusiveMultidiagonal (T := 𝗜𝚺₁) (fairBotPairBody T) (i := 1) + +/-- Coopération mutuelle de la paire de codes distincts. -/ +theorem standard_fairBot_pair_cooperation : + T ⊢ fairBotA T ⋏ fairBotB T := + fairBot_mutual_cooperation (fairBotA_spec T) (fairBotB_spec T) + +/-- Corollaire sans hypothèse restante sur `𝗣𝗔`. -/ +theorem pa_fairBot_pair_cooperation : + 𝗣𝗔 ⊢ fairBotA 𝗣𝗔 ⋏ fairBotB 𝗣𝗔 := + standard_fairBot_pair_cooperation 𝗣𝗔 + +/-- FairBot contre DefectBot dans `𝗣𝗔` : sa clause de coopération est `□⊥`. +`𝗣𝗔` ne prouve ni que FairBot coopère, ni qu'il dévie. -/ +theorem pa_fairBot_vs_defectBot : + 𝗣𝗔 ⊬ 𝗣𝗔.standardProvability ⊥ ∧ 𝗣𝗔 ⊬ ∼𝗣𝗔.standardProvability ⊥ := + ⟨fairBot_vs_defectBot (𝔅 := 𝗣𝗔.standardProvability) (by cl_prover), + fairBot_vs_defectBot_defection_unprovable (𝔅 := 𝗣𝗔.standardProvability) + (by cl_prover)⟩ + +/-- … et pourtant FairBot dévie **réellement** contre DefectBot : sa clause +`□⊥` est fausse dans le modèle standard `ℕ`, par correction de la prouvabilité +standard (`Provability.SoundOn ℕ`) et cohérence de `𝗣𝗔`. L'issue (D, D) est +vraie dans `ℕ` sans être un théorème de `𝗣𝗔`. -/ +theorem pa_fairBot_defects_in_standard_model : + ¬ (ℕ↓[ℒₒᵣ] ⊧ 𝗣𝗔.standardProvability ⊥) := by + intro h + have hbot : 𝗣𝗔 ⊢ ⊥ := + Provability.SoundOn.sound_on (𝔅 := 𝗣𝗔.standardProvability) h + exact not_consistent_iff_inconsistent.mpr + (inconsistent_iff_provable_bot.mpr hbot) inferInstance + +end Arithmetic + +end FormalLogic.FairBotLoeb diff --git a/MyIA.AI.Notebooks/SymbolicAI/Lean/formal_logic_lean/README.md b/MyIA.AI.Notebooks/SymbolicAI/Lean/formal_logic_lean/README.md index 350866b655..b677d5daac 100644 --- a/MyIA.AI.Notebooks/SymbolicAI/Lean/formal_logic_lean/README.md +++ b/MyIA.AI.Notebooks/SymbolicAI/Lean/formal_logic_lean/README.md @@ -11,10 +11,15 @@ mêmes formules avec le noyau Lean via la bibliothèque |---|---|---| | `FormalizedFormalLogic/Foundation` | `81810b9f` | syntaxe/sémantique propositionnelles et métathéorie arithmétique | | `FormalizedFormalLogic/ProvabilityLogic` | `01628c51` | calcul GL, modèles de Kripke finis, points fixes et interprétation arithmétique | +| `MyIntelligenceAgency/ModalLogic` | `71968137` | cadres de Kripke génériques et cadres S4 finis (fork de compatibilité v4.33.1 de l'upstream `9c485ca9`, trois commits sans changement sémantique) | | `mathlib4` | `v4.33.1` | transitif commun et toolchain du lake | -Aucun module upstream n'est vendu ou adapté ici : les deux bibliothèques sont -consommées à des commits exacts. Le nom Lake `Foundation`, sensible à la casse, +Aucun module upstream n'est vendu ou adapté ici : les trois bibliothèques sont +consommées à des commits exacts. Pour `ModalLogic`, l'upstream reste en Lean +4.31.0 ; le lake consomme donc un fork qui ne porte que la compatibilité avec la +toolchain 4.33.1 (le détail est dans le commentaire du `lakefile.lean`). +`require mathlib` reste en dernier, pour que les révisions transitives soient +celles de mathlib v4.33.1 et non celles du manifeste 4.31 de `ModalLogic`. Le nom Lake `Foundation`, sensible à la casse, est déclaré à la racine afin que le pin `81810b9f` remplace bien la dépendance transitive de même nom de `ProvabilityLogic`, plutôt que de cloner deux copies. @@ -22,14 +27,21 @@ Le verdict du pilote #15916 est **CONSUMER_PINNÉ** : l'API upstream suffit sans port ni adaptation locale. La fermeture propositionnelle historique reste légère (17 modules, mesure du pilote #15520). Le fragment GL modal a compilé 1107 jobs ; le module `FormalLogic.GLBridge`, puis le lake complet avec sa fermeture -arithmétique, ont compilé respectivement 1356 et 1361 jobs. L'import arithmétique -est volontairement isolé dans `GLBridge` : il apporte les développements -FirstOrder, Arithmetic et Incompleteness nécessaires au théorème de correction -arithmétique. +arithmétique, ont compilé respectivement 1356 et 1361 jobs. Mesure du 2026-09-23, +après l'ajout de `ModalBridge` et de `FairBotLoeb` : le lake complet compile +1403 jobs, et `FormalLogic.FairBotLoeb` seul 1225. -`Foundation` et `ProvabilityLogic` déclarent Apache-2.0. Deux dépendances -transitives nouvelles, `Forgive@32667a19` et `LeanTypst@888d8656`, ne portent -aucun fichier de licence racine détecté à ces pins. Elles ne sont pas vendues +L'import arithmétique reste cantonné à deux modules. `GLBridge` en a besoin pour +le théorème de correction arithmétique ; `FairBotLoeb` importe directement +`Foundation.FirstOrder.Incompleteness`, pour instancier le théorème de Löb sur la +prouvabilité standard de 𝗣𝗔. `FolBridge` n'importe que la logique du premier +ordre (sémantique, correction, complétude), sans arithmétique. + +`Foundation`, `ProvabilityLogic` et `ModalLogic` déclarent Apache-2.0. Deux +dépendances transitives, `Forgive@32667a19` et `LeanTypst@2158f3de`, ne portent +aucun fichier de licence racine détecté à ces pins (vérifié le 2026-09-23 ; le +pin de `LeanTypst` est passé de `888d8656` à `2158f3de` avec l'ajout de +`ModalLogic`, #17017). Elles ne sont pas vendues dans CoursIA, mais ce caveat doit être levé avant toute redistribution autonome de la fermeture complète. @@ -42,11 +54,36 @@ de la fermeture complète. `peirce_valid` (validité par exhaustivité de la table), le contre-modèle `or_not_valid`, le contrôle négatif satisfiable-non-valide, et `peirce_provable` (versant preuve, reprise de `FFL.Entailment.peirce`). +- `FormalLogic/FolBridge.lean` — versant Lean du notebook + `Tweety-02d-FOL-Lab-Lean.ipynb` : la même micro-théorie du premier ordre + (quatre prédicats unaires, deux constantes). `KB ⊨ Mortel(socrate)` y devient + un théorème de conséquence sémantique. Un contre-modèle fini à deux éléments + montre que les deux existentiels ne fusionnent pas en un témoin unique, et que + `∀X Mortel(X)` n'est pas conséquence. - `FormalLogic/GLBridge.lean` — le schéma de Löb dérivé dans le calcul de Hilbert, une instance concrète de membership, la disponibilité de la décision GL sans `native_decide`, un contre-modèle fini certifiant que `¬□⊥` n'est pas un théorème, une spécialisation du point fixe de de Jongh–Sambin et le pont vers la correction arithmétique sous les conditions de Hilbert–Bernays–Löb. +- `FormalLogic/ModalBridge.lean` — l'axiome `K` est valide sur tout cadre de + Kripke. `T`, `4` et `5` échouent chacun sur un cadre témoin qui viole + exactement sa condition (irréflexif, non transitif, non euclidien) ; ce sont + des contre-modèles certifiés par le noyau. Sur les cadres réflexifs et + transitifs de `Fin74`, les duaux diamant de `T` et `4` sont des théorèmes. +- `FormalLogic/FairBotLoeb.lean` — la coopération FairBot × FairBot du + dilemme du prisonnier entre programmes (Barasz et al., 2014) est déduite du + théorème de Löb que FFL **prouve** (`ProvabilityAbstraction.löb_theorem`), et + non d'un champ postulé. Le résultat est d'abord abstrait (tout prédicat de + prouvabilité vérifiant D1–D3 sur une théorie diagonalisable), puis instancié + sur la prouvabilité standard de 𝗣𝗔. Le module contient aussi une paire de + FairBots de **codes distincts** (`exclusiveMultifixedpoint`). Il établit que + FairBot n'est pas exploitable (sous l'hypothèse de Kreisel), qu'il coopère + avec CooperateBot, et qu'il n'est pas prouvable face à DefectBot. Il montre + enfin que la défection n'y est pas prouvable non plus (second théorème de + Gödel), alors qu'elle est vraie dans le modèle standard. La leçon de ce + module : une modalité qui vérifie D1–D3 sans lemme diagonal ne donne pas le + théorème de Löb. C'est la `Diagonalization` qui manque, pas une quatrième + condition. La procédure de décision GL est exposée comme instance `Decidable`. Sur le schéma concret de Löb, sa réduction par `decide` reste bloquée dans la réduction