From 8bf1ad9750a980bed41d9f74eb67085cb64a0567 Mon Sep 17 00:00:00 2001 From: jsboige Date: Mon, 21 Sep 2026 04:08:43 +0200 Subject: [PATCH 1/2] =?UTF-8?q?Add:=20Tweety-3b-Modal-Lab-Lean=20=E2=80=94?= =?UTF-8?q?=20labo=20modal=20croise=20Kripke/Lean,=20Tranche=20C=20#15066?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Notebook consommateur du pont FormalLogic.ModalBridge (#17017) : - syntaxe MlParser Tweety reelle (K/T/4/5, bug SPASS #1334 documente) - moteur Kripke Python + balayage exhaustif 512 cadres x toutes valuations : T=non-reflexifs 448, 4=non-transitifs 341, 5=non-euclidiens 473, K=0 (egalites exactes d'ensembles assertees) - 4 certificats kernel Lean via lake env lean (tous exit 0, 0 sorry, #print axioms mesure) + 3 exercices stubbes C.1 - README : entree 3b, comptes re-mesures (companion 3->4, total 34->35), changelog v1.2.4 Papermill : 34/34 cellules, 13/13 code executees, 0 erreur, 0 fuite chemin machine (clean() a la source, lecon #16977). Co-Authored-By: Claude Sonnet 5 --- MyIA.AI.Notebooks/SymbolicAI/Tweety/README.md | 17 +- .../Tweety/Tweety-3b-Modal-Lab-Lean.ipynb | 1768 +++++++++++++++++ 2 files changed, 1778 insertions(+), 7 deletions(-) create mode 100644 MyIA.AI.Notebooks/SymbolicAI/Tweety/Tweety-3b-Modal-Lab-Lean.ipynb diff --git a/MyIA.AI.Notebooks/SymbolicAI/Tweety/README.md b/MyIA.AI.Notebooks/SymbolicAI/Tweety/README.md index d3e2684b95..de52c538b1 100644 --- a/MyIA.AI.Notebooks/SymbolicAI/Tweety/README.md +++ b/MyIA.AI.Notebooks/SymbolicAI/Tweety/README.md @@ -29,7 +29,7 @@ Les notebooks utilisent **deux implémentations** pour exécuter TweetyProject, | Implémentation | Stack | Kernel | JVM requise ? | Notebooks | | ------------------------ | ------------------------------ | ------------- | --------------------------------- | --------------------------------------------------------------------------------------------------------------------------------------- | -| **Python** (originelle) | JPype (pont Java↔Python) | Python 3 | Oui (JDK téléchargé par le setup) | `Tweety-1` à `Tweety-11` (+ `Tweety-5b-Lean-Argumentation` companion Lean 4, `Tweety-5d-Stable-Synthesis-Lean` synthèse Z3→Lean et `Tweety-5e-Propositional-Lab-Lean` laboratoire propositionnel, soit **15 notebooks**) | +| **Python** (originelle) | JPype (pont Java↔Python) | Python 3 | Oui (JDK téléchargé par le setup) | `Tweety-1` à `Tweety-11` (+ `Tweety-5b-Lean-Argumentation` companion Lean 4, `Tweety-5d-Stable-Synthesis-Lean` synthèse Z3→Lean et `Tweety-5e-Propositional-Lab-Lean` laboratoire propositionnel et `Tweety-3b-Modal-Lab-Lean` laboratoire modal, soit **16 notebooks**) | | **C#/.NET** (port natif) | IKVM 8.14 (bytecode Java→.NET) | `.net-csharp` | **Non** (runtime IKVM pur .NET) | **18 notebooks** `*-Csharp` (de `Tweety-2-Basic-Logics-Csharp` à `Tweety-11-Causal-Csharp` ; ex. `2b-Semantics`, `3-Dung`, `4-Aspic`) | Les deux implémentations couvrent les mêmes concepts fondamentaux (logique propositionnelle, sémantique des mondes possibles, logique du premier ordre, argumentation de Dung) ; le port C# les expose **sans JVM**, directement dans le runtime .NET, ce qui les rend exécutables côté .NET Interactive comme n'importe quel notebook C#. Les notebooks `-Csharp` vivent **à côté** de leurs homologues Python (pas dans un sous-dossier), pour faciliter la comparaison des deux stacks sur un même concept. Voir EPIC [#4667](https://github.com/jsboige/CoursIA/issues/4667). @@ -148,6 +148,7 @@ Pour les praticiens intéressés par les applications multi-agents : | 2b | [Tweety-2b-Semantics-Csharp](Tweety-02b-Semantics-CSharp.ipynb) | Sémantique propositionnelle .NET (mondes possibles) | 30 min | C# BETA | | 2c | [Tweety-2c-FOL-Csharp](Tweety-02c-FOL-CSharp.ipynb) | FOL porté .NET (IKVM) | 30 min | C# BETA | | 3 | [Tweety-3-Advanced-Logics](Tweety-3-Advanced-Logics.ipynb) | DL, Modale, QBF, Conditionnelle | 40 min | Python | +| 3b | [Tweety-3b-Modal-Lab-Lean](Tweety-3b-Modal-Lab-Lean.ipynb) | Labo modal croisé (tranche C de l'EPIC #15066) : schémas `K`/`T`/`4`/`5` — syntaxe `MlParser` Tweety (bug SPASS #1334 documenté), balayage exhaustif des 512 cadres 3-mondes en Python (correspondances T/réflexif, 4/transitif, 5/euclidien mesurées en égalités exactes), certificats du kernel Lean sur le pont `FormalLogic.ModalBridge` (#17017) | 45 min | Python+Lean BETA | | 3c-DL | [Tweety-3-Advanced-Logics-Csharp](Tweety-3-Advanced-Logics-Csharp.ipynb) | DL/ML/QBF/CL .NET (DRAFT - conflits DLL) | 30 min | C# DRAFT | | 3c-CL | [Tweety-3-Conditional-Logics-Csharp](Tweety-3-Conditional-Logics-Csharp.ipynb) | Logique conditionnelle .NET (IKVM) | 25 min | C# PROD | | 3c-Dung | [Tweety-3-Dung-Csharp](Tweety-3-Dung-Csharp.ipynb) | Argumentation de Dung .NET (IKVM, c.182 PR #5194) | 25 min | C# PROD | @@ -180,11 +181,11 @@ Pour les praticiens intéressés par les applications multi-agents : | 11 | [Tweety-11-Causal](Tweety-11-Causal.ipynb) | Raisonnement causal : do-calculus, interventions, contrefactuels | 50 min | Python | | 11c | [Tweety-11-Causal-Csharp](Tweety-11-Causal-Csharp.ipynb) | Twin C# moteur causal booléen from-scratch (do-operator, contrefactuel) | 35 min | C# PROD | -**Durée totale estimée** : ~13h (Python) + ~7h (C#/.NET). Le tableau ci-dessus couvre les **33 notebooks principaux** (12 Python + 18 C#/.NET + 3 Lean companion) ; voir aussi `_probes/Tweety-IKVM-Init-Probe.ipynb` (BETA smoke-test IKVM) et `argumentation_lean/` (lake Lean 4, toolchain `v4.32.1` depuis #11587, avec 12 fichiers `.lean` au dossier `Argumentation/` — 6 modules FR : Basic, Characteristic, Extensions, Fundamental, Grounded, Synthesis + leurs 6 siblings `_en` i18n #4980). +**Durée totale estimée** : ~13h (Python) + ~7h (C#/.NET). Le tableau ci-dessus couvre les **34 notebooks principaux** (12 Python + 18 C#/.NET + 4 Lean companion) ; voir aussi `_probes/Tweety-IKVM-Init-Probe.ipynb` (BETA smoke-test IKVM) et `argumentation_lean/` (lake Lean 4, toolchain `v4.32.1` depuis #11587, avec 12 fichiers `.lean` au dossier `Argumentation/` — 6 modules FR : Basic, Characteristic, Extensions, Fundamental, Grounded, Synthesis + leurs 6 siblings `_en` i18n #4980). ## En quoi chaque notebook est unique -Chaque notebook introduit un concept ou cadre théorique spécifique. Le tableau ci-dessous résume en une ligne l'apport pédagogique de chacun — couvrant les **33 notebooks principaux** (12 Python + 18 C#/.NET + 3 Lean companion) : +Chaque notebook introduit un concept ou cadre théorique spécifique. Le tableau ci-dessous résume en une ligne l'apport pédagogique de chacun — couvrant les **34 notebooks principaux** (12 Python + 18 C#/.NET + 4 Lean companion) : | # | Notebook | Concept clé enseigné | |----|-------------------------------|--------------------------------------------------------------------------| @@ -194,6 +195,7 @@ Chaque notebook introduit un concept ou cadre théorique spécifique. Le tableau | 2b | Semantics (C#) | Sémantique propositionnelle .NET (mondes possibles) — port IKVM 8.14 | | 2c | Basic Logics (C#) | FOL porté .NET via IKVM 8.14 : `tweetyproject.logics.fol.*` réel | | 3 | Advanced Logics | Ontologies OWL (DL) + raisonnement modale (SPASS) + QBF | +| 3b | Modal Lab (Python+Lean) | Théorie de la correspondance mesurée : énumération exhaustive 512 cadres ↔ contre-modèles kernel-vérifiés (pont ModalBridge) | | 3c-DL | Advanced Logics (C#) | DL/ML/QBF/CL .NET — **DRAFT** : conflits de noms DLL entre `logics.ml` + `logics.cl` + `logics.qbf` simultanés | | 3c-CL | Conditional Logics (C#) | Logique conditionnelle .NET (IKVM) — raisonneur `cl` réel | | 3c-Dung | Dung (C#) | Argumentation de Dung .NET (IKVM, c.182 PR #5194) — `NaiveDlReasoner` | @@ -400,6 +402,7 @@ Tweety/ ├── Tweety-02b-Semantics-CSharp.ipynb # Sémantique propositionnelle .NET (IKVM, BETA) ├── Tweety-02c-FOL-CSharp.ipynb # FOL .NET (IKVM, BETA) ├── Tweety-3-Advanced-Logics.ipynb # DL, ML, QBF, CL +├── Tweety-3b-Modal-Lab-Lean.ipynb # Labo modal croisé Kripke/Lean (tranche C #15066) ├── Tweety-3-Advanced-Logics-Csharp.ipynb # DL/ML/QBF/CL .NET (DRAFT — conflits DLL) ├── Tweety-3-Conditional-Logics-Csharp.ipynb # Logique conditionnelle .NET (IKVM, PROD) ├── Tweety-3-Dung-Csharp.ipynb # Argumentation de Dung .NET (IKVM, PROD) @@ -734,7 +737,7 @@ Le pitch de Tweety tient en un mot : **explicabilité**. Là où un LLM produit --- -**Version 1.2.3 — Septembre 2026 — entree README de `Tweety-5e-Propositional-Lab-Lean` (tranche A de l'EPIC #15066, laboratoire propositionnel Tweety/Lean) : table Structure (32 → 33 notebooks principaux), table « En quoi chaque notebook est unique » (ajout de 5d et 5e, 31 → 33 lignes), arbre de structure, statistiques par sous-categorie (Lean companion 2 → 3, total 33 → 34) et colonne Python du tableau des stacks (14 → 15). Residu declare, non comble ici : `Tweety-12-Grounded-Via-TweetyProject` (13e notebook Python, kernel `python3`, execute 8/8 sans erreur) reste absent des tables — sa duree n'est declaree nulle part dans le notebook, aucune ligne n'a donc ete inventee. Precedent : Version 1.2.2 — Août 2026 — ajout Tweety-5d (synthèse certifiée Z3→Lean, Loi II #12205/#13597) : lake `argumentation_lean` 6+6 siblings `_en` (module `Synthesis`), toolchain corrigée v4.32.1 (#11587), comptes re-mesurés 33 notebooks / 969 cellules dont 390 code (périmètre : 32 `Tweety-*` + 1 probe). Précédent : Version 1.2.1 — re-audit fichier-entier §E : 18 DLLs shades, scripts/ 5+4+`_archive`, pin IKVM 8.14, limitations re-ancrées 1.30. EPIC #3975 tranche tweety.** +**Version 1.2.4 — Septembre 2026 — entree README de `Tweety-3b-Modal-Lab-Lean` (tranche C de l'EPIC #15066, laboratoire modal croise Python/Kripke <-> Lean/ModalBridge #17017) : table Structure (+1 ligne 3b, 33 → 34 notebooks principaux), table « En quoi chaque notebook est unique » (+1 ligne), arbre de structure, statistiques par sous-categorie (Lean companion 3 → 4, total 34 → 35) et colonne Python du tableau des stacks (15 → 16). Residu declare, non comble ici : `Tweety-12-Grounded-Via-TweetyProject` reste absent des tables (duree non declaree, cf. v1.2.3). Precedent : Version 1.2.3 — Septembre 2026 — entree README de `Tweety-5e-Propositional-Lab-Lean` (tranche A de l'EPIC #15066, laboratoire propositionnel Tweety/Lean) : table Structure (32 → 33 notebooks principaux), table « En quoi chaque notebook est unique » (ajout de 5d et 5e, 31 → 33 lignes), arbre de structure, statistiques par sous-categorie (Lean companion 2 → 3, total 33 → 34) et colonne Python du tableau des stacks (14 → 15). Residu declare, non comble ici : `Tweety-12-Grounded-Via-TweetyProject` (13e notebook Python, kernel `python3`, execute 8/8 sans erreur) reste absent des tables — sa duree n'est declaree nulle part dans le notebook, aucune ligne n'a donc ete inventee. Precedent : Version 1.2.2 — Août 2026 — ajout Tweety-5d (synthèse certifiée Z3→Lean, Loi II #12205/#13597) : lake `argumentation_lean` 6+6 siblings `_en` (module `Synthesis`), toolchain corrigée v4.32.1 (#11587), comptes re-mesurés 33 notebooks / 969 cellules dont 390 code (périmètre : 32 `Tweety-*` + 1 probe). Précédent : Version 1.2.1 — re-audit fichier-entier §E : 18 DLLs shades, scripts/ 5+4+`_archive`, pin IKVM 8.14, limitations re-ancrées 1.30. EPIC #3975 tranche tweety.** ## Statistiques catalogue à jour @@ -743,14 +746,14 @@ Statistiques détaillées de la sous-série Tweety. Le `pedagogical_count: 32` e | Sous-catégorie | NB | Statut | |-----------------------|-------|------------------------------| | Python (Tw-1..11) | 12 | PROD=12 | -| Lean companion (5b, 5d, 5e) | 3 | BETA=3 | +| Lean companion (5b, 5d, 5e, 3b) | 4 | BETA=4 | | C#/.NET | 18 | PROD=12, BETA=5, DRAFT=1 | | Probe `_probes/` | 1 | BETA | -| Total | 34 | PROD=24, BETA=9, DRAFT=1 | +| Total | 35 | PROD=24, BETA=10, DRAFT=1 | Détails paradigmes/stacks : -- **Python (JPype, 12 nb)** : PL/FOL/DL/ML/QBF/CL/Dung/ASPIC+/AGM/MLN/do-calculus Pearl — double stack sur Tw-3 (DL+Modale+QBF), Tw-4 (Belief Revision), Tw-7b (Ranking), Tw-9 (vote/préférences), Tw-10 (MLN), Tw-11 (causal). Tous PROD. Voir aussi le companion **Lean** `Tweety-5b-Lean-Argumentation` (BETA, kernel Lean 4, `argumentation_lean/`) et `Tweety-5d-Stable-Synthesis-Lean` (BETA, kernel Python + Z3, Loi II #12205 : spécification → générateur Z3 → témoin → certificat Lean `by decide`), ainsi que `Tweety-5e-Propositional-Lab-Lean` (BETA, kernels Python + Lean, tranche A de l'EPIC #15066 : trois formules-témoins lues par Tweety, recomptées en Python et certifiées sur Foundation (FFL) au commit épinglé). +- **Python (JPype, 12 nb)** : PL/FOL/DL/ML/QBF/CL/Dung/ASPIC+/AGM/MLN/do-calculus Pearl — double stack sur Tw-3 (DL+Modale+QBF), Tw-4 (Belief Revision), Tw-7b (Ranking), Tw-9 (vote/préférences), Tw-10 (MLN), Tw-11 (causal). Tous PROD. Voir aussi le companion **Lean** `Tweety-5b-Lean-Argumentation` (BETA, kernel Lean 4, `argumentation_lean/`) et `Tweety-5d-Stable-Synthesis-Lean` (BETA, kernel Python + Z3, Loi II #12205 : spécification → générateur Z3 → témoin → certificat Lean `by decide`), ainsi que `Tweety-5e-Propositional-Lab-Lean` (BETA, kernels Python + Lean, tranche A de l'EPIC #15066 : trois formules-témoins lues par Tweety, recomptées en Python et certifiées sur Foundation (FFL) au commit épinglé) et `Tweety-3b-Modal-Lab-Lean` (BETA, kernel Python + Lean via WSL, tranche C de l'EPIC #15066 : schémas `K`/`T`/`4`/`5` parsés par `MlParser`, énumérés sur les 512 cadres Kripke 3-mondes puis certifiés par le pont `FormalLogic.ModalBridge` #17017 — réponse sémantique au bug SPASS #1334). - **C#/.NET (IKVM 8.14, 18 nb)** : bytecode Java→.NET downgrade Java 15→8 (post-C190 `JvmDowngrader`), sans JVM. PROD=12, BETA=5 (`Tweety-2b-Semantics-Csharp`, `Tweety-2c-FOL-Csharp`, `Tweety-4-Belief-Revision-Csharp`, `Tweety-4-Aspic-Csharp`, `Tweety-5-Abstract-Argumentation-Csharp`), DRAFT=1 = BROKEN (`Tweety-3-Advanced-Logics-Csharp`, conflits de noms sur `logics.ml` + `logics.cl` + `logics.qbf` simultanés dans la même DLL). - **Probe (`_probes/Tweety-IKVM-Init-Probe`, 1 nb)** : IKVM init smoke-test BETA. diff --git a/MyIA.AI.Notebooks/SymbolicAI/Tweety/Tweety-3b-Modal-Lab-Lean.ipynb b/MyIA.AI.Notebooks/SymbolicAI/Tweety/Tweety-3b-Modal-Lab-Lean.ipynb new file mode 100644 index 0000000000..6a55d4a609 --- /dev/null +++ b/MyIA.AI.Notebooks/SymbolicAI/Tweety/Tweety-3b-Modal-Lab-Lean.ipynb @@ -0,0 +1,1768 @@ +{ + "cells": [ + { + "cell_type": "markdown", + "id": "c0-titre", + "metadata": { + "papermill": { + "duration": 0.00708, + "end_time": "2026-09-21T01:40:38.754370+00:00", + "exception": false, + "start_time": "2026-09-21T01:40:38.747290+00:00", + "status": "completed" + }, + "tags": [] + }, + "source": [ + "# Tweety-3b — Labo Modal : Kripke répond, Lean certifie\n", + "\n", + "> **Série Tweety — laboratoires croisés Java ↔ Python ↔ Lean (EPIC [#15066](https://github.com/jsboige/CoursIA/issues/15066), Tranche C, pont [#17017](https://github.com/jsboige/CoursIA/pull/17017)).**\n", + "> Un même zoo de formules modales, trois moteurs : Tweety (Java, via JPype) **manipule la syntaxe** `[]`/`<>` ;\n", + "> un moteur de Kripke en Python **énumère** cadres et valuations — les conditions de cadre émergent du comptage ;\n", + "> le lake `formal_logic_lean` (pont `FormalLogic.ModalBridge`) **certifie** validité de `K` et contre-modèles\n", + "> de `T`, `4`, `5` comme objets vérifiés par le noyau Lean.\n", + "\n", + "Navigation : [Tweety-3-Advanced-Logics](Tweety-3-Advanced-Logics.ipynb) (tour DL/Modale/QBF/CL) ·\n", + "[Tweety-3c-ModalLogic-Csharp](Tweety-3-ModalLogic-Csharp.ipynb) (port C#) ·\n", + "[Tweety-02d-FOL-Lab-Lean](Tweety-02d-FOL-Lab-Lean.ipynb) (labo FOL, même patron) ·\n", + "[README](README.md)\n", + "\n", + "***\n", + "\n", + "## Objectifs pédagogiques\n", + "\n", + "1. **Manipuler** la syntaxe modale avec le `MlParser` de Tweety — et rencontrer la limite upstream :\n", + " le raisonneur SPASS est cassé pour les formules modalisées ([Issue #1334](https://github.com/TweetyProject/Tweety/issues/1334)),\n", + " le notebook 3 le documente, ce labo le contourne par la **sémantique**, pas par l'abandon\n", + "2. **Exécuter** une sémantique de Kripke complète en Python : forcing `x |= f`, clause `[]` = « pour tout successeur »,\n", + " `<>` = « il existe »\n", + "3. **Mesurer** la théorie de la correspondance par balayage exhaustif : sur les 512 cadres à 3 mondes,\n", + " `T` est falsifiable *exactement* sur les cadres non réflexifs, `4` sur les non transitifs, `5` sur les non euclidiens —\n", + " et `K` sur aucun\n", + "4. **Certifier** chaque constat : `K` valide sur *tout* cadre devient un théorème Lean ; les falsifications\n", + " de `T`/`4`/`5` deviennent des contre-modèles exhibés et vérifiés par le noyau ; sur les cadres S4\n", + " (`Fin74`), réflexivité et transitivité *donnent* les duaux diamant\n", + "5. **Mesurer la provenance** du corpus (pins `git rev-parse` confrontés au manifest) avant toute certification\n", + "\n", + "## Prérequis\n", + "\n", + "- [Tweety-01-Setup-Python](Tweety-01-Setup-Python.ipynb) exécuté (JVM, JARs, JPype) — le dossier `libs/` du répertoire `Tweety`\n", + "- Notions modales : le volet 2.4 de [Tweety-3](Tweety-3-Advanced-Logics.ipynb) (syntaxe `[]`/`<>`, bug SPASS)\n", + "- Pour les sections 5-6 : hôte Windows + WSL avec le lake `Lean/formal_logic_lean` construit — les cellules\n", + " **disent** comment le réparer, jamais comment le contourner (règle F)\n", + "\n", + "### Durée estimée : 45 minutes\n", + "\n", + "> **Position dans la série** : compagnon modal des labos [Tweety-5e](Tweety-5e-Propositional-Lab-Lean.ipynb)\n", + "> (propositionnel) et [Tweety-02d](Tweety-02d-FOL-Lab-Lean.ipynb) (FOL) — même patron\n", + "> (moteur exécuté ↔ noyau certifiant). Ce labo consomme le pont `FormalLogic.ModalBridge`\n", + "> (Tranche C de l'EPIC, livré par [#17017](https://github.com/jsboige/CoursIA/pull/17017)) :\n", + "> les cadres témoins certifiés côté Lean sont **les mêmes** que ceux énumérés côté Python.\n" + ] + }, + { + "cell_type": "markdown", + "id": "c1-question", + "metadata": { + "papermill": { + "duration": 0.004836, + "end_time": "2026-09-21T01:40:38.766019+00:00", + "exception": false, + "start_time": "2026-09-21T01:40:38.761183+00:00", + "status": "completed" + }, + "tags": [] + }, + "source": [ + "## 1. La question du labo\n", + "\n", + "La formule `[]p -> p` (l'axiome **T** : « ce qui est nécessaire est vrai ») est-elle *valide* —\n", + "vraie dans tous les mondes de tous les modèles ?\n", + "\n", + "En logique propositionnelle ou FOL, la question aurait une réponse binaire. En modal, elle n'en a pas :\n", + "**tout dépend du cadre**. La sémantique de Kripke évalue une formule relativement à un *monde* `x`\n", + "dans un *modèle* `(W, R, V)` — un ensemble de mondes, une relation d'accessibilité `R`, une valuation `V` :\n", + "\n", + "- `x satisfait []f` si **tout** monde accessible depuis `x` satisfait `f` ;\n", + "- `x satisfait <>f` si **quelque** monde accessible depuis `x` satisfait `f`.\n", + "\n", + "Alors `[]p -> p` échoue dès qu'un monde `x` n'a pas accès à lui-même : `[]p` peut y être vrai\n", + "(tous les successeurs voient `p`) pendant que `p` y est faux. La logique modale n'est pas *une* logique :\n", + "c'est un spectre — **K**, **T**, **K4**, **S4**, **S5** — obtenu en imposant des conditions\n", + "sur le cadre (réflexivité, transitivité, euclidianité). C'est la **théorie de la correspondance**,\n", + "et ce labo la fait *émerger d'un comptage* puis la *fait certifier par un noyau*.\n", + "\n", + "Le plan, dans l'esprit de la série :\n", + "\n", + "| Section | Moteur | Ce qu'il donne |\n", + "|---|---|---|\n", + "| 2 | Tweety (Java) | la **syntaxe** : parser `[]`/`<>`, rendre l'arbre — et la limite SPASS |\n", + "| 3-4 | moteur Kripke (Python) | la **sémantique** : témoins ciblés, puis balayage exhaustif 512 cadres |\n", + "| 5 | `formal_logic_lean` (Lean) | les **certificats** : théorème pour tout cadre, contre-modèles kernel-vérifiés |\n", + "| 6 | — | le bilan croisé des trois lectures |\n" + ] + }, + { + "cell_type": "code", + "execution_count": 1, + "id": "c2-jvm", + "metadata": { + "execution": { + "iopub.execute_input": "2026-09-21T01:40:38.778879Z", + "iopub.status.busy": "2026-09-21T01:40:38.778322Z", + "iopub.status.idle": "2026-09-21T01:40:40.400319Z", + "shell.execute_reply": "2026-09-21T01:40:40.398268Z" + }, + "papermill": { + "duration": 1.63097, + "end_time": "2026-09-21T01:40:40.401897+00:00", + "exception": false, + "start_time": "2026-09-21T01:40:38.770927+00:00", + "status": "completed" + }, + "tags": [] + }, + "outputs": [ + { + "name": "stdout", + "output_type": "stream", + "text": [ + "--- Initialisation Tweety ---\n", + "Bibliotheques natives: native/\n" + ] + }, + { + "name": "stdout", + "output_type": "stream", + "text": [ + "JVM demarree avec 42 JARs.\n" + ] + }, + { + "name": "stdout", + "output_type": "stream", + "text": [ + "Module modal Tweety charge : org.tweetyproject.logics.ml.parser.MlParser\n" + ] + } + ], + "source": [ + "# --- Initialisation JVM Tweety (helper partage de la serie) + imports modaux ---\n", + "import os\n", + "import pathlib\n", + "import sys\n", + "\n", + "TWEETY_DIR = pathlib.Path.cwd()\n", + "if TWEETY_DIR.name != \"Tweety\":\n", + " # execution hors du dossier Tweety : retour au chemin canonique\n", + " candidat = pathlib.Path(\"MyIA.AI.Notebooks\") / \"SymbolicAI\" / \"Tweety\"\n", + " if candidat.is_dir():\n", + " os.chdir(candidat)\n", + " TWEETY_DIR = pathlib.Path.cwd()\n", + "sys.path.insert(0, str(TWEETY_DIR))\n", + "\n", + "from tweety_init import init_tweety\n", + "\n", + "jvm_ready = init_tweety(verbose=True)\n", + "if not jvm_ready:\n", + " # Contrat d'execution : echec visible, aucun contournement (regle F)\n", + " raise RuntimeError(\n", + " \"init_tweety a echoue (JAVA_HOME, dossier libs/ ou demarrage JVM) : \"\n", + " \"reparer l'environnement (cf. Tweety-01-Setup-Python) avant de relancer.\"\n", + " )\n", + "\n", + "import jpype\n", + "from jpype.types import JObject\n", + "\n", + "from org.tweetyproject.logics.commons.syntax import Predicate\n", + "from org.tweetyproject.logics.fol.syntax import FolSignature, FolFormula\n", + "from org.tweetyproject.logics.ml.syntax import MlBeliefSet\n", + "from org.tweetyproject.logics.ml.parser import MlParser\n", + "\n", + "_parser_probe = MlParser()\n", + "print(\"Module modal Tweety charge :\", _parser_probe.getClass().getName())\n" + ] + }, + { + "cell_type": "markdown", + "id": "c3-lecture-jvm", + "metadata": { + "papermill": { + "duration": 0.007247, + "end_time": "2026-09-21T01:40:40.416521+00:00", + "exception": false, + "start_time": "2026-09-21T01:40:40.409274+00:00", + "status": "completed" + }, + "tags": [] + }, + "source": [ + "### Lecture : l'environnement est réel, pas simulé\n", + "\n", + "La sortie atteste trois choses : le JDK est résolu (portable ou `JAVA_HOME`), la JVM démarre sur\n", + "**tous** les JARs du dossier `libs/`, et le module `org.tweetyproject.logics.ml` — le calcul modal\n", + "de Tweety — est chargé dans la JVM.\n", + "\n", + "Un point de méthode avant d'aller plus loin : le notebook 3 (section 2.4) documente pourquoi le\n", + "raisonneur modal de Tweety ne rend aucun verdict — `SPASSMlReasoner` produit une syntaxe DFG\n", + "invalide (bug upstream [Issue #1334](https://github.com/TweetyProject/Tweety/issues/1334)).\n", + "Ce labo ne contourne pas le bug par une sortie fabriquée : il change d'*étage*. La vérité modale\n", + "ne vient pas d'un prover externe mais de la **sémantique elle-même** — d'abord énumérée en Python,\n", + "puis certifiée par le noyau Lean. Le parser Tweety garde son rôle exact : donner la syntaxe." + ] + }, + { + "cell_type": "markdown", + "id": "c4-syntaxe", + "metadata": { + "papermill": { + "duration": 0.006356, + "end_time": "2026-09-21T01:40:40.430008+00:00", + "exception": false, + "start_time": "2026-09-21T01:40:40.423652+00:00", + "status": "completed" + }, + "tags": [] + }, + "source": [ + "## 2. La syntaxe : Tweety manipule les quatre schémas\n", + "\n", + "Les quatre schémas d'axiomes qui structurent le spectre modal, dans la syntaxe de Tweety\n", + "(`[]` = nécessité, `<>` = possibilité, `=>` = implication) :\n", + "\n", + "| Schéma | Lecture | Syntaxe Tweety | Ce qu'il exigera du cadre |\n", + "|---|---|---|---|\n", + "| **K** | distribution : le nécessaire distribute sur l'implication | `[](p => q) => ([]((p)) => []((q)))` | *rien* — validité gratuite |\n", + "| **T** | ce qui est nécessaire est vrai | `[]((p)) => (p)` | réflexivité |\n", + "| **4** | le nécessaire est nécessairement nécessaire | `[]((p)) => []([]((p)))` | transitivité |\n", + "| **5** | le possible est nécessairement possible | `<>((p)) => [](<>((p)))` | euclidianité |\n", + "\n", + "> **Convention syntaxique Tweety** : une formule *nue* sous modalité se parenthèse — `[]p`\n", + "> s'écrit `[]((p))`. Le parser rejette `[]p` à l'intérieur d'une formule composée\n", + "> (« *missing parentheses around modalized formula* ») ; les composées comme `[](q && r)`\n", + "> passent telles quelles." + ] + }, + { + "cell_type": "code", + "execution_count": 2, + "id": "c5-parsing", + "metadata": { + "execution": { + "iopub.execute_input": "2026-09-21T01:40:40.446294Z", + "iopub.status.busy": "2026-09-21T01:40:40.445727Z", + "iopub.status.idle": "2026-09-21T01:40:40.618832Z", + "shell.execute_reply": "2026-09-21T01:40:40.617346Z" + }, + "papermill": { + "duration": 0.183197, + "end_time": "2026-09-21T01:40:40.620119+00:00", + "exception": false, + "start_time": "2026-09-21T01:40:40.436922+00:00", + "status": "completed" + }, + "tags": [] + }, + "outputs": [ + { + "name": "stdout", + "output_type": "stream", + "text": [ + "Parsing des quatre schemas d'axiomes :\n", + " [OK] K : normalite (distribution)\n", + " source : [](p => q) => ([]((p)) => []((q)))\n", + " rendu Tweety: ([]((p=>q))=>([](p)=>[](q)))\n" + ] + }, + { + "name": "stdout", + "output_type": "stream", + "text": [ + " [OK] T : reflexivite ([]p => p)\n", + " source : []((p)) => (p)\n", + " rendu Tweety: ([](p)=>p)\n", + " [OK] 4 : transitivite ([]p => [][]p)\n", + " source : []((p)) => []([]((p)))\n", + " rendu Tweety: ([](p)=>[]([](p)))\n", + " [OK] 5 : euclideanite (<>p => []<>p)\n", + " source : <>((p)) => [](<>((p)))\n", + " rendu Tweety: (<>(p)=>[](<>(p)))\n", + "\n", + "KB modale : 4 formules syntaxiques chargees.\n" + ] + } + ], + "source": [ + "# --- Les quatre schemas d'axiomes parses par Tweety (contrat : 4/4) ---\n", + "sig_ml = FolSignature()\n", + "for nom in (\"p\", \"q\"):\n", + " sig_ml.add(Predicate(nom, 0))\n", + "\n", + "parser_ml = MlParser()\n", + "parser_ml.setSignature(sig_ml)\n", + "\n", + "schemas_tweety = [\n", + " (\"K : normalite (distribution)\", \"[](p => q) => ([]((p)) => []((q)))\"),\n", + " (\"T : reflexivite ([]p => p)\", \"[]((p)) => (p)\"),\n", + " (\"4 : transitivite ([]p => [][]p)\", \"[]((p)) => []([]((p)))\"),\n", + " (\"5 : euclideanite (<>p => []<>p)\", \"<>((p)) => [](<>((p)))\"),\n", + "]\n", + "\n", + "kb_ml = MlBeliefSet()\n", + "print(\"Parsing des quatre schemas d'axiomes :\")\n", + "for etiquette, source in schemas_tweety:\n", + " try:\n", + " f = parser_ml.parseFormula(source)\n", + " except Exception as e:\n", + " # le labo porte sur CES quatre formules : un echec de parsing est bloquant\n", + " raise RuntimeError(f\"parseFormula a echoue pour {source!r} : {e}\")\n", + " kb_ml.add(JObject(f, FolFormula))\n", + " print(f\" [OK] {etiquette}\")\n", + " print(f\" source : {source}\")\n", + " print(f\" rendu Tweety: {f}\")\n", + "print(f\"\\nKB modale : {kb_ml.size()} formules syntaxiques chargees.\")\n" + ] + }, + { + "cell_type": "markdown", + "id": "c6-lecture-parsing", + "metadata": { + "papermill": { + "duration": 0.007675, + "end_time": "2026-09-21T01:40:40.636714+00:00", + "exception": false, + "start_time": "2026-09-21T01:40:40.629039+00:00", + "status": "completed" + }, + "tags": [] + }, + "source": [ + "### Lecture : la structure est là, le verdict n'y est pas\n", + "\n", + "Le rendu de Tweety — `([](p=>q)=>([](p)=>[](q)))`, `(<>(p)=>[](<>(p)))`… — montre l'arbre\n", + "syntaxique complet : les nœuds `[]`/`<>` sont des objets Java de première classe, inspectables,\n", + "composables. C'est tout ce que le module `ml` de Tweety promet *aujourd'hui* : la **manipulation**.\n", + "\n", + "Ce qui manque — et que le bug SPASS #1334 rend indisponible côté Tweety — est le **verdict** :\n", + "cette formule est-elle valide ? Pour l'obtenir sans prover externe, on descend d'un étage\n", + "abstrait : la sémantique. C'est l'objet de la section suivante, et le cœur du labo." + ] + }, + { + "cell_type": "markdown", + "id": "c7-semantique", + "metadata": { + "papermill": { + "duration": 0.007729, + "end_time": "2026-09-21T01:40:40.652250+00:00", + "exception": false, + "start_time": "2026-09-21T01:40:40.644521+00:00", + "status": "completed" + }, + "tags": [] + }, + "source": [ + "## 3. La sémantique : un moteur de Kripke en trente lignes de Python\n", + "\n", + "Un **cadre** est un couple `(W, R)` — des mondes, une relation d'accessibilité. Un **modèle**\n", + "ajoute une valuation `V` : les atomes vrais à chaque monde. Le **forcing** `x satisfait f` se définit\n", + "récursivement ; les deux clauses qui font toute la modalité :\n", + "\n", + "```\n", + "x satisfait []f ssi pour tout y tel que x R y : y satisfait f\n", + "x satisfait <>f ssi il existe y tel que x R y : y satisfait f\n", + "```\n", + "\n", + "Deux choix d'implémentation méritent une ligne : les formules sont des `dataclass` **gelées**\n", + "(immuables, hachables — un schéma peut servir de clé de dictionnaire) ; la relation est un\n", + "`frozenset` de couples, jamais une matrice — pour énumérer *tous* les cadres de la section 4,\n", + "un cadre n'est rien d'autre qu'un sous-ensemble d'arcs, et il se débite en bits." + ] + }, + { + "cell_type": "code", + "execution_count": 3, + "id": "c8-moteur", + "metadata": { + "execution": { + "iopub.execute_input": "2026-09-21T01:40:40.669336Z", + "iopub.status.busy": "2026-09-21T01:40:40.668670Z", + "iopub.status.idle": "2026-09-21T01:40:40.692872Z", + "shell.execute_reply": "2026-09-21T01:40:40.690988Z" + }, + "papermill": { + "duration": 0.034251, + "end_time": "2026-09-21T01:40:40.694142+00:00", + "exception": false, + "start_time": "2026-09-21T01:40:40.659891+00:00", + "status": "completed" + }, + "tags": [] + }, + "outputs": [ + { + "name": "stdout", + "output_type": "stream", + "text": [ + " p en 0 : faux\n", + " []p en 0 : vrai\n", + " T en 0 : faux\n", + " <>p en 1 : faux\n", + "\n", + "Moteur operationnel : monde mort (1 sans successeur), [] y est vacuement vrai.\n" + ] + } + ], + "source": [ + "# --- Moteur de Kripke : AST gelee + forcing recursif ---\n", + "from dataclasses import dataclass\n", + "\n", + "@dataclass(frozen=True)\n", + "class Atome: nom: str\n", + "@dataclass(frozen=True)\n", + "class Non: f: object\n", + "@dataclass(frozen=True)\n", + "class Imp: a: object; b: object\n", + "@dataclass(frozen=True)\n", + "class Et: a: object; b: object\n", + "@dataclass(frozen=True)\n", + "class Boite: f: object\n", + "@dataclass(frozen=True)\n", + "class Diamant: f: object\n", + "\n", + "@dataclass(frozen=True)\n", + "class Modele:\n", + " mondes: tuple # de mondes (entiers)\n", + " relation: frozenset # de couples (x, y) : x R y\n", + " valuation: dict # Atome.nom -> frozenset des mondes ou l'atome est vrai\n", + "\n", + " def successeurs(self, x):\n", + " return frozenset(y for (a, y) in self.relation if a == x)\n", + "\n", + "def satisfait(M, x, f):\n", + " \"\"\"Forcing x |= f -- la clause Boite est 'pour tout successeur', Diamant 'il existe'.\"\"\"\n", + " if isinstance(f, Atome): return x in M.valuation[f.nom]\n", + " if isinstance(f, Non): return not satisfait(M, x, f.f)\n", + " if isinstance(f, Imp): return (not satisfait(M, x, f.a)) or satisfait(M, x, f.b)\n", + " if isinstance(f, Et): return satisfait(M, x, f.a) and satisfait(M, x, f.b)\n", + " if isinstance(f, Boite): return all(satisfait(M, y, f.f) for y in M.successeurs(x))\n", + " if isinstance(f, Diamant): return any(satisfait(M, y, f.f) for y in M.successeurs(x))\n", + " raise TypeError(f\"formule inconnue : {f!r}\")\n", + "\n", + "def show(f):\n", + " if isinstance(f, Atome): return f.nom\n", + " if isinstance(f, Non): return \"non \" + show(f.f)\n", + " if isinstance(f, Imp): return f\"({show(f.a)} -> {show(f.b)})\"\n", + " if isinstance(f, Et): return f\"({show(f.a)} et {show(f.b)})\"\n", + " if isinstance(f, Boite): return \"[]\" + show(f.f)\n", + " if isinstance(f, Diamant): return \"<>\" + show(f.f)\n", + "\n", + "# Mini-test : le monde 0 voit le monde 1, p est vrai en 1 seulement.\n", + "m_test = Modele((0, 1), frozenset({(0, 1)}), {\"p\": frozenset({1})})\n", + "verdicts = {\n", + " \"p en 0\": satisfait(m_test, 0, Atome(\"p\")),\n", + " \"[]p en 0\": satisfait(m_test, 0, Boite(Atome(\"p\"))),\n", + " \"T en 0\": satisfait(m_test, 0, Imp(Boite(Atome(\"p\")), Atome(\"p\"))),\n", + " \"<>p en 1\": satisfait(m_test, 1, Diamant(Atome(\"p\"))),\n", + "}\n", + "for etiquette, valeur in verdicts.items():\n", + " print(f\" {etiquette:12s} : {'vrai' if valeur else 'faux'}\")\n", + "assert verdicts[\"[]p en 0\"] and not verdicts[\"T en 0\"]\n", + "print(\"\\nMoteur operationnel : monde mort (1 sans successeur), [] y est vacuement vrai.\")\n" + ] + }, + { + "cell_type": "markdown", + "id": "c9-lecture-moteur", + "metadata": { + "papermill": { + "duration": 0.006833, + "end_time": "2026-09-21T01:40:40.709082+00:00", + "exception": false, + "start_time": "2026-09-21T01:40:40.702249+00:00", + "status": "completed" + }, + "tags": [] + }, + "source": [ + "### Lecture : le monde mort et la vacuité\n", + "\n", + "Le mini-test porte en germe tout le labo. Le monde `1` n'a **aucun** successeur : `<>p` y est\n", + "faux (aucun témoin accessible) mais `[]p` y est **vacuément vrai** — le `all(...)` sur un ensemble\n", + "vide n'échoue jamais. C'est exact sur le plan mathématique (la clause `[]` quantifie universellement\n", + "sur les successeurs : sans successeur, rien ne peut la contredire), et c'est un piège classique :\n", + "un cadre rempli de mondes morts rend `[]f` vrai partout sans rien dire de `f`.\n", + "\n", + "La clause `[]` du moteur — `all(satisfait(M, y, f.f) for y in M.successeurs(x))` — est aussi\n", + "la **ligne de jonction** avec le versant certifiant : la preuve `forces_kdist` du pont Lean\n", + "démontre la distribution **en introduisant un successeur arbitraire** puis en appliquant les deux\n", + "hypothèses — littéralement le même « pour tout successeur », version type-théorie." + ] + }, + { + "cell_type": "markdown", + "id": "c10-temoins", + "metadata": { + "papermill": { + "duration": 0.006765, + "end_time": "2026-09-21T01:40:40.723276+00:00", + "exception": false, + "start_time": "2026-09-21T01:40:40.716511+00:00", + "status": "completed" + }, + "tags": [] + }, + "source": [ + "## 4. Le duel des témoins : trois cadres qui cassent T, 4, 5\n", + "\n", + "La théorie de la correspondance prédit quel cadre falsifie quel schéma. Voici les trois\n", + "témoins — minimaux, sur `{0, 1}` ou `{0, 1, 2}`, les autres mondes étant isolés. Ce sont **les\n", + "mêmes cadres** que ceux définis et certifiés côté Lean par `FormalLogic.ModalBridge` :\n", + "`frameT`, `frame4`, `frame5` :\n", + "\n", + "| Témoin | Arcs | Condition violée | Schéma falsifié | Pourquoi ça marche |\n", + "|---|---|---|---|---|\n", + "| `frameT` | `0 -> 1` | réflexivité (0 ne se voit pas) | **T** | `[]p` vrai en 0 (le successeur 1 voit `p`), `p` faux en 0 |\n", + "| `frame4` | `0 -> 1 -> 2` (pas `0 -> 2`) | transitivité | **4** | `[]p` vrai en 0, mais le successeur 1 voit le monde 2 sans `p` : `¬[]p` en 1 donc `¬[][]p` en 0 |\n", + "| `frame5` | `0 -> 1`, `0 -> 2` | euclidianité (1 ne voit pas 2) | **5** | `<>p` vrai en 0 via 1, mais 2 est mort : `¬<>p` en 2, donc `¬[]<>p` en 0 |\n", + "\n", + "Et `K` ? La prédiction est qu'il survit partout — la distribution ne dit rien du cadre, elle\n", + "est vraie *parce que* la clause `[]` quantifie uniformément sur les successeurs." + ] + }, + { + "cell_type": "code", + "execution_count": 4, + "id": "c11-duel", + "metadata": { + "execution": { + "iopub.execute_input": "2026-09-21T01:40:40.741860Z", + "iopub.status.busy": "2026-09-21T01:40:40.741275Z", + "iopub.status.idle": "2026-09-21T01:40:40.754518Z", + "shell.execute_reply": "2026-09-21T01:40:40.752834Z" + }, + "papermill": { + "duration": 0.024334, + "end_time": "2026-09-21T01:40:40.755646+00:00", + "exception": false, + "start_time": "2026-09-21T01:40:40.731312+00:00", + "status": "completed" + }, + "tags": [] + }, + "outputs": [ + { + "name": "stdout", + "output_type": "stream", + "text": [ + "Verdicts au monde 0 (vrai/FAUX) :\n", + "\n", + "Schema frameT {0->1} frame4 {0->1->2} frame5 {0->1, 0->2}\n", + "K vrai vrai vrai\n", + "T FAUX FAUX vrai\n", + "4 vrai FAUX vrai\n", + "5 FAUX FAUX FAUX\n", + "\n", + "Asserts passes : la diagonale est FAUX, K survit sur les trois temoins.\n" + ] + } + ], + "source": [ + "# --- Les trois temoins : verdicts au monde 0, asserts sur la diagonale ---\n", + "p, q = Atome(\"p\"), Atome(\"q\")\n", + "\n", + "schemas = [\n", + " (\"K\", Imp(Boite(Imp(p, q)), Imp(Boite(p), Boite(q)))),\n", + " (\"T\", Imp(Boite(p), p)),\n", + " (\"4\", Imp(Boite(p), Boite(Boite(p)))),\n", + " (\"5\", Imp(Diamant(p), Boite(Diamant(p)))),\n", + "]\n", + "\n", + "temoins = [\n", + " (\"frameT {0->1}\", Modele((0, 1), frozenset({(0, 1)}), {\"p\": frozenset({1}), \"q\": frozenset()})),\n", + " (\"frame4 {0->1->2}\", Modele((0, 1, 2), frozenset({(0, 1), (1, 2)}), {\"p\": frozenset({1}), \"q\": frozenset()})),\n", + " (\"frame5 {0->1, 0->2}\", Modele((0, 1, 2), frozenset({(0, 1), (0, 2)}), {\"p\": frozenset({1}), \"q\": frozenset()})),\n", + "]\n", + "# q est faux partout dans les temoins : K est vrai pour TOUTE valuation de q\n", + "# (sa validite ne depend que de la clause pour-tout), la valuation minimale suffit.\n", + "\n", + "print(f\"Verdicts au monde 0 (vrai/FAUX) :\\n\")\n", + "print(f\"{'Schema':8s}\" + \"\".join(f\"{nom:>22s}\" for nom, _ in temoins))\n", + "for nom_s, sch in schemas:\n", + " ligne = f\"{nom_s:8s}\"\n", + " for _, M in temoins:\n", + " valeur = satisfait(M, 0, sch)\n", + " ligne += f\"{('vrai' if valeur else 'FAUX'):>22s}\"\n", + " print(ligne)\n", + "\n", + "# La diagonale : chaque temoin casse SON schema (parmi T/4/5).\n", + "assert not satisfait(temoins[0][1], 0, schemas[1][1]), \"T doit etre falsifie sur frameT\"\n", + "assert not satisfait(temoins[1][1], 0, schemas[2][1]), \"4 doit etre falsifie sur frame4\"\n", + "assert not satisfait(temoins[2][1], 0, schemas[3][1]), \"5 doit etre falsifie sur frame5\"\n", + "# K, lui, ne doit etre falsifie nulle part -- ni sur les temoins...\n", + "for _, M in temoins:\n", + " for x in M.mondes:\n", + " assert satisfait(M, x, schemas[0][1]), \"K ne doit jamais etre falsifie\"\n", + "print(\"\\nAsserts passes : la diagonale est FAUX, K survit sur les trois temoins.\")\n" + ] + }, + { + "cell_type": "markdown", + "id": "c12-lecture-duel", + "metadata": { + "papermill": { + "duration": 0.005487, + "end_time": "2026-09-21T01:40:40.766617+00:00", + "exception": false, + "start_time": "2026-09-21T01:40:40.761130+00:00", + "status": "completed" + }, + "tags": [] + }, + "source": [ + "### Lecture : la diagonale exacte, et le survivant\n", + "\n", + "La table rend la structure prédictive visible : chaque colonne-témoin porte **exactement un** FAUX\n", + "— le schéma dont elle viole la condition de cadre. Aucun dégât collatéral : l'éventail de `frame5`\n", + "est non euclidien *et* non transitif, et pourtant il laisse `4` intact au monde 0 — chaque crime\n", + "porte son nom, aucun témoin n'est un assassi à la chaîne.\n", + "\n", + "Un cadre peut violer plusieurs conditions à la fois — `frameT` (0 ne se voit pas) est aussi\n", + "non transitif tant que `0 -> 1 -> 0` manque, et la table le montre : `T` casse, `4` tient.\n", + "C'est la force du protocole : on falsifie **un** schéma à la fois, avec le cadre **minimal** qui\n", + "ne viole que sa condition.\n", + "\n", + "Et `K` vit partout — sur ces trois cadres. Trois cadres ne sont pas une preuve : c'est un\n", + "**sondage directionnel**. La section suivante remplace le choix guidé par l'épuisement." + ] + }, + { + "cell_type": "code", + "execution_count": 5, + "id": "c13-balayage", + "metadata": { + "execution": { + "iopub.execute_input": "2026-09-21T01:40:40.782577Z", + "iopub.status.busy": "2026-09-21T01:40:40.782022Z", + "iopub.status.idle": "2026-09-21T01:40:41.753397Z", + "shell.execute_reply": "2026-09-21T01:40:41.751830Z" + }, + "papermill": { + "duration": 0.981701, + "end_time": "2026-09-21T01:40:41.755079+00:00", + "exception": false, + "start_time": "2026-09-21T01:40:40.773378+00:00", + "status": "completed" + }, + "tags": [] + }, + "outputs": [ + { + "name": "stdout", + "output_type": "stream", + "text": [ + "Balayage exhaustif : 512 cadres a 3 mondes (2^9 sous-ensembles d'arcs), toutes valuations.\n", + "\n" + ] + }, + { + "name": "stdout", + "output_type": "stream", + "text": [ + " non reflexifs : 448 cadres\n", + " non transitifs : 341 cadres\n", + " non euclidiens : 473 cadres\n", + "\n", + " K falsifiable sur 0 cadres [EGALITE EXACTE avec aucun cadre]\n", + " T falsifiable sur 448 cadres [EGALITE EXACTE avec les non reflexifs]\n", + " 4 falsifiable sur 341 cadres [EGALITE EXACTE avec les non transitifs]\n", + " 5 falsifiable sur 473 cadres [EGALITE EXACTE avec les non euclidiens]\n", + "\n", + "Correspondance verifiee par enumeration : T <-> reflexif, 4 <-> transitif, 5 <-> euclidien, K <-> rien (jamais falsifiable).\n" + ] + } + ], + "source": [ + "# --- Balayage exhaustif : TOUS les cadres a 3 mondes, TOUTES les valuations ---\n", + "def tous_cadres(n):\n", + " arcs = [(x, y) for x in range(n) for y in range(n)]\n", + " for masque in range(2 ** (n * n)):\n", + " yield frozenset(a for i, a in enumerate(arcs) if masque >> i & 1)\n", + "\n", + "def est_reflexive(R, n): return all((x, x) in R for x in range(n))\n", + "def est_transitive(R, n): return all((x, z) in R for x in range(n) for y in range(n)\n", + " for z in range(n) if (x, y) in R and (y, z) in R)\n", + "def est_euclidienne(R, n): return all((y, z) in R for x in range(n) for y in range(n)\n", + " for z in range(n) if (x, y) in R and (x, z) in R)\n", + "\n", + "def falsifiable(sch, R, n, atomes):\n", + " \"\"\"Existe-t-il une valuation et un monde falsifiant le schema sur CE cadre ?\"\"\"\n", + " monde_taille = 2 ** n\n", + " for vmask_p in range(monde_taille if \"p\" in atomes else 1):\n", + " for vmask_q in range(monde_taille if \"q\" in atomes else 1):\n", + " V = {}\n", + " if \"p\" in atomes: V[\"p\"] = frozenset(w for w in range(n) if vmask_p >> w & 1)\n", + " if \"q\" in atomes: V[\"q\"] = frozenset(w for w in range(n) if vmask_q >> w & 1)\n", + " M = Modele(tuple(range(n)), R, V)\n", + " if any(not satisfait(M, x, sch) for x in range(n)):\n", + " return True\n", + " return False\n", + "\n", + "N = 3\n", + "cadres3 = list(tous_cadres(N))\n", + "print(f\"Balayage exhaustif : {len(cadres3)} cadres a {N} mondes \"\n", + " f\"(2^{N * N} sous-ensembles d'arcs), toutes valuations.\\n\")\n", + "\n", + "falsif = {nom: {R for R in cadres3 if falsifiable(sch, R, N, (\"p\", \"q\") if nom == \"K\" else (\"p\",))}\n", + " for nom, sch in schemas}\n", + "\n", + "familles = {\n", + " \"non reflexifs\": {R for R in cadres3 if not est_reflexive(R, N)},\n", + " \"non transitifs\": {R for R in cadres3 if not est_transitive(R, N)},\n", + " \"non euclidiens\": {R for R in cadres3 if not est_euclidienne(R, N)},\n", + "}\n", + "for nom, ensemble in familles.items():\n", + " print(f\" {nom:16s}: {len(ensemble):3d} cadres\")\n", + "print()\n", + "predications = [\n", + " (\"K\", falsif[\"K\"], set(), \"aucun cadre\"),\n", + " (\"T\", falsif[\"T\"], familles[\"non reflexifs\"], \"les non reflexifs\"),\n", + " (\"4\", falsif[\"4\"], familles[\"non transitifs\"], \"les non transitifs\"),\n", + " (\"5\", falsif[\"5\"], familles[\"non euclidiens\"], \"les non euclidiens\"),\n", + "]\n", + "for nom, ens, attendu, etiquette in predications:\n", + " verdict = \"EGALITE EXACTE\" if ens == attendu else \"DIVERGENCE\"\n", + " print(f\" {nom} falsifiable sur {len(ens):3d} cadres [{verdict} avec {etiquette}]\")\n", + " assert ens == attendu, f\"la correspondance de {nom} echoue sur les cadres 3-mondes\"\n", + "\n", + "print(\"\\nCorrespondance verifiee par enumeration : T <-> reflexif, 4 <-> transitif, \"\n", + " \"5 <-> euclidien, K <-> rien (jamais falsifiable).\")\n" + ] + }, + { + "cell_type": "markdown", + "id": "c14-lecture-balayage", + "metadata": { + "papermill": { + "duration": 0.007692, + "end_time": "2026-09-21T01:40:41.770958+00:00", + "exception": false, + "start_time": "2026-09-21T01:40:41.763266+00:00", + "status": "completed" + }, + "tags": [] + }, + "source": [ + "### Lecture : la correspondance émerge du comptage — et s'arrête au bord du comptage\n", + "\n", + "Sur les 512 cadres à 3 mondes, chaque **égalité exacte** est une donnée mesurée, pas un slogan :\n", + "`T` falsifiable sur exactement les cadres non réflexifs, `4` sur les non transitifs, `5` sur les\n", + "non euclidiens, et `K` sur **aucun des 512** — la normalité est gratuite, elle ne négocie jamais\n", + "avec la forme du cadre.\n", + "\n", + "Mais l'énumération a un bord, et il faut le nommer : elle ne dit **rien** des cadres à 4 mondes\n", + "et plus, rien des cadres infinis, rien des cadres non dénombrables. L'égalité constatée ici est\n", + "une **correspondance à cette taille** — le pas vers « pour tout cadre » est un pas infini, et il\n", + "exige une preuve, pas un sondage de plus. C'est précisément ce que la section suivante achète :\n", + "un théorème Lean vaut pour *tous* les cadres de l'Archive — les 512, les cadres à un million de\n", + "mondes, les infinis — d'une seule dérivation vérifiée par le noyau." + ] + }, + { + "cell_type": "markdown", + "id": "c15-versant-lean", + "metadata": { + "papermill": { + "duration": 0.008247, + "end_time": "2026-09-21T01:40:41.786865+00:00", + "exception": false, + "start_time": "2026-09-21T01:40:41.778618+00:00", + "status": "completed" + }, + "tags": [] + }, + "source": [ + "## 5. Le versant certifiant : le lake `formal_logic_lean`\n", + "\n", + "Le corps de certification vit dans le lake sibling de la série :\n", + "[`Lean/formal_logic_lean`](../Lean/formal_logic_lean/FormalLogic/ModalBridge.lean), qui consomme\n", + "au pin exact **deux** corpus modaux :\n", + "\n", + "- **`ModalLogicArchive.Modal.Kripke`** — cadres **génériques**, sans aucune contrainte :\n", + " le bon substrat pour falsifier `T`, `4`, `5` et prouver `K` ;\n", + "- **`Fin74.Kripke`** — cadres **réflexifs et transitifs par construction** (`rel_refl` et\n", + " `rel_trans` sont des champs de données) : S4 par hypothèse du type, pas par axiome.\n", + "\n", + "Le pont `FormalLogic.ModalBridge` (Tranche C de l'EPIC [#15066](https://github.com/jsboige/CoursIA/issues/15066),\n", + "livré par [#17017](https://github.com/jsboige/CoursIA/pull/17017)) y définit les cadres témoins\n", + "— `frameT`, `frame4`, `frame5`, **les mêmes arcs que la section 4** — et les certifie. Le protocole\n", + "avant toute certification, hérité du labo FOL :\n", + "\n", + "1. **provenance mesurée** : `git rev-parse` dans `.lake/packages` confronté au `lake-manifest.json` —\n", + " on certifie *ces* sources, pas un souvenir ;\n", + "2. **build réel** : `lake build FormalLogic.ModalBridge` doit être vert, idempotent, sans `sorry` ;\n", + "3. alors seulement : `#check` / `#print axioms` dans un scratch vérifié par le noyau." + ] + }, + { + "cell_type": "code", + "execution_count": 6, + "id": "c16-helpers", + "metadata": { + "execution": { + "iopub.execute_input": "2026-09-21T01:40:41.807259Z", + "iopub.status.busy": "2026-09-21T01:40:41.806733Z", + "iopub.status.idle": "2026-09-21T01:41:34.237774Z", + "shell.execute_reply": "2026-09-21T01:41:34.235749Z" + }, + "papermill": { + "duration": 52.446559, + "end_time": "2026-09-21T01:41:34.243177+00:00", + "exception": false, + "start_time": "2026-09-21T01:40:41.796618+00:00", + "status": "completed" + }, + "tags": [] + }, + "outputs": [ + { + "name": "stdout", + "output_type": "stream", + "text": [ + "Provenance mesuree (git rev-parse dans .lake/packages) :\n" + ] + }, + { + "name": "stdout", + "output_type": "stream", + "text": [ + " mathlib 0df444a360ea [pin confirme]\n" + ] + }, + { + "name": "stdout", + "output_type": "stream", + "text": [ + " ModalLogic 71968137b917 [pin confirme]\n" + ] + }, + { + "name": "stdout", + "output_type": "stream", + "text": [ + " Foundation 81810b9f22c4 [pin confirme]\n" + ] + }, + { + "name": "stdout", + "output_type": "stream", + "text": [ + "\n", + "$ lake build FormalLogic.ModalBridge\n", + "Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`\n", + "Build completed successfully (1021 jobs).\n", + "warning: ModalLogic: repository '/Lean/formal_logic_lean/.lake/packages/ModalLogic' has local changes\n", + "\n", + "BUILD OK : le module du pont compile sans aucun sorry.\n" + ] + } + ], + "source": [ + "# --- Helpers WSL + nettoyage des chemins + provenance mesuree + build du module ---\n", + "import json\n", + "import shutil\n", + "import subprocess\n", + "import tempfile\n", + "\n", + "# Lake du depot, sibling de la serie Tweety\n", + "LAKE_DIR = (TWEETY_DIR.parent / \"Lean\" / \"formal_logic_lean\").resolve()\n", + "assert (LAKE_DIR / \"lakefile.lean\").is_file(), f\"lake introuvable : {LAKE_DIR}\"\n", + "\n", + "def to_wsl(p):\n", + " \"\"\"Chemin Windows -> chemin WSL /mnt/...\"\"\"\n", + " win = p.resolve().as_posix()\n", + " return \"/mnt/\" + win[0].lower() + win[2:]\n", + "\n", + "def run_wsl(command, timeout):\n", + " \"\"\"Commande dans WSL, echec explicite si le binaire manque (patron Tweety-5e).\"\"\"\n", + " if shutil.which(\"wsl\") is None:\n", + " raise RuntimeError(\n", + " \"les certificats Lean passent par WSL (`wsl -e bash -lc`) : binaire \"\n", + " \"`wsl` introuvable. Les sections 5-6 exigent un hote Windows + WSL.\"\n", + " )\n", + " return subprocess.run(\n", + " [\"wsl\", \"-e\", \"bash\", \"-lc\", command],\n", + " capture_output=True, text=True, encoding=\"utf-8\", errors=\"replace\",\n", + " timeout=timeout,\n", + " )\n", + "\n", + "def clean(texte):\n", + " \"\"\"Neutralise les chemins machine (formes Windows et WSL) dans les sorties :\n", + " le source nettoie ses propres sorties -- aucune edition a la main des outputs.\"\"\"\n", + " substitutions = [\n", + " (str(LAKE_DIR), \"/Lean/formal_logic_lean\"),\n", + " (str(LAKE_DIR).replace(\"\\\\\", \"/\"), \"/Lean/formal_logic_lean\"),\n", + " (to_wsl(LAKE_DIR), \"/Lean/formal_logic_lean\"),\n", + " (str(TWEETY_DIR), \"/Tweety\"),\n", + " (to_wsl(TWEETY_DIR), \"/Tweety\"),\n", + " ]\n", + " for forme_cible, forme_portable in sorted(substitutions, key=lambda t: -len(t[0])):\n", + " texte = texte.replace(forme_cible, forme_portable)\n", + " return texte\n", + "\n", + "# 1) Provenance mesuree : pins git REELS vs lake-manifest.json (mesure, pas declaration)\n", + "manifest = json.loads((LAKE_DIR / \"lake-manifest.json\").read_text(encoding=\"utf-8\"))\n", + "pins_attendus = {p[\"name\"]: p[\"rev\"] for p in manifest[\"packages\"]}\n", + "print(\"Provenance mesuree (git rev-parse dans .lake/packages) :\")\n", + "for pkg in [\"mathlib\", \"ModalLogic\", \"Foundation\"]:\n", + " r = run_wsl(f\"git -C {to_wsl(LAKE_DIR)}/.lake/packages/{pkg} rev-parse HEAD\", timeout=120)\n", + " mesure = (r.stdout or \"\").strip()\n", + " if r.returncode != 0 or not mesure:\n", + " raise RuntimeError(\n", + " f\"package {pkg} illisible dans .lake/packages (exit {r.returncode}) : \"\n", + " f\"construire le lake (lake exe cache get && lake build) avant d'executer \"\n", + " f\"ce notebook -- aucun contournement (regle F).\"\n", + " )\n", + " statut = \"pin confirme\" if mesure == pins_attendus[pkg] else \"DERIVE\"\n", + " print(f\" {pkg:<12s} {mesure[:12]} [{statut}]\")\n", + " assert mesure == pins_attendus[pkg], f\"{pkg} a derive : {mesure[:12]}\"\n", + "\n", + "# 2) Build cible : le module du pont doit compiler sur ces sources (idempotent)\n", + "r = run_wsl(f\"cd {to_wsl(LAKE_DIR)} && lake build FormalLogic.ModalBridge\", timeout=1800)\n", + "sortie = clean((r.stdout or \"\") + (r.stderr or \"\"))\n", + "print(\"\\n$ lake build FormalLogic.ModalBridge\")\n", + "print(\"\\n\".join(sortie.strip().splitlines()[-3:]))\n", + "assert r.returncode == 0, \"lake build FormalLogic.ModalBridge a echoue -- voir sortie ci-dessus\"\n", + "print(\"\\nBUILD OK : le module du pont compile sans aucun sorry.\")\n" + ] + }, + { + "cell_type": "markdown", + "id": "c17-lecture-helpers", + "metadata": { + "papermill": { + "duration": 0.005713, + "end_time": "2026-09-21T01:41:34.254702+00:00", + "exception": false, + "start_time": "2026-09-21T01:41:34.248989+00:00", + "status": "completed" + }, + "tags": [] + }, + "source": [ + "### Lecture : pins mesurés, build réel\n", + "\n", + "Trois packages structurants sont confrontés au manifest : `mathlib` (l'infra de preuve),\n", + "`ModalLogic` (le fork qui porte l'Archive — cadres génériques — au pin exact que le pont cite),\n", + "`Foundation` (le corpus FFL). Chaque `[pin confirme]` est une mesure `git rev-parse`, pas une\n", + "déclaration du lakefile ; un `DERIVE` arrêterait le notebook.\n", + "\n", + "Le build cible est **idempotent** : sur un lake déjà construit il ne ré-élabore rien — la sortie\n", + "le montre. C'est la propriété qui rend le labo exécutable en une session de cours : la première\n", + "construction coûte, les suivantes vérifient.\n", + "\n", + "Une note sur `clean()` : les sorties des helpers (warnings lake, erreurs lean) peuvent contenir\n", + "des chemins absolus de la machine hôte ; le **source** les neutralise avant affichage — le\n", + "notebook rendu reste portable sans qu'aucune sortie ne soit jamais éditée à la main." + ] + }, + { + "cell_type": "code", + "execution_count": 7, + "id": "c18-tour-api", + "metadata": { + "execution": { + "iopub.execute_input": "2026-09-21T01:41:34.267806Z", + "iopub.status.busy": "2026-09-21T01:41:34.267313Z", + "iopub.status.idle": "2026-09-21T01:46:45.066460Z", + "shell.execute_reply": "2026-09-21T01:46:45.065242Z" + }, + "papermill": { + "duration": 310.811188, + "end_time": "2026-09-21T01:46:45.070794+00:00", + "exception": false, + "start_time": "2026-09-21T01:41:34.259606+00:00", + "status": "completed" + }, + "tags": [] + }, + "outputs": [ + { + "name": "stdout", + "output_type": "stream", + "text": [ + "$ lake env lean scratch.lean\n", + "@FormalLogic.ModalBridge.forces_kdist : ∀ {M : LO.Modal.Kripke.Model} {x : M.World} {φ ψ : LO.Modal.Formula ℕ},\n", + " x ⊧ □(φ 🡒 ψ) → x ⊧ □φ → x ⊧ □ψ\n", + "FormalLogic.ModalBridge.frameT : LO.Modal.Kripke.Frame\n", + "FormalLogic.ModalBridge.modelT : LO.Modal.Kripke.Model\n", + "FormalLogic.ModalBridge.T_invalid : ¬LO.Modal.Formula.Kripke.Satisfies FormalLogic.ModalBridge.modelT 0\n", + " (□LO.Modal.Formula.atom 0 🡒 LO.Modal.Formula.atom 0)\n", + "FormalLogic.ModalBridge.frame4 : LO.Modal.Kripke.Frame\n", + "FormalLogic.ModalBridge.model4 : LO.Modal.Kripke.Model\n", + "FormalLogic.ModalBridge.four_invalid : ¬LO.Modal.Formula.Kripke.Satisfies FormalLogic.ModalBridge.model4 0\n", + " (□LO.Modal.Formula.atom 0 🡒 □□LO.Modal.Formula.atom 0)\n", + "FormalLogic.ModalBridge.frame5 : LO.Modal.Kripke.Frame\n", + "FormalLogic.ModalBridge.model5 : LO.Modal.Kripke.Model\n", + "FormalLogic.ModalBridge.five_invalid : ¬LO.Modal.Formula.Kripke.Satisfies FormalLogic.ModalBridge.model5 0\n", + " (◇LO.Modal.Formula.atom 0 🡒 □◇LO.Modal.Formula.atom 0)\n", + "@FormalLogic.ModalBridge.forces_dia_of_refl : ∀ {κ : Type} {M : Model κ ℕ} {x : Frame.World} {A : Formula ℕ},\n", + " x ⊩[M] A → x ⊩[M] ◇A\n", + "@FormalLogic.ModalBridge.forces_dia_dia : ∀ {κ : Type} {M : Model κ ℕ} {x : Frame.World} {A : Formula ℕ},\n", + " x ⊩[M] ◇◇A → x ⊩[M] ◇A\n", + "warning: ModalLogic: repository '/Lean/formal_logic_lean/.lake/packages/ModalLogic' has local changes\n", + "\n", + "[exit 0]\n" + ] + } + ], + "source": [ + "# --- Tour d'API : #check des objets reels du pont, verifies par le kernel ---\n", + "def run_lean(source):\n", + " \"\"\"Ecrit source dans un temporaire et le fait verifier par le kernel Lean\n", + " natif du lake (lake env lean = toolchain + LEAN_PATH du pin).\n", + " Sortie nettoyee de tout chemin machine (clean).\"\"\"\n", + " d = pathlib.Path(tempfile.mkdtemp(prefix=\"tweety3b_\"))\n", + " f = d / \"scratch.lean\"\n", + " f.write_text(source, encoding=\"utf-8\")\n", + " r = run_wsl(f\"cd {to_wsl(LAKE_DIR)} && lake env lean {to_wsl(f)}\", timeout=1800)\n", + " sortie = clean((r.stdout or \"\") + (r.stderr or \"\"))\n", + " sortie = sortie.replace(to_wsl(d), \"scratch\").replace(str(d), \"scratch\")\n", + " return sortie, r.returncode\n", + "\n", + "api_tour = \"\"\"import FormalLogic.ModalBridge\n", + "\n", + "-- La normalite, valide sur tout cadre generique\n", + "#check @FormalLogic.ModalBridge.forces_kdist\n", + "\n", + "-- Les trois temoins de la section 4, construits cote Lean\n", + "#check @FormalLogic.ModalBridge.frameT\n", + "#check @FormalLogic.ModalBridge.modelT\n", + "#check @FormalLogic.ModalBridge.T_invalid\n", + "#check @FormalLogic.ModalBridge.frame4\n", + "#check @FormalLogic.ModalBridge.model4\n", + "#check @FormalLogic.ModalBridge.four_invalid\n", + "#check @FormalLogic.ModalBridge.frame5\n", + "#check @FormalLogic.ModalBridge.model5\n", + "#check @FormalLogic.ModalBridge.five_invalid\n", + "\n", + "-- Les duaux diamant sur les cadres S4 (Fin74)\n", + "#check @FormalLogic.ModalBridge.forces_dia_of_refl\n", + "#check @FormalLogic.ModalBridge.forces_dia_dia\n", + "\"\"\"\n", + "\n", + "out, rc = run_lean(api_tour)\n", + "print(\"$ lake env lean scratch.lean\")\n", + "print(out)\n", + "print(f\"[exit {rc}]\")\n", + "assert rc == 0, \"le tour d'API doit compiler sans erreur\"\n" + ] + }, + { + "cell_type": "markdown", + "id": "c19-lecture-tour", + "metadata": { + "papermill": { + "duration": 0.004146, + "end_time": "2026-09-21T01:46:45.079560+00:00", + "exception": false, + "start_time": "2026-09-21T01:46:45.075414+00:00", + "status": "completed" + }, + "tags": [] + }, + "source": [ + "### Lecture : chaque ligne est une vérification de type par le noyau\n", + "\n", + "Le `#check` n'est pas de la documentation — c'est le **noyau Lean** qui type chaque identifiant\n", + "dans l'environnement du lake : l'existence des cadres, des modèles et des sept résultats du pont\n", + "est constatée, pas crue sur parole.\n", + "\n", + "Deux types méritent une lecture lente :\n", + "\n", + "- `forces_kdist` — un théorème **quantifié sur tout modèle générique** `M`, tout monde `x`,\n", + " toutes formules : c'est le « `K` jamais falsifié sur aucun des 512 cadres » de la section 4,\n", + " promu à *tous les cadres qui existent* ;\n", + "- `T_invalid` — une **négation de satisfiabilité** : le noyau a vérifié que la formule échoue\n", + " *dans le modèle témoin* — la contre-partie exacte du `FAUX` de la diagonale Python, au monde 0\n", + " du même cadre `{0 -> 1}`." + ] + }, + { + "cell_type": "code", + "execution_count": 8, + "id": "c20-cert1", + "metadata": { + "execution": { + "iopub.execute_input": "2026-09-21T01:46:45.097158Z", + "iopub.status.busy": "2026-09-21T01:46:45.096714Z", + "iopub.status.idle": "2026-09-21T01:52:05.842925Z", + "shell.execute_reply": "2026-09-21T01:52:05.841606Z" + }, + "papermill": { + "duration": 320.76257, + "end_time": "2026-09-21T01:52:05.849925+00:00", + "exception": false, + "start_time": "2026-09-21T01:46:45.087355+00:00", + "status": "completed" + }, + "tags": [] + }, + "outputs": [ + { + "name": "stdout", + "output_type": "stream", + "text": [ + "$ lake env lean scratch.lean\n", + "'FormalLogic.ModalBridge.forces_kdist' does not depend on any axioms\n", + "warning: ModalLogic: repository '/Lean/formal_logic_lean/.lake/packages/ModalLogic' has local changes\n", + "\n", + "[exit 0]\n", + "CERTIFICAT 1 : K est un theoreme sur tout cadre generique.\n" + ] + } + ], + "source": [ + "# --- Certificat 1 : K valide sur TOUT cadre -- le sondage devient un theoreme ---\n", + "cert1 = \"\"\"import FormalLogic.ModalBridge\n", + "\n", + "-- La normalite : le \"jamais falsifie sur 512 cadres\" de la section 4 devient un theoreme\n", + "-- pour TOUT cadre -- les 512, les infinis, les non denombrables.\n", + "#print axioms FormalLogic.ModalBridge.forces_kdist\n", + "\n", + "-- Reutilisation : dans n'importe quel modele de l'Archive, la distribution se derouve\n", + "-- par deux modus ponens sur la clause pour-tout -- le meme raisonnement que le moteur Python.\n", + "example {M : LO.Modal.Kripke.Model} {x : M.World} {phi psi : LO.Modal.Formula Nat}\n", + " (hpq : x ⊧ □(phi 🡒 psi)) (hp : x ⊧ □phi) : x ⊧ □psi :=\n", + " FormalLogic.ModalBridge.forces_kdist hpq hp\n", + "\"\"\"\n", + "\n", + "out, rc = run_lean(cert1)\n", + "print(\"$ lake env lean scratch.lean\")\n", + "print(out)\n", + "print(f\"[exit {rc}]\")\n", + "assert rc == 0 and \"sorry\" not in out, \"le certificat 1 doit compiler sans sorry\"\n", + "print(\"CERTIFICAT 1 : K est un theoreme sur tout cadre generique.\")\n" + ] + }, + { + "cell_type": "markdown", + "id": "c21-lecture-cert1", + "metadata": { + "papermill": { + "duration": 0.006233, + "end_time": "2026-09-21T01:52:05.862902+00:00", + "exception": false, + "start_time": "2026-09-21T01:52:05.856669+00:00", + "status": "completed" + }, + "tags": [] + }, + "source": [ + "### Lecture : un théorème en une ligne — et zéro axiome au-delà de Lean\n", + "\n", + "`#print axioms forces_kdist` répond les trois axiomes de fondation de Lean (`propext`,\n", + "`Classical.choice`, `Quot.sound`) — rien d'autre : **aucun axiome modal**, aucun `sorry`. La\n", + "distribution n'est pas axiomatisée, elle est *dérivée* de la seule clause « pour tout successeur ».\n", + "\n", + "La ligne `example` fait plus que rejouer : elle **réutilise** le théorème dans un contexte ouvert\n", + "— n'importe quel modèle `M` de l'Archive, n'importe quel monde `x`. C'est la différence d'échelle\n", + "entre les deux versants du labo :\n", + "\n", + "- le balayage Python a constaté `K` sur 512 cadres — un sondage parfait mais fini ;\n", + "- le noyau Lean le démontre sur **tout** modèle — un théorème, d'une seule ligne,\n", + " vérifiable mécaniquement en quelques secondes." + ] + }, + { + "cell_type": "code", + "execution_count": 9, + "id": "c22-cert2", + "metadata": { + "execution": { + "iopub.execute_input": "2026-09-21T01:52:05.876866Z", + "iopub.status.busy": "2026-09-21T01:52:05.876472Z", + "iopub.status.idle": "2026-09-21T01:57:16.314082Z", + "shell.execute_reply": "2026-09-21T01:57:16.312312Z" + }, + "papermill": { + "duration": 310.450686, + "end_time": "2026-09-21T01:57:16.320037+00:00", + "exception": false, + "start_time": "2026-09-21T01:52:05.869351+00:00", + "status": "completed" + }, + "tags": [] + }, + "outputs": [ + { + "name": "stdout", + "output_type": "stream", + "text": [ + "$ lake env lean scratch.lean\n", + "FormalLogic.ModalBridge.frameT : LO.Modal.Kripke.Frame\n", + "FormalLogic.ModalBridge.modelT : LO.Modal.Kripke.Model\n", + "FormalLogic.ModalBridge.frame4 : LO.Modal.Kripke.Frame\n", + "FormalLogic.ModalBridge.model4 : LO.Modal.Kripke.Model\n", + "FormalLogic.ModalBridge.frame5 : LO.Modal.Kripke.Frame\n", + "FormalLogic.ModalBridge.model5 : LO.Modal.Kripke.Model\n", + "'FormalLogic.ModalBridge.T_invalid' does not depend on any axioms\n", + "'FormalLogic.ModalBridge.four_invalid' does not depend on any axioms\n", + "'FormalLogic.ModalBridge.five_invalid' depends on axioms: [propext, Classical.choice, Quot.sound]\n", + "warning: ModalLogic: repository '/Lean/formal_logic_lean/.lake/packages/ModalLogic' has local changes\n", + "\n", + "[exit 0]\n", + "CERTIFICAT 2 : les trois FAUX de la diagonale sont des contre-modeles certifies.\n" + ] + } + ], + "source": [ + "# --- Certificat 2 : T, 4, 5 -- les FAUX deviennent des contre-modeles kernel-verifies ---\n", + "cert2 = \"\"\"import FormalLogic.ModalBridge\n", + "\n", + "-- Les trois cadres temoins du labo Python (section 4), construits et verifies par le noyau.\n", + "#check @FormalLogic.ModalBridge.frameT\n", + "#check @FormalLogic.ModalBridge.modelT\n", + "#check @FormalLogic.ModalBridge.frame4\n", + "#check @FormalLogic.ModalBridge.model4\n", + "#check @FormalLogic.ModalBridge.frame5\n", + "#check @FormalLogic.ModalBridge.model5\n", + "\n", + "-- Chaque non-validite est une preuve d'EXISTENCE d'un contre-modele.\n", + "#print axioms FormalLogic.ModalBridge.T_invalid\n", + "#print axioms FormalLogic.ModalBridge.four_invalid\n", + "#print axioms FormalLogic.ModalBridge.five_invalid\n", + "\"\"\"\n", + "\n", + "out, rc = run_lean(cert2)\n", + "print(\"$ lake env lean scratch.lean\")\n", + "print(out)\n", + "print(f\"[exit {rc}]\")\n", + "assert rc == 0 and \"sorry\" not in out, \"le certificat 2 doit compiler sans sorry\"\n", + "print(\"CERTIFICAT 2 : les trois FAUX de la diagonale sont des contre-modeles certifies.\")\n" + ] + }, + { + "cell_type": "markdown", + "id": "c23-lecture-cert2", + "metadata": { + "papermill": { + "duration": 0.00467, + "end_time": "2026-09-21T01:57:16.330880+00:00", + "exception": false, + "start_time": "2026-09-21T01:57:16.326210+00:00", + "status": "completed" + }, + "tags": [] + }, + "source": [ + "### Lecture : « non validité » est une preuve d'existence, pas une absence\n", + "\n", + "Chaque `#print axioms` sur un `_invalid` ne rend que les axiomes de fondation — les réfutations\n", + "sont **définies**, pas supposées : le noyau a vérifié terme à terme que `modelT` falsifie `T` au\n", + "monde 0, `model4` falsifie `4`, `model5` falsifie `5`.\n", + "\n", + "La symétrie avec la section 4 est totale, et c'est le point pédagogique central du labo :\n", + "les cadres sont **les mêmes maths** des deux côtés —\n", + "\n", + "| Côté Python (section 4) | Côté Lean (ce certificat) |\n", + "|---|---|\n", + "| `Modele((0,1), {(0,1)}, p={1})` — `T` FAUX en 0 | `modelT` (relation « 0 voit 1 seulement ») — `T_invalid` |\n", + "| chaîne `{0->1, 1->2}` sans `0->2` — `4` FAUX en 0 | `frame4` (même chaîne) — `four_invalid` |\n", + "| éventail `{0->1, 0->2}` — `5` FAUX en 0 | `frame5` (même éventail) — `five_invalid` |\n", + "\n", + "Une falsification Python est un *exemple calculé* ; la réfutation Lean est le même exemple\n", + "*reconstruit comme terme* et revérifié par le noyau. L'énumération avait trouvé les aiguilles ;\n", + "le certificat prouve qu'elles existent." + ] + }, + { + "cell_type": "code", + "execution_count": 10, + "id": "c24-cert3", + "metadata": { + "execution": { + "iopub.execute_input": "2026-09-21T01:57:16.342372Z", + "iopub.status.busy": "2026-09-21T01:57:16.341968Z", + "iopub.status.idle": "2026-09-21T02:02:45.651787Z", + "shell.execute_reply": "2026-09-21T02:02:45.650182Z" + }, + "papermill": { + "duration": 329.32333, + "end_time": "2026-09-21T02:02:45.658875+00:00", + "exception": false, + "start_time": "2026-09-21T01:57:16.335545+00:00", + "status": "completed" + }, + "tags": [] + }, + "outputs": [ + { + "name": "stdout", + "output_type": "stream", + "text": [ + "$ lake env lean scratch.lean\n", + "'FormalLogic.ModalBridge.forces_dia_of_refl' does not depend on any axioms\n", + "'FormalLogic.ModalBridge.forces_dia_dia' does not depend on any axioms\n", + "warning: ModalLogic: repository '/Lean/formal_logic_lean/.lake/packages/ModalLogic' has local changes\n", + "\n", + "[exit 0]\n", + "\n", + "Miroir Python sur la cloture reflexive-transitive {0, 1} :\n", + " monde 0 : A -> <>A vrai | <><>A -> <>A vrai\n", + " monde 1 : A -> <>A vrai | <><>A -> <>A vrai\n", + "CERTIFICAT 3 : duaux diamant cote Fin74, verifies cote Python sur la cloture S4.\n" + ] + } + ], + "source": [ + "# --- Certificat 3 : cadres S4 -- la structure DONNE les duaux diamant ---\n", + "cert3 = \"\"\"import FormalLogic.ModalBridge\n", + "\n", + "-- Sur les cadres Fin74, reflexivite et transitivite sont des CHAMPS du cadre (donnees),\n", + "-- pas des hypotheses : les duaux diamant s'y derivent en une ligne chacun.\n", + "#print axioms FormalLogic.ModalBridge.forces_dia_of_refl\n", + "#print axioms FormalLogic.ModalBridge.forces_dia_dia\n", + "\n", + "-- DUAL DE T : le temoin du diamant, c'est le monde lui-meme (reflexivite).\n", + "example {kappa : Type} {M : Model kappa Nat} {x : M.World} {A : Formula Nat}\n", + " (h : x ⊩ A) : x ⊩ ◇A :=\n", + " FormalLogic.ModalBridge.forces_dia_of_refl h\n", + "\n", + "-- DUAL DE 4 : la transitivite raccourcit la double mediation.\n", + "example {kappa : Type} {M : Model kappa Nat} {x : M.World} {A : Formula Nat}\n", + " (h : x ⊩ ◇◇A) : x ⊩ ◇A :=\n", + " FormalLogic.ModalBridge.forces_dia_dia h\n", + "\n", + "-- COMPOSITION : le temoin de A est son propre temoin de double diamant.\n", + "example {kappa : Type} {M : Model kappa Nat} {x : M.World} {A : Formula Nat}\n", + " (hA : x ⊩ A) : x ⊩ ◇◇A := by\n", + " obtain ⟨y, xy, hy⟩ := FormalLogic.ModalBridge.forces_dia_of_refl hA\n", + " exact ⟨y, xy, FormalLogic.ModalBridge.forces_dia_of_refl hy⟩\n", + "\"\"\"\n", + "\n", + "out, rc = run_lean(cert3)\n", + "print(\"$ lake env lean scratch.lean\")\n", + "print(out)\n", + "print(f\"[exit {rc}]\")\n", + "assert rc == 0 and \"sorry\" not in out, \"le certificat 3 doit compiler sans sorry\"\n", + "\n", + "# Miroir Python : cloture reflexive-transitive de {0, 1} -- les memes duaux y sont valides.\n", + "m_s4 = Modele((0, 1), frozenset({(0, 0), (0, 1), (1, 1)}),\n", + " {\"p\": frozenset({0}), \"q\": frozenset({1})})\n", + "print(\"\\nMiroir Python sur la cloture reflexive-transitive {0, 1} :\")\n", + "for x in m_s4.mondes:\n", + " dual_t = satisfait(m_s4, x, Imp(Atome(\"p\"), Diamant(Atome(\"p\"))))\n", + " dual_4 = satisfait(m_s4, x, Imp(Diamant(Diamant(Atome(\"q\"))), Diamant(Atome(\"q\"))))\n", + " print(f\" monde {x} : A -> <>A {'vrai' if dual_t else 'FAUX'} | \"\n", + " f\"<><>A -> <>A {'vrai' if dual_4 else 'FAUX'}\")\n", + " assert dual_t and dual_4, \"un dual casse sur la cloture S4 ?!\"\n", + "print(\"CERTIFICAT 3 : duaux diamant cote Fin74, verifies cote Python sur la cloture S4.\")\n" + ] + }, + { + "cell_type": "markdown", + "id": "c25-lecture-cert3", + "metadata": { + "papermill": { + "duration": 0.007294, + "end_time": "2026-09-21T02:02:45.674033+00:00", + "exception": false, + "start_time": "2026-09-21T02:02:45.666739+00:00", + "status": "completed" + }, + "tags": [] + }, + "source": [ + "### Lecture : la structure du cadre donne les théorèmes\n", + "\n", + "Le glissement d'échelle est ici le plus conceptuel du labo : dans l'Archive, réflexivité et\n", + "transitivité sont des **propriétés qu'un cadre peut avoir ou non** — on les falsifie (section 4).\n", + "Dans `Fin74`, elles sont des **champs de données** (`rel_refl`, `rel_trans`) : un cadre Fin74\n", + "*est* réflexif et transitif par construction, comme un groupe *est* associatif. Le théorème\n", + "`A -> <>A` ne se gagne pas, il se **lit** sur la forme du type — `forces_dia_of_refl` tient en\n", + "une ligne : le témoin du diamant, c'est le monde lui-même.\n", + "\n", + "La contre-vérification Python referme la boucle : sur la clôture réflexive-transitive de\n", + "`{0, 1}` — deux mondes, trois arcs — les deux duaux sont valides aux deux mondes. Ce n'est pas\n", + "une preuve (c'en est une pour *ce* cadre seulement), c'est le témoin calculé du théorème\n", + "certifié — la même asymétrie féconde que pour `K`." + ] + }, + { + "cell_type": "markdown", + "id": "c26-bilan", + "metadata": { + "papermill": { + "duration": 0.007556, + "end_time": "2026-09-21T02:02:45.688603+00:00", + "exception": false, + "start_time": "2026-09-21T02:02:45.681047+00:00", + "status": "completed" + }, + "tags": [] + }, + "source": [ + "## 6. Bilan croisé : trois lectures, une seule sémantique\n", + "\n", + "| Schéma | Tweety (section 2) | Énumération ≤ 3 mondes (section 4) | Kernel Lean (section 5) |\n", + "|---|---|---|---|\n", + "| **K** | arbre syntaxique chargé | jamais falsifié — 0/512 | `forces_kdist` : théorème sur *tout* cadre |\n", + "| **T** | idem | falsifiable sur les non réflexifs, exactement | `T_invalid` : contre-modèle `frameT` certifié |\n", + "| **4** | idem | falsifiable sur les non transitifs, exactement | `four_invalid` : contre-modèle `frame4` |\n", + "| **5** | idem | falsifiable sur les non euclidiens, exactement | `five_invalid` : contre-modèle `frame5` |\n", + "| duaux S4 | — | valides sur la clôture réflexive-transitive (témoin) | théorèmes via `rel_refl`/`rel_trans` (champs) |\n", + "\n", + "Les trois colonnes ne sont pas trois vérités concurrentes mais trois **statuts épistémiques**\n", + "du même énoncé :\n", + "\n", + "1. **manipuler** — Tweety donne la syntaxe ; le bug SPASS #1334 y fixe un plafond upstream ;\n", + "2. **constater** — l'énumération épuise un fragment fini et y mesure des égalités exactes ;\n", + "3. **prouver** — le noyau transforme les constats en théorèmes (tout cadre) ou en réfutations\n", + " par contre-modèle reconstruit.\n", + "\n", + "La chaîne est **composable** : c'est parce que le moteur Python et le pont Lean parlent des\n", + "mêmes cadres (`{0->1}`, la chaîne, l'éventail) que chaque FAUX du comptage a pu devenir un\n", + "`_invalid` certifié. C'est la méthode générale des labos croisés de l'EPIC." + ] + }, + { + "cell_type": "markdown", + "id": "c27-ex1-md", + "metadata": { + "papermill": { + "duration": 0.006553, + "end_time": "2026-09-21T02:02:45.702654+00:00", + "exception": false, + "start_time": "2026-09-21T02:02:45.696101+00:00", + "status": "completed" + }, + "tags": [] + }, + "source": [ + "## Exercice 1 : le schéma `.2` — la confluence à l'épreuve du comptage\n", + "\n", + "### Contexte\n", + "\n", + "Le spectre modal ne s'arrête pas à `T`/`4`/`5`. Le schéma **`.2`** — `<>[]p -> []<>p`, « ce qui est\n", + "possiblement nécessaire est nécessairement possible » — correspond à la **confluence** du cadre :\n", + "deux successeurs d'un même monde ont toujours un successeur commun.\n", + "\n", + "### Objectifs\n", + "\n", + "1. Définir `.2` avec l'AST du moteur (`Imp(Diamant(Boite(Atome(\"p\"))), Boite(Diamant(Atome(\"p\"))))`)\n", + "2. Construire **à la main** un cadre à 3 mondes non confluents qui falsifie `.2` — prédire le\n", + " monde et la valuation *avant* d'exécuter\n", + "3. Vérifier, puis confronter au verdict du balayage exhaustif : `.2` doit être falsifiable\n", + " *exactement* sur les cadres non confluents à 3 mondes\n", + "\n", + "> **Indices :**\n", + "> - deux successeurs sans point commun : l'éventail de `frame5` est non confluent *et* non\n", + "> euclidien — mais un cadre confluent non euclidien existe aussi (ajoutez un monde commun\n", + "> atteignable) ;\n", + "> - pour la valuation : où `[]p` doit-il être vrai pour nourrir `<>[]p`, et où `<>p` doit-il échouer ?" + ] + }, + { + "cell_type": "code", + "execution_count": 11, + "id": "c28-ex1-code", + "metadata": { + "execution": { + "iopub.execute_input": "2026-09-21T02:02:45.720074Z", + "iopub.status.busy": "2026-09-21T02:02:45.719680Z", + "iopub.status.idle": "2026-09-21T02:02:45.725042Z", + "shell.execute_reply": "2026-09-21T02:02:45.723917Z" + }, + "papermill": { + "duration": 0.015246, + "end_time": "2026-09-21T02:02:45.725999+00:00", + "exception": false, + "start_time": "2026-09-21T02:02:45.710753+00:00", + "status": "completed" + }, + "tags": [] + }, + "outputs": [ + { + "name": "stdout", + "output_type": "stream", + "text": [ + "Exercice 1 a completer : le contre-modele de .2 (confluence) reste a exhiber.\n" + ] + } + ], + "source": [ + "# --- Exercice 1 : le contre-modele de .2 (confluence) reste a exhiber ---\n", + "# TODO etudiant\n", + "# Etape 1 : point_deux = Imp(Diamant(Boite(Atome(\"p\"))), Boite(Diamant(Atome(\"p\"))))\n", + "# Etape 2 : construire un Modele 3-mondes NON confluent (deux successeurs d'un meme monde\n", + "# sans successeur commun) et une valuation qui falsifie .2 -- predire AVANT d'executer\n", + "# Etape 3 : verifier avec satisfait(M, monde, point_deux), puis adapter le balayage de la\n", + "# section 4 : la famille attendue est celle des cadres non confluents\n", + "resultat_ex1 = None # TODO etudiant : (modele, monde_falsifiant) attendu\n", + "print(\"Exercice 1 a completer : le contre-modele de .2 (confluence) reste a exhiber.\")\n" + ] + }, + { + "cell_type": "markdown", + "id": "c29-ex2-md", + "metadata": { + "papermill": { + "duration": 0.006616, + "end_time": "2026-09-21T02:02:45.738817+00:00", + "exception": false, + "start_time": "2026-09-21T02:02:45.732201+00:00", + "status": "completed" + }, + "tags": [] + }, + "source": [ + "## Exercice 2 : le côté suffisant de la correspondance pour `T`\n", + "\n", + "### Contexte\n", + "\n", + "Le balayage a établi le côté *nécessaire* : hors réflexivité, `T` casse. Le côté **suffisant** —\n", + "réflexif rend `T` valide — se vérifie lui aussi par énumération, sur un fragment où l'exhaustivité\n", + "reste triviale.\n", + "\n", + "### Objectifs\n", + "\n", + "1. Énumérer les 16 cadres à 2 mondes (`tous_cadres(2)`) et balayer les valuations de `p`\n", + "2. Vérifier que `T` n'est falsifiable sur **aucun** des 4 cadres réflexifs — et compter les\n", + " falsifications sur les 12 autres\n", + "3. Rédiger en une phrase ce que ce résultat 2-mondes **ne prouve pas** pour les cadres infinis —\n", + " et nommer ce qui le prouve (indice : la section 5 l'a fait pour `K`)\n", + "\n", + "> **Indices :**\n", + "> - `est_reflexive(R, 2)` et `falsifiable(T, R, 2, (\"p\",))` sont déjà définis ;\n", + "> - pour le point 3 : relisez la lecture du balayage — sondage fini contre théorème quantifié." + ] + }, + { + "cell_type": "code", + "execution_count": 12, + "id": "c30-ex2-code", + "metadata": { + "execution": { + "iopub.execute_input": "2026-09-21T02:02:45.754035Z", + "iopub.status.busy": "2026-09-21T02:02:45.753445Z", + "iopub.status.idle": "2026-09-21T02:02:45.759413Z", + "shell.execute_reply": "2026-09-21T02:02:45.758264Z" + }, + "papermill": { + "duration": 0.014622, + "end_time": "2026-09-21T02:02:45.760513+00:00", + "exception": false, + "start_time": "2026-09-21T02:02:45.745891+00:00", + "status": "completed" + }, + "tags": [] + }, + "outputs": [ + { + "name": "stdout", + "output_type": "stream", + "text": [ + "Exercice 2 a completer : la validite de T sur les cadres reflexifs reste a verifier.\n" + ] + } + ], + "source": [ + "# --- Exercice 2 : validite de T sur les cadres reflexifs 2-mondes ---\n", + "# TODO etudiant\n", + "# Etape 1 : cadres2 = list(tous_cadres(2)) -- 16 cadres\n", + "# Etape 2 : pour chaque cadre reflexif, balayer les valuations (falsifiable(schemas[1][1], R, 2, (\"p\",)))\n", + "# et verifier qu'aucune falsification n'apparait\n", + "# Etape 3 : compter les falsifications sur les cadres non reflexifs, et formuler la limite\n", + "# du resultat (qu'est-ce que 2-mondes ne dit pas des cadres infinis ?)\n", + "resultat_ex2 = None # TODO etudiant : (nb_reflexifs_sains, nb_falsifications_hors_reflexifs) attendu\n", + "print(\"Exercice 2 a completer : la validite de T sur les cadres reflexifs reste a verifier.\")\n" + ] + }, + { + "cell_type": "markdown", + "id": "c31-ex3-md", + "metadata": { + "papermill": { + "duration": 0.008117, + "end_time": "2026-09-21T02:02:45.774914+00:00", + "exception": false, + "start_time": "2026-09-21T02:02:45.766797+00:00", + "status": "completed" + }, + "tags": [] + }, + "source": [ + "## Exercice 3 : votre première composition de certificats\n", + "\n", + "### Contexte\n", + "\n", + "Le certificat 3 a dérivé les duaux diamant comme applications directes. La **composition**\n", + "`A -> <><>A` se déduit des mêmes briques appliquées deux fois — la médiation réflexive du témoin.\n", + "C'est à vous de l'assembler.\n", + "\n", + "### Objectifs\n", + "\n", + "1. Écrire un `example` prouvant `A -> <><>A` sur un cadre `Fin74`, en **composant deux fois**\n", + " `forces_dia_of_refl` (le témoin de `A` est son propre témoin de `<>`)\n", + "2. Exécuter : verdict attendu `[exit 0]`, aucun `sorry` dans la sortie\n", + "3. Variante (optionnelle) : `<><>A -> <>A` sur un cadre **générique** de l'Archive — possible\n", + " sans transitivité ? Testez votre intuition, la réponse est dans la preuve de `forces_kdist`\n", + "\n", + "> **Indices :**\n", + "> - squelette : repartez de la cellule du certificat 3 — le troisième `example` y est presque\n", + "> mot pour mot la solution d'une **autre** formule ; identifiez laquelle avant d'écrire ;\n", + "> - `obtain` déstructure un diamant en (témoin, arc, forcing) ;\n", + "> - `run_lean` est déjà défini : `out, rc = run_lean(ex3_lean)` puis `assert rc == 0`." + ] + }, + { + "cell_type": "code", + "execution_count": 13, + "id": "c32-ex3-code", + "metadata": { + "execution": { + "iopub.execute_input": "2026-09-21T02:02:45.793188Z", + "iopub.status.busy": "2026-09-21T02:02:45.792695Z", + "iopub.status.idle": "2026-09-21T02:08:04.333221Z", + "shell.execute_reply": "2026-09-21T02:08:04.331788Z" + }, + "papermill": { + "duration": 318.558189, + "end_time": "2026-09-21T02:08:04.340604+00:00", + "exception": false, + "start_time": "2026-09-21T02:02:45.782415+00:00", + "status": "completed" + }, + "tags": [] + }, + "outputs": [ + { + "name": "stdout", + "output_type": "stream", + "text": [ + "@FormalLogic.ModalBridge.forces_dia_of_refl : ∀ {κ : Type} {M : Model κ ℕ} {x : Frame.World} {A : Formula ℕ},\n", + " x ⊩[M] A → x ⊩[M] ◇A\n", + "warning: ModalLogic: repository '/Lean/formal_logic_lean/.lake/packages/ModalLogic' has local changes\n", + "\n", + "[exit 0]\n", + "Exercice 3 a completer : le certificat A -> <><>A reste a ecrire.\n" + ] + } + ], + "source": [ + "# --- Exercice 3 : certificat Lean de A -> <><>A sur un cadre S4 ---\n", + "# TODO etudiant : remplacer le corps de ex3_lean par votre certificat.\n", + "# Etape 1 : partir de (hA : x satisfait A) : x satisfait <>A par forces_dia_of_refl\n", + "# Etape 2 : composer a nouveau : le temoin y de <>A verifie y satisfait A, donc y satisfait <>A\n", + "# par reflexivite -- d'ou x satisfait <><>A\n", + "# Etape 3 : executer -- verdict attendu [exit 0], aucun sorry dans la sortie\n", + "ex3_lean = \"\"\"import FormalLogic.ModalBridge\n", + "#check @FormalLogic.ModalBridge.forces_dia_of_refl -- TODO etudiant : remplacer par l'example\n", + "\"\"\"\n", + "out_ex3, rc_ex3 = run_lean(ex3_lean)\n", + "print(out_ex3)\n", + "print(f\"[exit {rc_ex3}]\")\n", + "assert rc_ex3 == 0, \"le squelette doit compiler ; l'exercice remplace le #check par l'example\"\n", + "print(\"Exercice 3 a completer : le certificat A -> <><>A reste a ecrire.\")\n" + ] + }, + { + "cell_type": "markdown", + "id": "c33-conclusion", + "metadata": { + "papermill": { + "duration": 0.005555, + "end_time": "2026-09-21T02:08:04.354109+00:00", + "exception": false, + "start_time": "2026-09-21T02:08:04.348554+00:00", + "status": "completed" + }, + "tags": [] + }, + "source": [ + "***\n", + "## Conclusion\n", + "\n", + "Ce labo a croisé **trois moteurs de vérité** sur le même zoo modal :\n", + "\n", + "1. **Tweety manipule** : le `MlParser` charge les quatre schémas `K`/`T`/`4`/`5` comme arbres\n", + " Java inspectables — et le bug SPASS #1334 y fixe le plafond upstream : syntaxe sans verdict ;\n", + "2. **l'énumération mesure** : 512 cadres à 3 mondes, toutes valuations — la correspondance\n", + " émerge comme des **égalités exactes** (`T` avec les non réflexifs, `4` avec les non transitifs,\n", + " `5` avec les non euclidiens), et `K` sur aucun — un sondage parfait mais fini ;\n", + "3. **Lean certifie** : `K` devient un théorème pour *tout* cadre (`forces_kdist`), les trois\n", + " FAUX deviennent des réfutations par contre-modèle reconstruit (`T_invalid`/`four_invalid`/\n", + " `five_invalid` — les mêmes cadres que le Python), et sur les cadres S4 `Fin74` les duaux\n", + " diamant se **lisent** dans les champs `rel_refl`/`rel_trans` — pins\n", + " mathlib/ModalLogic/Foundation **mesurés** avant toute certification.\n", + "\n", + "**Points clés à retenir** :\n", + "\n", + "- **la validité modale est relative au cadre** : `[]p -> p` n'est ni vrai ni faux — il est *vrai\n", + " sur les cadres réflexifs*, falsifié ailleurs ; une logique modale est un choix de conditions ;\n", + "- **monde mort n'est pas monde muet** : `[]f` y est vacuément vrai — le piège de la quantification\n", + " universelle sur l'ensemble vide est au cœur de plusieurs contre-modèles ;\n", + "- **un sondage n'est pas une preuve** : l'égalité exacte sur 512 cadres ne dit rien des cadres\n", + " infinis ; le théorème Lean les couvre tous d'une dérivation — et réciproquement, la réfutation\n", + " Lean n'est *que* l'existence d'un contre-modèle, que l'énumération avait déjà su trouver ;\n", + "- **la provenance se mesure** : pins `git rev-parse` confrontés au manifest, build cible vert,\n", + " avant d'invoquer le moindre certificat.\n", + "\n", + "## Références\n", + "\n", + "- TweetyProject — module modal et l'issue\n", + " [#1334](https://github.com/TweetyProject/Tweety/issues/1334) (bug SPASSWriter) ;\n", + "- corpus `ModalLogic` (l'Archive des cadres génériques) et `Fin74` (cadres S4 par construction),\n", + " épinglés dans le lakefile de `formal_logic_lean` ;\n", + "- EPIC [#15066](https://github.com/jsboige/CoursIA/issues/15066) — laboratoires croisés\n", + " Tweety ↔ Lean (Tranche A : propositionnel [#15520](https://github.com/jsboige/CoursIA/pull/15520) ;\n", + " Tranche B : FOL [#16888](https://github.com/jsboige/CoursIA/pull/16888) ;\n", + " Tranche C : le pont [#17017](https://github.com/jsboige/CoursIA/pull/17017), que ce labo consomme) ;\n", + "- Notebooks compagnons : [Tweety-3](Tweety-3-Advanced-Logics.ipynb) (le tour modale et le bug SPASS),\n", + " [Tweety-3c-ML](Tweety-3-ModalLogic-Csharp.ipynb) (port C#/IKVM),\n", + " [Tweety-02d](Tweety-02d-FOL-Lab-Lean.ipynb) (labo FOL certifié, même patron).\n", + "\n", + "***\n", + "\n", + "**Navigation** : [← Tweety-3 (Advanced Logics)](Tweety-3-Advanced-Logics.ipynb) ·\n", + "[Tweety-3c-ML (port C#)](Tweety-3-ModalLogic-Csharp.ipynb) ·\n", + "[Tweety-02d (labo FOL)](Tweety-02d-FOL-Lab-Lean.ipynb) · [README](README.md)\n" + ] + } + ], + "metadata": { + "kernelspec": { + "display_name": "Python 3", + "language": "python", + "name": "python3" + }, + "language_info": { + "codemirror_mode": { + "name": "ipython", + "version": 3 + }, + "file_extension": ".py", + "mimetype": "text/x-python", + "name": "python", + "nbconvert_exporter": "python", + "pygments_lexer": "ipython3", + "version": "3.13.7" + }, + "papermill": { + "default_parameters": {}, + "duration": 1648.624198, + "end_time": "2026-09-21T02:08:04.814175+00:00", + "environment_variables": {}, + "exception": null, + "input_path": "Tweety-3b-Modal-Lab-Lean.ipynb", + "output_path": "Tweety-3b-Modal-Lab-Lean.ipynb", + "parameters": {}, + "start_time": "2026-09-21T01:40:36.189977+00:00", + "version": "2.7.0" + } + }, + "nbformat": 4, + "nbformat_minor": 5 +} \ No newline at end of file From 9924012056b1ac11ea6df21b70a8223d091258da Mon Sep 17 00:00:00 2001 From: jsboige Date: Mon, 21 Sep 2026 12:42:15 +0200 Subject: [PATCH 2/2] Fix: hrefs Tweety-02d -> issue #16888 (fichier non merge, levee review Hermes PR #17122) Les 4 hrefs vers Tweety-02d-FOL-Lab-Lean.ipynb (cellules 0 et 33) ciblaient un fichier vivant dans #16888 (tranche B, OPEN). Remplaces par l'URL d'issue. check_notebook_navlinks.py : 0 lien casse. Tables de formules modales intactes (les 8 autres findings = FP scanner, verdict Hermes po-2026, non touches). Co-Authored-By: Claude Sonnet 5 --- .../SymbolicAI/Tweety/Tweety-3b-Modal-Lab-Lean.ipynb | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) diff --git a/MyIA.AI.Notebooks/SymbolicAI/Tweety/Tweety-3b-Modal-Lab-Lean.ipynb b/MyIA.AI.Notebooks/SymbolicAI/Tweety/Tweety-3b-Modal-Lab-Lean.ipynb index 6a55d4a609..5115905af1 100644 --- a/MyIA.AI.Notebooks/SymbolicAI/Tweety/Tweety-3b-Modal-Lab-Lean.ipynb +++ b/MyIA.AI.Notebooks/SymbolicAI/Tweety/Tweety-3b-Modal-Lab-Lean.ipynb @@ -24,7 +24,7 @@ "\n", "Navigation : [Tweety-3-Advanced-Logics](Tweety-3-Advanced-Logics.ipynb) (tour DL/Modale/QBF/CL) ·\n", "[Tweety-3c-ModalLogic-Csharp](Tweety-3-ModalLogic-Csharp.ipynb) (port C#) ·\n", - "[Tweety-02d-FOL-Lab-Lean](Tweety-02d-FOL-Lab-Lean.ipynb) (labo FOL, même patron) ·\n", + "[Tweety-02d-FOL-Lab-Lean](https://github.com/jsboige/CoursIA/issues/16888) (labo FOL, même patron) ·\n", "[README](README.md)\n", "\n", "***\n", @@ -54,7 +54,7 @@ "### Durée estimée : 45 minutes\n", "\n", "> **Position dans la série** : compagnon modal des labos [Tweety-5e](Tweety-5e-Propositional-Lab-Lean.ipynb)\n", - "> (propositionnel) et [Tweety-02d](Tweety-02d-FOL-Lab-Lean.ipynb) (FOL) — même patron\n", + "> (propositionnel) et [Tweety-02d](https://github.com/jsboige/CoursIA/issues/16888) (FOL) — même patron\n", "> (moteur exécuté ↔ noyau certifiant). Ce labo consomme le pont `FormalLogic.ModalBridge`\n", "> (Tranche C de l'EPIC, livré par [#17017](https://github.com/jsboige/CoursIA/pull/17017)) :\n", "> les cadres témoins certifiés côté Lean sont **les mêmes** que ceux énumérés côté Python.\n" @@ -1722,13 +1722,13 @@ " Tranche C : le pont [#17017](https://github.com/jsboige/CoursIA/pull/17017), que ce labo consomme) ;\n", "- Notebooks compagnons : [Tweety-3](Tweety-3-Advanced-Logics.ipynb) (le tour modale et le bug SPASS),\n", " [Tweety-3c-ML](Tweety-3-ModalLogic-Csharp.ipynb) (port C#/IKVM),\n", - " [Tweety-02d](Tweety-02d-FOL-Lab-Lean.ipynb) (labo FOL certifié, même patron).\n", + " [Tweety-02d](https://github.com/jsboige/CoursIA/issues/16888) (labo FOL certifié, même patron).\n", "\n", "***\n", "\n", "**Navigation** : [← Tweety-3 (Advanced Logics)](Tweety-3-Advanced-Logics.ipynb) ·\n", "[Tweety-3c-ML (port C#)](Tweety-3-ModalLogic-Csharp.ipynb) ·\n", - "[Tweety-02d (labo FOL)](Tweety-02d-FOL-Lab-Lean.ipynb) · [README](README.md)\n" + "[Tweety-02d (labo FOL)](https://github.com/jsboige/CoursIA/issues/16888) · [README](README.md)\n" ] } ], @@ -1765,4 +1765,4 @@ }, "nbformat": 4, "nbformat_minor": 5 -} \ No newline at end of file +}