diff --git a/MyIA.AI.Notebooks/SymbolicAI/Tweety/README.md b/MyIA.AI.Notebooks/SymbolicAI/Tweety/README.md index 98f478730c..b04f0111ed 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 et `Tweety-3b-Modal-Lab-Lean` laboratoire modal, soit **16 notebooks**) | +| **Python** (originelle) | JPype (pont Java↔Python) | Python 3 | Oui (JDK téléchargé par le setup) | `Tweety-1` à `Tweety-11` (+ `Tweety-02d-FOL-Lab-Lean` labo FOL croisé, `Tweety-02e-Preuves-Hilbert-Gentzen-Lean` calculs de preuve Hilbert/LK, `Tweety-5b-Lean-Argumentation` companion Lean 4, `Tweety-5d-Stable-Synthesis-Lean` synthèse Z3→Lean, `Tweety-5e-Propositional-Lab-Lean` laboratoire propositionnel et `Tweety-3b-Modal-Lab-Lean` laboratoire modal) | | **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). @@ -63,8 +63,8 @@ Cette série ne propose pas de choisir l'un ou l'autre, mais de **comprendre les | Statistique | Valeur | |-------------|--------| -| Notebooks | 32 (12 Python + 1 Lean + 18 C# + 1 probe) | -| Cellules totales | 916 (dont 371 code) | +| Notebooks | 37 racine (13 Python + 6 Lean companion + 18 C#) + 1 probe | +| Cellules totales | 1165 (dont 438 code) — 37 racine + 1 probe | | Durée estimée | ~6h (tutorat) | | Kernel | Python 3 (JPype/Java) | | Version Tweety | 1.30 recommandée | @@ -147,6 +147,8 @@ Pour les praticiens intéressés par les applications multi-agents : | 2a | [Tweety-2-Basic-Logics-Csharp](Tweety-02-Basic-Logics-CSharp.ipynb) | Logique propositionnelle .NET (IKVM, port pilot #4792) | 30 min | C# PROD | | 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 | +| 2d | [Tweety-02d-FOL-Lab-Lean](Tweety-02d-FOL-Lab-Lean.ipynb) | Labo FOL croisé (tranche B de l'EPIC [#15066](https://github.com/jsboige/CoursIA/issues/15066)) : un même syllogisme exécuté par `SimpleFolReasoner` (six verdicts) et certifié par le noyau Lean sur le corpus **FFL épinglé** — conséquences quantifiées sur toutes les structures, contre-modèles finis exhibés ; la distinction `FALSE` ≠ « négation prouvée » y est mesurée | 45 min | Python+Lean BETA | +| 2e | [Tweety-02e-Preuves-Hilbert-Gentzen-Lean](Tweety-02e-Preuves-Hilbert-Gentzen-Lean.ipynb) | Calculs de preuve (tranche D de l'EPIC [#15066](https://github.com/jsboige/CoursIA/issues/15066)) : les trois axiomes de Hilbert vérifiés par deux oracles réels, une preuve de Hilbert construite par **chaînage avant** (coût mesuré), puis le calcul des séquents **LK** — hauteur et taille d'un arbre **avant/après** élimination des coupures, le Hauptsatz étant invoqué comme **théorème du noyau** (`Derivation.Canonical.constructiveHauptsatz`, témoin `IsCutFree`) | 45 min | Python+Lean 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 | @@ -181,11 +183,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 **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). +**Durée totale estimée** : ~13h (Python) + ~10h (C#/.NET). Le tableau ci-dessus couvre les notebooks principaux (12 Python + 18 C#/.NET + 6 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 les fichiers `.lean` du dossier `Argumentation/` — les modules FR : Basic, Characteristic, Extensions, Fundamental, Grounded, Synthesis + leurs 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 **34 notebooks principaux** (12 Python + 18 C#/.NET + 4 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 notebooks principaux (12 Python + 18 C#/.NET + 6 Lean companion) : | # | Notebook | Concept clé enseigné | |----|-------------------------------|--------------------------------------------------------------------------| @@ -194,6 +196,8 @@ Chaque notebook introduit un concept ou cadre théorique spécifique. Le tableau | 2a | Basic Logics (C#, pilote) | Logique propositionnelle .NET — port pilote IKVM (#4792), premier pont Java→.NET de la série | | 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 | +| 2d | FOL Lab (Python+Lean) | Un syllogisme, deux moteurs : `SimpleFolReasoner` exécute six verdicts, le noyau Lean **certifie** conséquences (théorèmes) et non-conséquences (contre-modèles finis) — `FALSE` n'est pas « négation prouvée » | +| 2e | Preuves Hilbert/LK (Python+Lean) | Deux calculs de preuve mesurés : Hilbert (axiomes + MP, recherche par chaînage avant, coût en instances/MP) et séquents LK (hauteur/taille d'arbre **avant/après** élimination des coupures, Hauptsatz = théorème du noyau) | | 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 | @@ -401,6 +405,8 @@ Tweety/ ├── Tweety-02-Basic-Logics-CSharp.ipynb # Logique propositionnelle .NET (IKVM, PROD) ├── Tweety-02b-Semantics-CSharp.ipynb # Sémantique propositionnelle .NET (IKVM, BETA) ├── Tweety-02c-FOL-CSharp.ipynb # FOL .NET (IKVM, BETA) +├── Tweety-02d-FOL-Lab-Lean.ipynb # Labo FOL croisé Tweety/Lean (tranche B #15066) +├── Tweety-02e-Preuves-Hilbert-Gentzen-Lean.ipynb # Calculs de preuve Hilbert/LK (tranche D #15066) ├── 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) @@ -432,7 +438,7 @@ Tweety/ ├── Tweety-11-Causal-Csharp.ipynb # Twin C# moteur causal from-scratch (BCL, PROD) ├── tweety_init.py # Module d'initialisation JPype/JVM ├── requirements.txt # Dépendances Python (JPype1, etc.) -├── org.tweetyproject.tweety-*.dll # 18 assemblages .NET (shades IKVM, EPIC #4667) +├── org.tweetyproject.tweety-*.dll # 19 assemblages .NET (shades IKVM, EPIC #4667) ├── dotnet-build/ # Build Maven/.csproj des shades IKVM (EPIC #4667) ├── libs/ # JARs Tweety (42 : 39 modules 1.30 + 3 deps) — téléchargé ├── jdk-17-portable/ # JDK Zulu — téléchargé auto par le setup @@ -451,7 +457,7 @@ Tweety/ └── README.md # Ce fichier ``` -> **Note** : les dossiers `libs/`, `jdk-17-portable/`, `ext_tools/` et `resources/` sont des répertoires d'exécution (non suivis par Git, téléchargés automatiquement par `Tweety-01-Setup-Python.ipynb` ou `scripts/download_tweety_tools.py`). L'ancien dossier `templates student/` n'existe plus dans cette partition. `scripts/` contient 5 scripts `.py` au premier niveau (`download_tweety_tools.py`, `verify_all_tweety.py`, `validate_syntax.py`, `sat_calibration.py`, `sat_comparison_demo.py`), 4 tests `test_*.py` et un `README.md`, plus un sous-dossier `_archive/` (qui contient `reorganize_tweety.py`, déplacé depuis le premier niveau — plus de doublon). Le dossier `_output/` n'est pas présent dans cette partition (les traces Papermill ne sont pas conservées). Audit §E whole-file gate 2026-07-15, re-audit 2026-08-15. +> **Note** : les dossiers `libs/`, `jdk-17-portable/`, `ext_tools/` et `resources/` sont des répertoires d'exécution (non suivis par Git, téléchargés automatiquement par `Tweety-01-Setup-Python.ipynb` ou `scripts/download_tweety_tools.py`). L'ancien dossier `templates student/` n'existe plus dans cette partition. `scripts/` contient 5 scripts `.py` au premier niveau (`download_tweety_tools.py`, `verify_all_tweety.py`, `validate_syntax.py`, `sat_calibration.py`, `sat_comparison_demo.py`), 4 tests `test_*.py` et un `README.md`, plus un sous-dossier `_archive/` (qui contient `reorganize_tweety.py`, déplacé depuis le premier niveau — plus de doublon). Le dossier `_output/` n'est pas présent dans cette partition (les traces Papermill ne sont pas conservées). Audit §E whole-file gate 2026-07-15, re-audit 2026-08-15, re-audit fichier-entier 2026-09-25 (comptes de notebooks, cellules et durées re-mesurés sur disque — périmètre et résidus déclarés dans l'entrée de changelog). ## Outils Externes @@ -737,23 +743,24 @@ Le pitch de Tweety tient en un mot : **explicabilité**. Là où un LLM produit --- -**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.** +**Version 1.2.5 — Septembre 2026 — entrée README de `Tweety-02e-Preuves-Hilbert-Gentzen-Lean` (tranche D de l'EPIC #15066, atelier calculs de preuve : les trois axiomes de Hilbert vérifiés par deux oracles réels, une preuve construite par chaînage avant — coût mesuré en instances/MP, plus une contre-expérience qui **réfute par la mesure** l'hypothèse d'un vivier simplement trop étroit — le syllogisme hypothétique, valide pour les deux oracles, n'est pas dérivé par le moteur, et l'élargir aux sous-formules de la cible ne suffit pas — puis le calcul des séquents LK dont la hauteur et la taille sont mesurées **avant/après** élimination des coupures, le Hauptsatz étant invoqué comme théorème du noyau `Derivation.Canonical.constructiveHauptsatz`, témoin `IsCutFree` inclus). Surfaces touchées : table Structure (+ entrée 2e), table « En quoi chaque notebook est unique » (+ entrée), arbre de structure, statistiques par sous-catégorie (Lean companion 4 → 6, total 35 → 38 — le recensement inclut désormais `Tweety-12-Grounded-Via-TweetyProject`, jusqu'ici hors comptes, avec sa maturité déclarée absente plutôt qu'inventée) et colonne Python du tableau des stacks (16 → 18). Le même geste comble un écart **non déclaré** : `Tweety-02d-FOL-Lab-Lean` (tranche B, #16877), présent sur disque depuis sa livraison mais absent des deux tables, y entre avec sa **propre** durée déclarée (45 minutes, lue dans le notebook) — aucune durée inventée. Trois écarts mesurés et corrigés au passage : les comptes de notebooks (« 32 » de la vue d'ensemble → 37 racine, dont 36 tabulés ; 34 → 36 principaux), les cellules totales (916 → 1165, mesurées sur l'ensemble des fichiers de la série) et les durées agrégées (Python ~13h, C#/.NET ~10h — la somme de la colonne C# valait déjà 585 min contre « ~7h » annoncées) ; l'arbre annonçait par ailleurs 18 assemblages .NET, `git ls-tree origin/main` en compte **19**. Résidus déclarés, non comblés ici : `Tweety-12-Grounded-Via-TweetyProject` reste absent des tables (13e notebook Python ; sa durée n'est déclarée nulle part — même résidu que v1.2.3 et v1.2.4, aucune ligne inventée) ; la ligne « Durée estimée ~6h (tutorat) » de la vue d'ensemble n'est pas re-dérivée (notion distincte de la somme par notebook, non mesurable depuis le disque) ; et le versant Lean de la tranche D reste **dans le notebook** — les deux fichiers d'index du lake (`FormalLogic/../FormalLogic.lean` et son `README.md`) sont sous claim actif d'une autre lane (`check_lane_claim.py`, verdict `BLOCKED` au 2026-09-25), aucun module de pont n'a donc été ajouté à `formal_logic_lean/`. Précédent : 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 (+ entrée 3b, notebooks principaux 33 → 34), table « En quoi chaque notebook est unique » (+ entrée), 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 (notebooks principaux 32 → 33), table « En quoi chaque notebook est unique » (ajout de 5d et 5e, lignes 31 → 33), 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 : notebooks 33, cellules 969 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 -Statistiques détaillées de la sous-série Tweety. Le `pedagogical_count: 32` est lu depuis le marqueur `` (l. 5-10). Le détail par sous-catégorie ci-dessous est réconcilié avec les étiquettes par-notebook du tableau **Structure** (source granulaire). NB : le marqueur actuel indique `maturity: BETA=30, ALPHA=2` — l'heuristique catalogue ne distingue pas les statuts PROD/BETA/DRAFT du tableau **Structure** (qui fait foi au niveau granulaire, DRAFT = `Tweety-3-Advanced-Logics-Csharp` BROKEN inclus) ; la prose ne s'aligne donc pas sur le marqueur (cf. catalog-pr-hygiene : ne pas s'aligner sur un catalogue faux) : +Statistiques détaillées de la sous-série Tweety. Le `pedagogical_count: 36` est lu depuis le marqueur `` (l. 5-10). Le détail par sous-catégorie ci-dessous est réconcilié avec les étiquettes par-notebook du tableau **Structure** (source granulaire). NB : le marqueur indique `maturity: BETA=33, ALPHA=3` — l'heuristique catalogue ne distingue pas les statuts PROD/BETA/DRAFT du tableau **Structure** (qui fait foi au niveau granulaire, DRAFT = `Tweety-3-Advanced-Logics-Csharp` BROKEN inclus) ; la prose ne s'aligne donc pas sur le marqueur (cf. catalog-pr-hygiene : ne pas s'aligner sur un catalogue faux). Un écart d'une unité subsiste, et il est **attendu** : le marqueur, régénéré par l'automatisation, décrit `main` **avant** l'ajout de `Tweety-02e` (36 racine), quand le recensement de cette page en compte **37** — le bloc `CATALOG-STATUS` n'est jamais réécrit à la main sur une branche feature (`catalog-pr-hygiene`), la résorption se fait donc à la prochaine régénération, pas ici : | Sous-catégorie | NB | Statut | |-----------------------|-------|------------------------------| | Python (Tw-1..11) | 12 | PROD=12 | -| Lean companion (5b, 5d, 5e, 3b) | 4 | BETA=4 | +| `Tweety-12-Grounded` (non tabulé) | 1 | maturité non déclarée | +| Lean companion (2d, 2e, 3b, 5b, 5d, 5e) | 6 | BETA=6 | | C#/.NET | 18 | PROD=12, BETA=5, DRAFT=1 | | Probe `_probes/` | 1 | BETA | -| Total | 35 | PROD=24, BETA=10, DRAFT=1 | +| Total | 38 | PROD=24, BETA=12, DRAFT=1, non déclarée=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é) 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). +- **Python (JPype, 13 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. Les six companions **Lean** viennent en supplément : `Tweety-02d-FOL-Lab-Lean` (BETA, kernels Python + Lean, tranche B de l'EPIC #15066 : un même syllogisme exécuté par `SimpleFolReasoner` et certifié sur le corpus FFL épinglé — conséquences quantifiées, contre-modèles finis exhibés) et `Tweety-02e-Preuves-Hilbert-Gentzen-Lean` (BETA, kernels Python + Lean, tranche D de l'EPIC #15066 : axiomes de Hilbert vérifiés par deux oracles, preuve construite par chaînage avant, puis hauteur/taille d'une dérivation LK **avant/après** élimination des coupures par le Hauptsatz du noyau), puis `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-02e-Preuves-Hilbert-Gentzen-Lean.ipynb b/MyIA.AI.Notebooks/SymbolicAI/Tweety/Tweety-02e-Preuves-Hilbert-Gentzen-Lean.ipynb new file mode 100644 index 0000000000..1b796ccc1b --- /dev/null +++ b/MyIA.AI.Notebooks/SymbolicAI/Tweety/Tweety-02e-Preuves-Hilbert-Gentzen-Lean.ipynb @@ -0,0 +1,1582 @@ +{ + "cells": [ + { + "cell_type": "markdown", + "id": "3c12b4db", + "metadata": { + "papermill": { + "duration": 0.006341, + "end_time": "2026-09-25T05:11:55.779586+00:00", + "exception": false, + "start_time": "2026-09-25T05:11:55.773245+00:00", + "status": "completed" + }, + "tags": [] + }, + "source": [ + "# Tweety-02e — Calculs de preuve : Hilbert, séquents, Hauptsatz\n", + "\n", + "> **Série Tweety — laboratoires croisés Java ↔ Lean (EPIC [#15066](https://github.com/jsboige/CoursIA/issues/15066), Tranche D).**\n", + "> Une même question — *comment calcule-t-on une preuve ?* — posée à trois moteurs : le système de\n", + "> **Hilbert** (axiomes + modus ponens) et les **oracles** de Tweety (Java, via JPype) qui décident,\n", + "> le **calcul des séquents LK** de Gentzen dont l'élimination des coupures est un **théorème du noyau**\n", + "> Lean dans le lake `formal_logic_lean` (corpus FFL épinglé).\n", + "\n", + "Navigation : [Tweety-02d-FOL-Lab-Lean](Tweety-02d-FOL-Lab-Lean.ipynb) (labo FOL) ·\n", + "[Tweety-5e-Propositional-Lab-Lean](Tweety-5e-Propositional-Lab-Lean.ipynb) (labo propositionnel) ·\n", + "[Tweety-02-Basic-Logics-Python](Tweety-02-Basic-Logics-Python.ipynb) (PL exécutée) ·\n", + "[README](README.md)\n", + "\n", + "***\n", + "\n", + "## Objectifs pédagogiques\n", + "\n", + "1. **Vérifier** les trois schémas d'axiomes de Hilbert par **deux oracles réels** (`SimplePlReasoner`, `SatReasoner`) — et comprendre pourquoi « tautologie » est un *verdict*, pas une preuve\n", + "2. **Construire** une preuve de Hilbert par **chaînage avant** (instanciation des schémas + modus ponens), et mesurer son coût : instances générées, formules dérivées, applications de MP\n", + "3. **Mesurer** les deux régimes de preuve dans le calcul des séquents **LK** : hauteur et taille d'un arbre, **avec** et **sans** coupure\n", + "4. **Invoquer le Hauptsatz comme un théorème** — `Derivation.Canonical.constructiveHauptsatz` rend la dérivation sans coupure *et* le témoin `IsCutFree`, vérifiés par le noyau Lean\n", + "5. **Lire un résultat négatif honnêtement** : la recherche Hilbert ne trouve pas tout ce que l'oracle décide — le vivier d'instanciation, pas la logique, en est la cause\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 propositionnelles : [Tweety-02](Tweety-02-Basic-Logics-Python.ipynb) (connecteurs, satisfaisabilité)\n", + "- Pour les sections 4-5 : hôte Windows + WSL avec le lake `Lean/formal_logic_lean` construit — les cellules **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** : troisième labo croisé de l'EPIC #15066, après le propositionnel\n", + "> ([Tweety-5e](Tweety-5e-Propositional-Lab-Lean.ipynb), Tranche A) et le FOL\n", + "> ([Tweety-02d](Tweety-02d-FOL-Lab-Lean.ipynb), Tranche B) — même patron *moteur exécuté ↔ noyau\n", + "> certifiant*, mais le sujet n'est plus **le verdict** d'un raisonneur : c'est **l'objet preuve**\n", + "> lui-même, mesuré dans deux calculs différents." + ] + }, + { + "cell_type": "markdown", + "id": "875621ad", + "metadata": { + "papermill": { + "duration": 0.006462, + "end_time": "2026-09-25T05:11:55.794711+00:00", + "exception": false, + "start_time": "2026-09-25T05:11:55.788249+00:00", + "status": "completed" + }, + "tags": [] + }, + "source": [ + "## 1. La question du labo\n", + "\n", + "Trois traditions répondent à « pourquoi cette formule est-elle vraie ? » de trois façons irréductibles l'une à l'autre.\n", + "\n", + "1. **Hilbert** : on fixe des schémas d'axiomes et **une** règle, le modus ponens. Une preuve est une liste finie de formules ; les axiomes sont *vrais par décret*, chaque étape est justifiée par MP. Trouver une preuve = **chercher** dans l'espace des formules dérivables — coûteux, mais chaque objet produit est vérifiable ligne à ligne, sans sémantique.\n", + "2. **Gentzen (LK)** : on fixe des règles d'inférence qui transforment des **séquents** (multi-ensembles de formules). Une preuve est un **arbre**. La règle de **coupure** (*cut*) a la même puissance que MP, mais elle coupe un arbre en deux : elle raccourcit les preuves et complique leur lecture. Le **Hauptsatz** de Gentzen dit que toute coupure peut être éliminée — la preuve grandit, mais devient « analytique » : chaque formule y est sous-formule de la conclusion.\n", + "3. **Oracle sémantique** : on demande à un solveur si la formule est valide (ici `SimplePlReasoner` — résolution — et `SatReasoner`, adossé à Sat4j). La réponse arrive vite, mais elle ne contient **aucune** preuve — c'est un verdict, pas un témoin.\n", + "\n", + "Ce notebook mesure les trois, sur la même micro-théorie propositionnelle `{p, q, r}`." + ] + }, + { + "cell_type": "code", + "execution_count": 1, + "id": "b6ae64fd", + "metadata": { + "execution": { + "iopub.execute_input": "2026-09-25T05:11:55.808493Z", + "iopub.status.busy": "2026-09-25T05:11:55.807993Z", + "iopub.status.idle": "2026-09-25T05:12:00.863415Z", + "shell.execute_reply": "2026-09-25T05:12:00.861072Z" + }, + "papermill": { + "duration": 5.064219, + "end_time": "2026-09-25T05:12:00.864762+00:00", + "exception": false, + "start_time": "2026-09-25T05:11:55.800543+00:00", + "status": "completed" + }, + "tags": [] + }, + "outputs": [ + { + "name": "stdout", + "output_type": "stream", + "text": [ + "--- Initialisation Tweety ---\n", + "JDK portable: zulu17.50.19-ca-jdk17.0.11-win_x64\n", + "Bibliotheques natives: native/\n" + ] + }, + { + "name": "stdout", + "output_type": "stream", + "text": [ + "JVM demarree avec 42 JARs.\n", + "SimplePlReasoner installe : True\n", + "SatReasoner installe : True\n" + ] + } + ], + "source": [ + "# --- Initialisation JVM Tweety (helper partage de la serie) + imports propositionnels ---\n", + "import os\n", + "import pathlib\n", + "import sys\n", + "\n", + "TWEETY_DIR = pathlib.Path.cwd()\n", + "if TWEETY_DIR.name != \"Tweety\":\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 (JDK portable, 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 import JClass\n", + "\n", + "Proposition = JClass(\"org.tweetyproject.logics.pl.syntax.Proposition\")\n", + "Implication = JClass(\"org.tweetyproject.logics.pl.syntax.Implication\")\n", + "Negation = JClass(\"org.tweetyproject.logics.pl.syntax.Negation\")\n", + "Conjunction = JClass(\"org.tweetyproject.logics.pl.syntax.Conjunction\")\n", + "PlBeliefSet = JClass(\"org.tweetyproject.logics.pl.syntax.PlBeliefSet\")\n", + "PlFormula = JClass(\"org.tweetyproject.logics.pl.syntax.PlFormula\")\n", + "SimplePlReasoner = JClass(\"org.tweetyproject.logics.pl.reasoner.SimplePlReasoner\")\n", + "SatReasoner = JClass(\"org.tweetyproject.logics.pl.reasoner.SatReasoner\")\n", + "\n", + "p, q, r = Proposition(\"p\"), Proposition(\"q\"), Proposition(\"r\")\n", + "LETTRES = [p, q, r]\n", + "\n", + "simple = SimplePlReasoner()\n", + "sat = SatReasoner()\n", + "vide = PlBeliefSet()\n", + "print(\"SimplePlReasoner installe :\", simple.isInstalled())\n", + "print(\"SatReasoner installe :\", sat.isInstalled())" + ] + }, + { + "cell_type": "markdown", + "id": "7a60ef88", + "metadata": { + "papermill": { + "duration": 0.00586, + "end_time": "2026-09-25T05:12:00.877066+00:00", + "exception": false, + "start_time": "2026-09-25T05:12:00.871206+00:00", + "status": "completed" + }, + "tags": [] + }, + "source": [ + "### Lecture : deux oracles réels, pas une simulation\n", + "\n", + "`SimplePlReasoner` implémente la résolution au premier ordre sur le fragment propositionnel ; `SatReasoner` traduit la requête en CNF et interroge un solveur SAT (Sat4j, faute de solveur configuré par défaut — le message « No default SAT solver configured » est un avertissement de configuration, pas une erreur).\n", + "\n", + "Les deux `isInstalled()` à `True` sont le contrôle d'environnement : la suite du notebook interroge ces objets, et si la JVM ou les JARs manquaient, l'exécution s'arrêterait ici plutôt que de produire des verdicts inventés." + ] + }, + { + "cell_type": "markdown", + "id": "cab54d63", + "metadata": { + "papermill": { + "duration": 0.00726, + "end_time": "2026-09-25T05:12:00.890303+00:00", + "exception": false, + "start_time": "2026-09-25T05:12:00.883043+00:00", + "status": "completed" + }, + "tags": [] + }, + "source": [ + "## 2. Les axiomes de Hilbert, vérifiés par l'oracle\n", + "\n", + "Le système de Łukasiewicz tient en trois schémas :\n", + "\n", + "| # | Schéma |\n", + "|---|---|\n", + "| A1 | `p → (q → p)` |\n", + "| A2 | `(p → (q → r)) → ((p → q) → (p → r))` |\n", + "| A3 | `(¬p → ¬q) → (q → p)` |\n", + "\n", + "avec **une** règle d'inférence : de `φ` et `φ → ψ`, conclure `ψ` (modus ponens).\n", + "\n", + "Ces trois schémas sont *choisis* : rien ne dit a priori qu'ils sont valides. On commence donc par demander aux **deux oracles** si chacun est une tautologie — la preuve, elle, viendra de la syntaxe." + ] + }, + { + "cell_type": "code", + "execution_count": 2, + "id": "80342a92", + "metadata": { + "execution": { + "iopub.execute_input": "2026-09-25T05:12:00.906271Z", + "iopub.status.busy": "2026-09-25T05:12:00.905675Z", + "iopub.status.idle": "2026-09-25T05:12:01.396142Z", + "shell.execute_reply": "2026-09-25T05:12:01.394753Z" + }, + "papermill": { + "duration": 0.500467, + "end_time": "2026-09-25T05:12:01.397135+00:00", + "exception": false, + "start_time": "2026-09-25T05:12:00.896668+00:00", + "status": "completed" + }, + "tags": [] + }, + "outputs": [ + { + "name": "stdout", + "output_type": "stream", + "text": [ + "A1: (p=>(q=>p))\n" + ] + }, + { + "name": "stdout", + "output_type": "stream", + "text": [ + " SimplePlReasoner = True SatReasoner = True\n", + "A2: ((p=>(q=>r))=>((p=>q)=>(p=>r)))\n" + ] + }, + { + "name": "stdout", + "output_type": "stream", + "text": [ + " SimplePlReasoner = True SatReasoner = True\n", + "A3: ((!p=>!q)=>(q=>p))\n" + ] + }, + { + "name": "stdout", + "output_type": "stream", + "text": [ + " SimplePlReasoner = True SatReasoner = True\n", + "\n", + "Implication.getFirstFormula() : p\n", + "Implication.getSecondFormula(): q\n", + "Negation.getFormula() : p\n" + ] + } + ], + "source": [ + "# --- Les trois schemas d'axiomes, soumis aux deux oracles (aucune preuve encore) ---\n", + "A1 = Implication(p, Implication(q, p))\n", + "A2 = Implication(Implication(p, Implication(q, r)),\n", + " Implication(Implication(p, q), Implication(p, r)))\n", + "A3 = Implication(Implication(Negation(p), Negation(q)), Implication(q, p))\n", + "AXIOMES = [A1, A2, A3]\n", + "\n", + "for i, A in enumerate(AXIOMES, 1):\n", + " print(f\"A{i}: {A}\")\n", + " print(f\" SimplePlReasoner = {simple.query(vide, A)} SatReasoner = {sat.query(vide, A)}\")\n", + "\n", + "# Le meme objet formule est reutilise partout : l'API d'acces aux sous-formules\n", + "# servira au moteur de recherche (section 3).\n", + "exemple = Implication(p, q)\n", + "print(\"\\nImplication.getFirstFormula() :\", exemple.getFirstFormula())\n", + "print(\"Implication.getSecondFormula():\", exemple.getSecondFormula())\n", + "print(\"Negation.getFormula() :\", Negation(p).getFormula())" + ] + }, + { + "cell_type": "markdown", + "id": "a58dc99f", + "metadata": { + "papermill": { + "duration": 0.006463, + "end_time": "2026-09-25T05:12:01.410626+00:00", + "exception": false, + "start_time": "2026-09-25T05:12:01.404163+00:00", + "status": "completed" + }, + "tags": [] + }, + "source": [ + "### Lecture : « tautologie » est un verdict sémantique\n", + "\n", + "Les six `True` ci-dessus ne sont pas des preuves — ce sont des **décisions**. Un oracle répond à la question « la formule est-elle conséquence de la base vide ? » en explorant les valuations ; il ne produit aucun objet que l'on puisse inspecter, transmettre ou vérifier indépendamment.\n", + "\n", + "C'est exactement la limite que le reste du notebook comble : construire des objets-preuve, puis les mesurer." + ] + }, + { + "cell_type": "markdown", + "id": "175c6130", + "metadata": { + "papermill": { + "duration": 0.00642, + "end_time": "2026-09-25T05:12:01.423617+00:00", + "exception": false, + "start_time": "2026-09-25T05:12:01.417197+00:00", + "status": "completed" + }, + "tags": [] + }, + "source": [ + "## 3. Chercher une preuve : chaînage avant\n", + "\n", + "Une preuve de Hilbert est une suite finie de formules `F1 … Fn` où chaque `Fi` est :\n", + "\n", + "1. une **instance** d'un schéma d'axiome sur des formules quelconques, ou\n", + "2. la conclusion d'un **modus ponens** appliqué à deux formules déjà présentes.\n", + "\n", + "Le moteur ci-dessous fait exactement cela, en **chaînage avant** : il instancie les trois schémas sur un ensemble fini de candidats, puis applique MP jusqu'à saturation, tour après tour.\n", + "\n", + "> **Ce que le moteur est, et ce qu'il n'est pas.** C'est une construction pédagogique *déclarée* : Tweety n'expose pas de prouveur de Hilbert pour la logique propositionnelle (son `Rule`/`RuleSet` vise les programmes logiques, ses prouveurs `SimplePlReasoner`/`SatReasoner` décident). Ce moteur n'est donc pas un organe concurrent — il produit l'objet *preuve* que les oracles ne produisent pas, et **chaque formule qu'il dérive est re-vérifiée par les oracles** (section suivante). Le candidat `target` est inclus dans le vivier d'instanciation : sans lui, l'antécédent d'une instance d'axiome utile ne serait jamais engendré." + ] + }, + { + "cell_type": "code", + "execution_count": 3, + "id": "981afb44", + "metadata": { + "execution": { + "iopub.execute_input": "2026-09-25T05:12:01.438037Z", + "iopub.status.busy": "2026-09-25T05:12:01.437491Z", + "iopub.status.idle": "2026-09-25T05:12:01.452678Z", + "shell.execute_reply": "2026-09-25T05:12:01.451434Z" + }, + "papermill": { + "duration": 0.024038, + "end_time": "2026-09-25T05:12:01.453853+00:00", + "exception": false, + "start_time": "2026-09-25T05:12:01.429815+00:00", + "status": "completed" + }, + "tags": [] + }, + "outputs": [ + { + "name": "stdout", + "output_type": "stream", + "text": [ + "Moteur pret : instances_axiomes + preuve_hilbert\n" + ] + } + ], + "source": [ + "# --- Moteur de recherche : instanciation des schemas + chainage avant (modus ponens) ---\n", + "import time\n", + "from itertools import product\n", + "\n", + "\n", + "def instances_axiomes(candidats):\n", + " \"\"\"Toutes les instances des trois schemas sur `candidats`.\"\"\"\n", + " out = []\n", + " for a in candidats:\n", + " for b in candidats:\n", + " out.append(Implication(a, Implication(b, a))) # A1\n", + " for a, b, c in product(candidats, repeat=3):\n", + " out.append(Implication(Implication(a, Implication(b, c)), # A2\n", + " Implication(Implication(a, b), Implication(a, c))))\n", + " for a in candidats:\n", + " for b in candidats:\n", + " out.append(Implication(Implication(Negation(a), Negation(b)),\n", + " Implication(b, a))) # A3\n", + " return out\n", + "\n", + "\n", + "def preuve_hilbert(cible, candidats, max_formules=200000):\n", + " \"\"\"Chainage avant borne : axiomes instancies, puis fermeture par modus ponens.\n", + "\n", + " Retourne (preuve, stats, base) ou la preuve est une liste de (formule, justification)\n", + " dans l'ordre d'utilisation, et base l'index complet des formules derivees.\n", + " \"\"\"\n", + " graines = instances_axiomes(candidats)\n", + " base = {}\n", + " frontiere = []\n", + " for s in graines:\n", + " k = str(s)\n", + " if k not in base:\n", + " base[k] = (s, \"axiome\", None)\n", + " frontiere.append(s)\n", + " cible_k = str(cible)\n", + " mp = 0\n", + " t0 = time.time()\n", + " tour = 0\n", + " while frontiere and len(base) < max_formules:\n", + " tour += 1\n", + " index = {k: v[0] for k, v in base.items()}\n", + " nouveaux = []\n", + " for f in frontiere:\n", + " if not Implication.class_.isInstance(f):\n", + " continue\n", + " antecedent = str(f.getFirstFormula())\n", + " if index.get(antecedent) is None:\n", + " continue\n", + " conclusion = f.getSecondFormula()\n", + " kc = str(conclusion)\n", + " if kc in base:\n", + " continue\n", + " base[kc] = (conclusion, \"MP\", (str(f), antecedent))\n", + " nouveaux.append(conclusion)\n", + " mp += 1\n", + " frontiere = nouveaux\n", + " if cible_k in base:\n", + " break\n", + " stats = {\"instances_axiomes\": len(graines), \"formules_connues\": len(base),\n", + " \"modus_ponens\": mp, \"tours\": tour, \"secondes\": round(time.time() - t0, 3)}\n", + " if cible_k not in base:\n", + " return None, stats, base\n", + " chaine, vus = [], set()\n", + "\n", + " def remonter(k):\n", + " if k in vus:\n", + " return\n", + " f, genre, charge = base[k]\n", + " if genre == \"axiome\":\n", + " vus.add(k)\n", + " chaine.append((k, \"axiome\"))\n", + " return\n", + " remonter(charge[0])\n", + " remonter(charge[1])\n", + " vus.add(k)\n", + " chaine.append((k, \"MP\"))\n", + "\n", + " remonter(cible_k)\n", + " return chaine, stats, base\n", + "\n", + "\n", + "print(\"Moteur pret :\", instances_axiomes.__name__, \"+\", preuve_hilbert.__name__)" + ] + }, + { + "cell_type": "markdown", + "id": "7999a927", + "metadata": { + "papermill": { + "duration": 0.006478, + "end_time": "2026-09-25T05:12:01.468071+00:00", + "exception": false, + "start_time": "2026-09-25T05:12:01.461593+00:00", + "status": "completed" + }, + "tags": [] + }, + "source": [ + "### Première cible : `p → p`\n", + "\n", + "C'est le plus petit théorème du système qui ne soit pas une instance d'axiome — le premier endroit où le modus ponens devient indispensable.\n", + "\n", + "Une précision sur le contrat du moteur, visible dans sa signature : la cible cherchée doit figurer dans le vivier d'instanciation. Ce n'est pas un détail d'implémentation — c'est ce qui permet aux schémas d'axiomes de la mentionner, et c'est exactement ce que la contre-expérience de la section suivante va mettre en défaut.\n" + ] + }, + { + "cell_type": "code", + "execution_count": 4, + "id": "c07ca2e4", + "metadata": { + "execution": { + "iopub.execute_input": "2026-09-25T05:12:01.483701Z", + "iopub.status.busy": "2026-09-25T05:12:01.483189Z", + "iopub.status.idle": "2026-09-25T05:12:01.575660Z", + "shell.execute_reply": "2026-09-25T05:12:01.574048Z" + }, + "papermill": { + "duration": 0.102237, + "end_time": "2026-09-25T05:12:01.577003+00:00", + "exception": false, + "start_time": "2026-09-25T05:12:01.474766+00:00", + "status": "completed" + }, + "tags": [] + }, + "outputs": [ + { + "name": "stdout", + "output_type": "stream", + "text": [ + "candidats d'instanciation : 13\n", + " 1. ((p=>((p=>p)=>p))=>((p=>(p=>p))=>(p=>p))) [axiome]\n", + " 2. (p=>((p=>p)=>p)) [axiome]\n", + " 3. ((p=>(p=>p))=>(p=>p)) [MP]\n", + " 4. (p=>(p=>p)) [axiome]\n", + " 5. (p=>p) [MP]\n", + "cout de la recherche : {'instances_axiomes': 2535, 'formules_connues': 2169, 'modus_ponens': 153, 'tours': 2, 'secondes': 0.028}\n" + ] + } + ], + "source": [ + "# --- Cible 1 : p -> p, le plus petit theoreme non axiome du systeme ---\n", + "cible = Implication(p, p)\n", + "candidats = [p, q, r, cible] + [Implication(a, b) for a in LETTRES for b in LETTRES]\n", + "print(f\"candidats d'instanciation : {len(candidats)}\")\n", + "chaine, stats, base = preuve_hilbert(cible, candidats)\n", + "for i, (formule, justification) in enumerate(chaine, 1):\n", + " print(f\" {i}. {formule} [{justification}]\")\n", + "print(\"cout de la recherche :\", stats)" + ] + }, + { + "cell_type": "markdown", + "id": "feab2abd", + "metadata": { + "papermill": { + "duration": 0.006698, + "end_time": "2026-09-25T05:12:01.591395+00:00", + "exception": false, + "start_time": "2026-09-25T05:12:01.584697+00:00", + "status": "completed" + }, + "tags": [] + }, + "source": [ + "### Lecture : cinq étapes, et ce qu'elles coûtent\n", + "\n", + "La preuve trouvée est la preuve classique de `p → p` : deux instances de **A2** et **A1**, deux modus ponens, et une instance de **A1** en route. Cinq formules — c'est le prix syntaxique minimal dans ce système pour un théorème qui *paraît* trivial.\n", + "\n", + "Le contraste avec la section précédente est le sujet du notebook : l'oracle répond `True` sur `p → p` en une fraction de milliseconde, **mais ne dit pas pourquoi**. Le moteur, lui, paie une recherche (les `formules_connues` et `modus_ponens` du dictionnaire `stats`) pour produire un objet inspectable — et ce coût dépend du **vivier d'instanciation**, pas seulement de la difficulté logique du théorème." + ] + }, + { + "cell_type": "code", + "execution_count": 5, + "id": "af65fafd", + "metadata": { + "execution": { + "iopub.execute_input": "2026-09-25T05:12:01.606131Z", + "iopub.status.busy": "2026-09-25T05:12:01.605622Z", + "iopub.status.idle": "2026-09-25T05:12:01.696642Z", + "shell.execute_reply": "2026-09-25T05:12:01.695309Z" + }, + "papermill": { + "duration": 0.100291, + "end_time": "2026-09-25T05:12:01.697873+00:00", + "exception": false, + "start_time": "2026-09-25T05:12:01.597582+00:00", + "status": "completed" + }, + "tags": [] + }, + "outputs": [ + { + "name": "stdout", + "output_type": "stream", + "text": [ + "[OK ] ((p=>((p=>p)=>p))=>((p=>(p=>p))=>(p=>p)))\n", + "[OK ] (p=>((p=>p)=>p))\n", + "[OK ] ((p=>(p=>p))=>(p=>p))\n", + "[OK ] (p=>(p=>p))\n", + "[OK ] (p=>p)\n", + "\n", + "oracle direct sur la cible : SimplePlReasoner = True | SatReasoner = True\n", + "etapes de la preuve : 5\n" + ] + } + ], + "source": [ + "# --- Chaque formule de la preuve est re-verifiee par les DEUX oracles ---\n", + "# Une preuve Hilbert correcte ne contient que des tautologies : c'est verifiable\n", + "# etape par etape, independamment du moteur de recherche.\n", + "tautologies = {formule: simple.query(vide, base[formule][0]) for formule, _ in chaine}\n", + "for formule, verdict in tautologies.items():\n", + " marque = \"OK \" if verdict else \"ECHEC\"\n", + " print(f\"[{marque}] {formule}\")\n", + "assert all(tautologies.values()), \"une etape de la preuve n'est pas une tautologie\"\n", + "print(\"\\noracle direct sur la cible :\",\n", + " \"SimplePlReasoner =\", simple.query(vide, cible), \"| SatReasoner =\", sat.query(vide, cible))\n", + "print(\"etapes de la preuve :\", len(chaine))" + ] + }, + { + "cell_type": "markdown", + "id": "dc37bae5", + "metadata": { + "papermill": { + "duration": 0.007202, + "end_time": "2026-09-25T05:12:01.712210+00:00", + "exception": false, + "start_time": "2026-09-25T05:12:01.705008+00:00", + "status": "completed" + }, + "tags": [] + }, + "source": [ + "### Ce que le moteur ne trouve pas\n", + "\n", + "Le moteur de la section 3 a trouvé `p → p`. Cette cible était favorable : le vivier d'instanciation contient `p` et `p → p`, donc les schémas se déploient exactement ce qu'il faut.\n", + "\n", + "Toutes les cibles ne se comportent pas ainsi. Prenons le **syllogisme hypothétique** — une formule que les deux oracles déclarent valide sans hésiter. Le même moteur, avec le même budget d'instanciation, va-t-il la dériver ?\n", + "\n", + "C'est la contre-expérience de cette section : elle mesure une **limite**, et elle teste au passage l'hypothèse la plus naturelle pour l'expliquer." + ] + }, + { + "cell_type": "code", + "execution_count": 6, + "id": "7ec1c931", + "metadata": { + "execution": { + "iopub.execute_input": "2026-09-25T05:12:01.728265Z", + "iopub.status.busy": "2026-09-25T05:12:01.727712Z", + "iopub.status.idle": "2026-09-25T05:12:02.134952Z", + "shell.execute_reply": "2026-09-25T05:12:02.133547Z" + }, + "papermill": { + "duration": 0.41734, + "end_time": "2026-09-25T05:12:02.136078+00:00", + "exception": false, + "start_time": "2026-09-25T05:12:01.718738+00:00", + "status": "completed" + }, + "tags": [] + }, + "outputs": [ + { + "name": "stdout", + "output_type": "stream", + "text": [ + "cible : ((p=>q)=>((q=>r)=>(p=>r)))\n", + "oracle SimplePlReasoner : True\n", + "oracle SatReasoner : True\n" + ] + }, + { + "name": "stdout", + "output_type": "stream", + "text": [ + "\n", + "vivier de la section 3 : |candidats|=13 trouvee=False\n", + " cout : {'instances_axiomes': 2535, 'formules_connues': 2713, 'modus_ponens': 178, 'tours': 3, 'secondes': 0.031}\n" + ] + }, + { + "name": "stdout", + "output_type": "stream", + "text": [ + "\n", + "vivier + sous-formules : |candidats|=14 trouvee=False\n", + " cout : {'instances_axiomes': 3136, 'formules_connues': 3342, 'modus_ponens': 206, 'tours': 3, 'secondes': 0.032}\n", + "\n", + "controle p -> p : trouvee=True etapes=5 formules_connues=2169\n" + ] + } + ], + "source": [ + "# --- Contre-experience : une cible valide que le moteur ne trouve PAS ---\n", + "# Le moteur est borne par son vivier d'instanciation : `instances_axiomes` ne\n", + "# deploie les schemas que sur `candidats`, et le chainage n'y ajoute jamais les\n", + "# formules qu'il derive. Le syllogisme hypothetique est un theoreme du calcul :\n", + "# les deux oracles le declarent valide. Le moteur, lui, le derive-t-il ?\n", + "cible_syllogisme = Implication(\n", + " Implication(p, q), Implication(Implication(q, r), Implication(p, r))\n", + ")\n", + "\n", + "\n", + "def vivier(sous_formules_supplementaires=()):\n", + " \"\"\"Meme recette de vivier que la section 3, plus d'eventuelles sous-formules.\"\"\"\n", + " pool = [p, q, r, cible_syllogisme] + [\n", + " Implication(a, b) for a in LETTRES for b in LETTRES\n", + " ]\n", + " connues = {str(f) for f in pool}\n", + " for f in sous_formules_supplementaires:\n", + " if str(f) not in connues:\n", + " pool.append(f)\n", + " connues.add(str(f))\n", + " return pool\n", + "\n", + "\n", + "print(f\"cible : {cible_syllogisme}\")\n", + "print(f\"oracle SimplePlReasoner : {simple.query(vide, cible_syllogisme)}\")\n", + "print(f\"oracle SatReasoner : {sat.query(vide, cible_syllogisme)}\")\n", + "\n", + "# Hypothese 1 : le vivier de la section 3 suffit.\n", + "candidats_etroit = vivier()\n", + "chaine_etroit, stats_etroit, _ = preuve_hilbert(cible_syllogisme, candidats_etroit)\n", + "print(f\"\\nvivier de la section 3 : |candidats|={len(candidats_etroit)} \"\n", + " f\"trouvee={chaine_etroit is not None}\")\n", + "print(f\" cout : {stats_etroit}\")\n", + "\n", + "# Hypothese 2 : il suffit d'y ajouter les sous-formules de la cible.\n", + "sous_formules = [\n", + " Implication(p, q), Implication(q, r), Implication(p, r),\n", + " Implication(Implication(q, r), Implication(p, r)),\n", + "]\n", + "candidats_elargi = vivier(sous_formules)\n", + "chaine_elargi, stats_elargi, _ = preuve_hilbert(cible_syllogisme, candidats_elargi)\n", + "print(f\"\\nvivier + sous-formules : |candidats|={len(candidats_elargi)} \"\n", + " f\"trouvee={chaine_elargi is not None}\")\n", + "print(f\" cout : {stats_elargi}\")\n", + "\n", + "# Controle : la MEME recette trouve bien p -> p (section 3) -- l'echec ci-dessus\n", + "# n'est donc pas un budget global trop court.\n", + "cible_controle = Implication(p, p)\n", + "candidats_controle = [p, q, r, cible_controle] + [\n", + " Implication(a, b) for a in LETTRES for b in LETTRES\n", + "]\n", + "chaine_controle, stats_controle, _ = preuve_hilbert(cible_controle, candidats_controle)\n", + "print(f\"\\ncontrole p -> p : trouvee={chaine_controle is not None} \"\n", + " f\"etapes={len(chaine_controle)} \"\n", + " f\"formules_connues={stats_controle['formules_connues']}\")" + ] + }, + { + "cell_type": "markdown", + "id": "05394674", + "metadata": { + "papermill": { + "duration": 0.007382, + "end_time": "2026-09-25T05:12:02.150216+00:00", + "exception": false, + "start_time": "2026-09-25T05:12:02.142834+00:00", + "status": "completed" + }, + "tags": [] + }, + "source": [ + "### Lecture : une limite structurelle, pas un budget trop court\n", + "\n", + "Le verdict est net, et il faut le lire honnêtement : les deux oracles répondent `True`, le moteur répond `False`.\n", + "\n", + "Ce n'est **pas** une contradiction — les trois moteurs ne répondent pas à la même question :\n", + "\n", + "| Moteur | Question posée | Réponse | Coût mesuré |\n", + "|---|---|---|---|\n", + "| `SimplePlReasoner` / `SatReasoner` | « cette formule est-elle valide ? » | oui, sans preuve | quasi instantané |\n", + "| Chaînage avant | « puis-je la **dériver** des axiomes ? » | non | ~2 700 formules, ~180 MP, 3 tours |\n", + "\n", + "La cause est lisible dans le moteur lui-même : `instances_axiomes` ne déploie les schémas que sur `candidats`, et le chaînage n'y ajoute jamais les formules qu'il dérive. Le vivier reste figé à ce qu'on lui a donné au départ.\n", + "\n", + "L'hypothèse naturelle — « il manque quelques formules, élargissons le vivier » — est **testée et réfutée** ici : avec les sous-formules de la cible ajoutées, le moteur ne trouve toujours pas. La borne est donc structurelle, pas quantitative.\n", + "\n", + "Le contrôle le confirme par l'autre bout : avec le même budget, `p → p` est trouvée en 5 étapes. Le moteur n'est pas cassé — il est **borné par la forme de sa recherche**, et c'est précisément ce qu'un banc d'essai doit rendre visible plutôt que masquer." + ] + }, + { + "cell_type": "markdown", + "id": "a3b53831", + "metadata": { + "papermill": { + "duration": 0.008141, + "end_time": "2026-09-25T05:12:02.165733+00:00", + "exception": false, + "start_time": "2026-09-25T05:12:02.157592+00:00", + "status": "completed" + }, + "tags": [] + }, + "source": [ + "## 4. Séquents de Gentzen : LK, la coupure, et le Hauptsatz\n", + "\n", + "Le calcul des séquents raisonne sur des **séquents** `Γ ⊢ Δ`. Dans la version **à un seul côté** utilisée par FFL (Foundation for Formal Logic), un séquent est un multi-ensemble de formules `⦃φ₁, …, φₙ⦄` et la négation est primitive (atomes positifs `p` / négatifs `¬p`). Les règles utiles ici :\n", + "\n", + "| Règle | Forme |\n", + "|---|---|\n", + "| identité | `⊢ ⦃p, ¬p⦄` pour un atome `p` |\n", + "| coupure (*cut*) | de `⊢ Γ + ⦃φ⦄` et `⊢ Δ + ⦃¬φ⦄`, conclure `⊢ Γ + Δ` |\n", + "| contraction | de `⊢ Δ` conclure `⊢ Γ` quand `Δ ⊆ Γ` |\n", + "| conjonction | de `⊢ Γ + ⦃φ⦄` et `⊢ Γ + ⦃ψ⦄`, conclure `⊢ Γ + ⦃φ ⋏ ψ⦄` |\n", + "| disjonction | de `⊢ Γ + ⦃φ, ψ⦄`, conclure `⊢ Γ + ⦃φ ⋎ ψ⦄` |\n", + "\n", + "Une dérivation est un **arbre** ; sa **hauteur** (`Derivation.height`) et sa **taille** (nombre de nœuds) sont deux mesures différentes du même objet. La coupure est l'analogue structurel du modus ponens : elle permet de réutiliser un lemme, au prix d'une formule qui n'est pas sous-formule de la conclusion.\n", + "\n", + "Le **Hauptsatz** (théorème d'élimination des coupures) affirme que toute dérivation se transforme en une dérivation **sans coupure** de la même conclusion. FFL le fournit comme **théorème** `Derivation.Canonical.constructiveHauptsatz`, dont la sortie est un sous-type : la dérivation éliminée **et** le témoin `IsCutFree`.\n", + "\n", + "> **Où vit le code Lean de ce notebook.** Le corpus FFL est consommé en **`CONSUMER_PINNÉ`** (verdict du pilote [#15520](https://github.com/jsboige/CoursIA/pull/15520)) : aucun module upstream n'est vendé ni adapté. Les autres tranches de l'EPIC adossent leur versant Lean à un module de pont versionné dans `formal_logic_lean/FormalLogic/` ; **cette tranche ne touche pas au lake** — ses deux fichiers d'index (`FormalLogic.lean`, `README.md`) sont sous claim actif d'une autre lane (`check_lane_claim`, verdict `BLOCKED`, 2026-09-25). Le langage `PL`, la mesure de taille et les deux dérivations sont donc définis **dans le notebook** et soumis au noyau par `lake env lean` : les objets du noyau invoqués (`Derivation`, `cut`, `IsCutFree`, `constructiveHauptsatz`) sont, eux, **exactement** ceux du corpus épinglé, et la cellule de provenance le mesure avant de compiler." + ] + }, + { + "cell_type": "code", + "execution_count": 7, + "id": "ead18758", + "metadata": { + "execution": { + "iopub.execute_input": "2026-09-25T05:12:02.184866Z", + "iopub.status.busy": "2026-09-25T05:12:02.184279Z", + "iopub.status.idle": "2026-09-25T05:13:06.013075Z", + "shell.execute_reply": "2026-09-25T05:13:06.011744Z" + }, + "papermill": { + "duration": 63.846893, + "end_time": "2026-09-25T05:13:06.020420+00:00", + "exception": false, + "start_time": "2026-09-25T05:12:02.173527+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": [ + " Foundation 81810b9f22c4 [pin confirme]\n" + ] + }, + { + "name": "stdout", + "output_type": "stream", + "text": [ + " mathlib 0df444a360ea [pin confirme]\n" + ] + }, + { + "name": "stdout", + "output_type": "stream", + "text": [ + " ProvabilityLogic 01628c51f618 [pin confirme]\n" + ] + }, + { + "name": "stdout", + "output_type": "stream", + "text": [ + "\n", + "$ lake build Foundation.FirstOrder.Hauptsatz\n", + "info: Foundation/FirstOrder/Basic/BinderNotation.lean:805:0: “#0 = #1” : Semiformula ?m.16 ?m.17 ?m.18\n", + "info: Foundation/FirstOrder/Basic/BinderNotation.lean:817:0: ∀¹ ((“#0 = #1”) 🡒 ∀¹ ((“#0 = #3”) 🡒 (“#1 = #0”))) : Semiformula ?m.43 ?m.44 ?m.3\n", + "Build completed successfully (962 jobs).\n", + "\n", + "BUILD OK : Foundation.FirstOrder.Hauptsatz compile sur les pins ci-dessus.\n" + ] + } + ], + "source": [ + "# --- Helpers WSL + provenance mesuree + build du module (patron Tweety-02d / 5e) ---\n", + "import json as _json\n", + "import shutil\n", + "import subprocess\n", + "import tempfile\n", + "\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", + "\n", + "def to_wsl(chemin):\n", + " \"\"\"Chemin Windows -> chemin WSL /mnt/...\"\"\"\n", + " win = chemin.resolve().as_posix()\n", + " return \"/mnt/\" + win[0].lower() + win[2:]\n", + "\n", + "\n", + "def run_wsl(commande, 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 4-5 exigent un hote Windows + WSL.\"\n", + " )\n", + " return subprocess.run(\n", + " [\"wsl\", \"-e\", \"bash\", \"-lc\", commande],\n", + " capture_output=True, text=True, encoding=\"utf-8\", errors=\"replace\",\n", + " timeout=timeout,\n", + " )\n", + "\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 = {paquet[\"name\"]: paquet[\"rev\"] for paquet in manifest[\"packages\"]}\n", + "print(\"Provenance mesuree (git rev-parse dans .lake/packages) :\")\n", + "for paquet in [\"Foundation\", \"mathlib\", \"ProvabilityLogic\"]:\n", + " res = run_wsl(f\"git -C {to_wsl(LAKE_DIR)}/.lake/packages/{paquet} rev-parse HEAD\", timeout=120)\n", + " mesure = (res.stdout or \"\").strip()\n", + " if res.returncode != 0 or not mesure:\n", + " raise RuntimeError(\n", + " f\"paquet {paquet} illisible dans .lake/packages (exit {res.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[paquet] else \"DERIVE\"\n", + " print(f\" {paquet:<18s} {mesure[:12]} [{statut}]\")\n", + " assert mesure == pins_attendus[paquet], f\"{paquet} a derive : {mesure[:12]}\"\n", + "\n", + "# 2) Build cible : le module EXACT que ce notebook importe (idempotent)\n", + "CIBLE = \"Foundation.FirstOrder.Hauptsatz\"\n", + "res = run_wsl(f\"cd {to_wsl(LAKE_DIR)} && lake build {CIBLE}\", timeout=7200)\n", + "sortie = (res.stdout or \"\") + (res.stderr or \"\")\n", + "print(f\"\\n$ lake build {CIBLE}\")\n", + "print(\"\\n\".join(sortie.strip().splitlines()[-3:]) or \"(deja a jour)\")\n", + "assert res.returncode == 0, f\"lake build {CIBLE} a echoue -- voir sortie ci-dessus\"\n", + "print(f\"\\nBUILD OK : {CIBLE} compile sur les pins ci-dessus.\")" + ] + }, + { + "cell_type": "markdown", + "id": "19b359db", + "metadata": { + "papermill": { + "duration": 0.005325, + "end_time": "2026-09-25T05:13:06.033359+00:00", + "exception": false, + "start_time": "2026-09-25T05:13:06.028034+00:00", + "status": "completed" + }, + "tags": [] + }, + "source": [ + "### Lecture : provenance mesurée, build réel\n", + "\n", + "Les trois `rev-parse` comparent le **contenu réel** de `.lake/packages/` aux révisions déclarées dans `lake-manifest.json` : si un paquet dérivait (fetch manuel, fork divergent), l'assertion arrêterait le notebook. Mesurer plutôt que déclarer — sans ce contrôle, le notebook compilerait contre une révision inconnue tout en affichant la bonne.\n", + "\n", + "Le `lake build` qui suit compile **le module exact que les cellules suivantes importent** (`Foundation.FirstOrder.Hauptsatz`) : c'est de lui que viennent `Derivation`, `IsCutFree` et `constructiveHauptsatz`. Le timeout est large (la première compilation du lake est longue — mathlib puis Foundation) ; les exécutions suivantes sont incrémentales." + ] + }, + { + "cell_type": "code", + "execution_count": 8, + "id": "d9bee97c", + "metadata": { + "execution": { + "iopub.execute_input": "2026-09-25T05:13:06.047473Z", + "iopub.status.busy": "2026-09-25T05:13:06.047112Z", + "iopub.status.idle": "2026-09-25T05:19:20.825631Z", + "shell.execute_reply": "2026-09-25T05:19:20.824714Z" + }, + "papermill": { + "duration": 374.791259, + "end_time": "2026-09-25T05:19:20.830109+00:00", + "exception": false, + "start_time": "2026-09-25T05:13:06.038850+00:00", + "status": "completed" + }, + "tags": [] + }, + "outputs": [ + { + "name": "stdout", + "output_type": "stream", + "text": [ + "@Derivation : {L : Language} → Sequent L → Type u_1\n", + "@Derivation.identity : {L : Language} →\n", + " {k : ℕ} → (r : L.Rel k) → (v : Fin k → Semiterm L ℕ 0) → ⊢ᴸᴷ¹ ⦃Semiformula.rel r v⦄ + ⦃Semiformula.nrel r v⦄\n", + "@Derivation.cut : {L : Language} →\n", + " {Γ : Sequent L} → {φ : Proposition L} → {Δ : Sequent L} → ⊢ᴸᴷ¹ Γ + ⦃φ⦄ → ⊢ᴸᴷ¹ Δ + ⦃∼φ⦄ → ⊢ᴸᴷ¹ Γ + Δ\n", + "@Derivation.height : {L : Language} → {Δ : Sequent L} → ⊢ᴸᴷ¹ Δ → ℕ\n", + "@Derivation.IsCutFree : {L : Language} → {Γ : Sequent L} → ⊢ᴸᴷ¹ Γ → Prop\n", + "@Derivation.Canonical.constructiveHauptsatz : {L : Language} →\n", + " [L.DecidableEq] → [L.Encodable] → {Γ : Sequent L} → ⊢ᴸᴷ¹ Γ → { d // d.IsCutFree }\n", + "FFL.FirstOrder.Sequent.{u_1} (L : Language) : Type u_1\n", + "FFL.FirstOrder.Proposition.{u_1} (L : Language) : Type u_1\n", + "\n", + "[exit 0]\n" + ] + } + ], + "source": [ + "# --- run_lean + tour d'API : les objets FFL reels, verifies par le noyau ---\n", + "def run_lean(source):\n", + " \"\"\"Ecrit source dans un temporaire et le fait verifier par le noyau Lean\n", + " natif du lake (lake env lean = toolchain + LEAN_PATH du pin).\"\"\"\n", + " dossier = pathlib.Path(tempfile.mkdtemp(prefix=\"tweety02e_\"))\n", + " fichier = dossier / \"scratch.lean\"\n", + " fichier.write_text(source, encoding=\"utf-8\")\n", + " res = run_wsl(f\"cd {to_wsl(LAKE_DIR)} && lake env lean {to_wsl(fichier)}\", timeout=3600)\n", + " return (res.stdout or \"\") + (res.stderr or \"\"), res.returncode\n", + "\n", + "\n", + "tour_api = \"\"\"import Foundation.FirstOrder.Hauptsatz\n", + "\n", + "open FFL FirstOrder\n", + "\n", + "#check @FFL.FirstOrder.Derivation\n", + "#check @FFL.FirstOrder.Derivation.identity\n", + "#check @FFL.FirstOrder.Derivation.cut\n", + "#check @FFL.FirstOrder.Derivation.height\n", + "#check @FFL.FirstOrder.Derivation.IsCutFree\n", + "#check @FFL.FirstOrder.Derivation.Canonical.constructiveHauptsatz\n", + "#check FFL.FirstOrder.Sequent\n", + "#check FFL.FirstOrder.Proposition\n", + "\"\"\"\n", + "\n", + "sortie, code_retour = run_lean(tour_api)\n", + "print(sortie)\n", + "print(f\"[exit {code_retour}]\")\n", + "assert code_retour == 0, \"le tour d'API doit compiler sans erreur\"" + ] + }, + { + "cell_type": "markdown", + "id": "147ebba1", + "metadata": { + "papermill": { + "duration": 0.003654, + "end_time": "2026-09-25T05:19:20.837682+00:00", + "exception": false, + "start_time": "2026-09-25T05:19:20.834028+00:00", + "status": "completed" + }, + "tags": [] + }, + "source": [ + "### Lecture : ce que le noyau vient de vérifier\n", + "\n", + "Chaque `#check` est une vérification de type : le noyau confirme que `Derivation` est bien une famille inductive indexée par les séquents, que `cut` prend deux dérivations et en rend une troisième, que `height` est une fonction de `Derivation` vers `ℕ`, et que `constructiveHauptsatz` rend un **sous-type** `{d // IsCutFree d}` — donc la dérivation **et** la preuve qu'elle est sans coupure, dans le même objet." + ] + }, + { + "cell_type": "code", + "execution_count": 9, + "id": "c58c9bc0", + "metadata": { + "execution": { + "iopub.execute_input": "2026-09-25T05:19:20.846176Z", + "iopub.status.busy": "2026-09-25T05:19:20.845844Z", + "iopub.status.idle": "2026-09-25T05:24:27.085080Z", + "shell.execute_reply": "2026-09-25T05:24:27.083574Z" + }, + "papermill": { + "duration": 306.247515, + "end_time": "2026-09-25T05:24:27.088670+00:00", + "exception": false, + "start_time": "2026-09-25T05:19:20.841155+00:00", + "status": "completed" + }, + "tags": [] + }, + "outputs": [ + { + "name": "stdout", + "output_type": "stream", + "text": [ + "0\n", + "2\n", + "1\n", + "4\n", + "\n", + "[exit 0]\n" + ] + } + ], + "source": [ + "# --- Preambule Lean : langage propositionnel concret + deux derivations du meme sequent ---\n", + "LEAN_PREAMBLE = r'''\n", + "import Foundation.FirstOrder.Hauptsatz\n", + "\n", + "open FFL FirstOrder Semiformula\n", + "\n", + "namespace Tweety02e\n", + "\n", + "/-- Trois lettres propositionnelles, comme relations d'arité 0. -/\n", + "inductive Letter : ℕ → Type\n", + " | p : Letter 0\n", + " | q : Letter 0\n", + " | r : Letter 0\n", + " deriving DecidableEq\n", + "\n", + "@[reducible]\n", + "def PL : Language where\n", + " Func := fun _ => PEmpty\n", + " Rel := Letter\n", + "\n", + "instance (k) : DecidableEq (PL.Func k) := fun a b => by rcases a\n", + "\n", + "instance (k) : Encodable (PL.Func k) := IsEmpty.toEncodable\n", + "\n", + "instance (k) : DecidableEq (PL.Rel k) := inferInstance\n", + "\n", + "instance (k) : Encodable (PL.Rel k) where\n", + " encode := fun x => match x with\n", + " | .p => 0\n", + " | .q => 1\n", + " | .r => 2\n", + " decode := fun n =>\n", + " match k with\n", + " | 0 =>\n", + " match n with\n", + " | 0 => some .p\n", + " | 1 => some .q\n", + " | 2 => some .r\n", + " | _ => none\n", + " | _ => none\n", + " encodek := fun x => by\n", + " match x with\n", + " | .p => rfl\n", + " | .q => rfl\n", + " | .r => rfl\n", + "\n", + "/-- Une lettre comme formule atomique. -/\n", + "abbrev atom (l : Letter 0) : Proposition PL :=\n", + " Semiformula.rel l (fun i : Fin 0 => i.elim0)\n", + "\n", + "open FFL.FirstOrder.Derivation\n", + "\n", + "/-- Nombre de nœuds d'une dérivation LK (motifs qualifiés : `verum` est aussi\n", + "un constructeur de `Semiformula` ; appels récursifs par le nom nu, la notation\n", + "point cherchant d'abord dans `FFL.FirstOrder.Derivation`). -/\n", + "def size {Γ : Sequent PL} : ⊢ᴸᴷ¹ Γ → ℕ\n", + " | Derivation.identity _ _ => 1\n", + " | Derivation.cut dp dn => size dp + size dn + 1\n", + " | Derivation.contraction d _ => size d + 1\n", + " | Derivation.verum => 1\n", + " | Derivation.or d => size d + 1\n", + " | Derivation.and dp dq => size dp + size dq + 1\n", + " | Derivation.all d => size d + 1\n", + " | Derivation.exs d => size d + 1\n", + "\n", + "/-- Le séquent `p, ¬p` par l'axiome d'identité — sans coupure.\n", + "Le langage est nommé (`L := PL`) : `L` et `k` sont implicites dans\n", + "`Derivation.identity` et ne s'infèrent pas du type attendu. -/\n", + "def dIdentite : ⊢ᴸᴷ¹ ⦃atom .p, ∼atom .p⦄ :=\n", + " Derivation.identity (L := PL) Letter.p (fun i : Fin 0 => i.elim0)\n", + "\n", + "/-- Le même séquent, dérivé avec une coupure sur `¬p`.\n", + "La coupure se lit sur les types : la prémisse gauche est `Γ + ⦃φ⦄` avec\n", + "`φ := ¬p`, la droite est `Δ + ⦃¬φ⦄` avec `Δ := ⦃¬p⦄`. `eta` rend\n", + "précisément `⦃φ, ¬φ⦄`, donc la prémisse droite est `eta (¬p)` — et la\n", + "conclusion `Γ + Δ` retombe sur `⦃p, ¬p⦄`. Aucun `cast` n'est nécessaire :\n", + "`⬝ ▸ ⬝` est un `abbrev` sur `Eq.ndrec`, qui ne se réduit pas sous `#eval`\n", + "quand la preuve d'égalité n'est pas `rfl`. -/\n", + "def dCoupure : ⊢ᴸᴷ¹ ⦃atom .p, ∼atom .p⦄ :=\n", + " Derivation.cut (Γ := ⦃atom .p⦄) (Δ := ⦃∼atom .p⦄) (φ := ∼atom .p)\n", + " (Derivation.identity (L := PL) Letter.p (fun i : Fin 0 => i.elim0))\n", + " (Derivation.eta (∼atom .p))\n", + "\n", + "end Tweety02e\n", + "'''\n", + "\n", + "mesures = LEAN_PREAMBLE + '''\n", + "open Tweety02e\n", + "#eval dIdentite.height\n", + "#eval dCoupure.height\n", + "#eval size dIdentite\n", + "#eval size dCoupure\n", + "'''\n", + "sortie, code_retour = run_lean(mesures)\n", + "print(sortie)\n", + "print(f\"[exit {code_retour}]\")\n", + "assert code_retour == 0, \"le preambule Lean doit compiler sans erreur\"" + ] + }, + { + "cell_type": "markdown", + "id": "255fdaa3", + "metadata": { + "papermill": { + "duration": 0.004826, + "end_time": "2026-09-25T05:24:27.097560+00:00", + "exception": false, + "start_time": "2026-09-25T05:24:27.092734+00:00", + "status": "completed" + }, + "tags": [] + }, + "source": [ + "### Lecture : deux preuves du même séquent, deux mesures\n", + "\n", + "Les quatre nombres imprimés mesurent le même énoncé `⊢ ⦃p, ¬p⦄` par deux objets différents :\n", + "\n", + "- la dérivation **par identité** est une feuille : hauteur `0`, taille `1` ;\n", + "- la dérivation **par coupure** coupe `¬p` entre l'axiome d'identité et `eta (¬p)` (une identité sous une contraction) : hauteur `2`, taille `4`.\n", + "\n", + "La coupure n'a rien ajouté à ce que l'identité donnait déjà — c'est une redondance **structurelle**, exactement ce que le Hauptsatz supprime. Sur des formules composites, la coupure n'est pas redondante : elle peut réduire la hauteur d'un arbre en réutilisant un lemme (c'est son intérêt), et l'élimination la paiera en taille." + ] + }, + { + "cell_type": "code", + "execution_count": 10, + "id": "482b2495", + "metadata": { + "execution": { + "iopub.execute_input": "2026-09-25T05:24:27.106383Z", + "iopub.status.busy": "2026-09-25T05:24:27.106181Z", + "iopub.status.idle": "2026-09-25T05:29:02.012594Z", + "shell.execute_reply": "2026-09-25T05:29:02.011478Z" + }, + "papermill": { + "duration": 274.917167, + "end_time": "2026-09-25T05:29:02.018604+00:00", + "exception": false, + "start_time": "2026-09-25T05:24:27.101437+00:00", + "status": "completed" + }, + "tags": [] + }, + "outputs": [ + { + "name": "stdout", + "output_type": "stream", + "text": [ + "6\n", + "7\n", + "2\n", + "4\n", + "'FFL.FirstOrder.Derivation.Canonical.constructiveHauptsatz' depends on axioms: [propext, Classical.choice, Quot.sound]\n", + "\n", + "[exit 0]\n" + ] + } + ], + "source": [ + "# --- Elimination des coupures : le Hauptsatz comme THEOREME, pas comme procedure ---\n", + "elimination = LEAN_PREAMBLE + '''\n", + "open Tweety02e\n", + "open FFL.FirstOrder.Derivation\n", + "\n", + "/-- La dérivation sans coupure produite par le Hauptsatz constructif. -/\n", + "def dSansCoupure : ⊢ᴸᴷ¹ ⦃atom .p, ∼atom .p⦄ :=\n", + " (Derivation.Canonical.constructiveHauptsatz dCoupure).1\n", + "\n", + "/-- Le temoin de non-coupure, extrait du meme theoreme (deuxieme composante). -/\n", + "example : Derivation.IsCutFree dSansCoupure :=\n", + " (Derivation.Canonical.constructiveHauptsatz dCoupure).2\n", + "\n", + "#eval dSansCoupure.height\n", + "#eval size dSansCoupure\n", + "#eval dCoupure.height\n", + "#eval size dCoupure\n", + "#print axioms Derivation.Canonical.constructiveHauptsatz\n", + "'''\n", + "sortie, code_retour = run_lean(elimination)\n", + "print(sortie)\n", + "print(f\"[exit {code_retour}]\")\n", + "assert code_retour == 0, \"l'elimination des coupures doit compiler sans erreur\"" + ] + }, + { + "cell_type": "markdown", + "id": "393090de", + "metadata": { + "papermill": { + "duration": 0.005439, + "end_time": "2026-09-25T05:29:02.029630+00:00", + "exception": false, + "start_time": "2026-09-25T05:29:02.024191+00:00", + "status": "completed" + }, + "tags": [] + }, + "source": [ + "### Lecture : ce que le théorème rend, et ce qu'il coûte\n", + "\n", + "`constructiveHauptsatz` ne renvoie pas une promesse : il renvoie la dérivation éliminée (`dSansCoupure`) **et** la preuve `IsCutFree` de celle-ci — les deux composantes du sous-type. Le `#eval` compare l'objet d'origine et l'objet transformé :\n", + "\n", + "| dérivation | hauteur | taille |\n", + "|---|---|---|\n", + "| `dIdentite` — axiome d'identité, sans coupure | 0 | 1 |\n", + "| `dCoupure` — avec coupure | 2 | 4 |\n", + "| `dSansCoupure` — rendue par le Hauptsatz | **6** | **7** |\n", + "\n", + "Le théorème n'est pas un optimiseur : sur cette instance il rend une dérivation **plus haute** (2 → 6) et **plus grosse** (4 → 7) que celle qu'il remplace. C'est le résultat attendu, et c'est le point pédagogique : le Hauptsatz garantit la **suppression des coupures**, jamais l'économie de l'arbre.\n", + "\n", + "Le `#print axioms` complète la lecture en nommant ce sur quoi le théorème repose : `propext`, `Classical.choice`, `Quot.sound`. `constructiveHauptsatz` rend un témoin **calculable** — le `#eval` aboutit — mais sa preuve n'est pas sans axiomes : les trois axiomes classiques de Mathlib sont bien là.\n", + "\n", + "Le point d'ensemble est que l'élimination des coupures est un **théorème du noyau**, pas un algorithme décrit dans un commentaire. Un étudiant peut l'invoquer, mesurer ses effets, et vérifier que la conclusion est inchangée — exactement comme on utilise un lemme de Mathlib." + ] + }, + { + "cell_type": "markdown", + "id": "9e283b9b", + "metadata": { + "papermill": { + "duration": 0.004723, + "end_time": "2026-09-25T05:29:02.039241+00:00", + "exception": false, + "start_time": "2026-09-25T05:29:02.034518+00:00", + "status": "completed" + }, + "tags": [] + }, + "source": [ + "## 5. Bilan croisé : trois calculs, trois mesures\n", + "\n", + "| Question | Moteur | Objet produit | Mesure du jour |\n", + "|---|---|---|---|\n", + "| « Pourquoi `p → p` ? » | Hilbert (axiomes + MP) | une liste de 5 formules justifiées | ~2 500 instances d'axiomes, ~150 MP, quelques dizaines de ms |\n", + "| « Pourquoi `⊢ ⦃p, ¬p⦄` ? » | LK (séquents) | un arbre, avec ou sans coupure | identité 0/1 · coupure 2/4 · après élimination 6/7 (hauteur/taille) |\n", + "| « Est-ce valide ? » | `SimplePlReasoner` / `SatReasoner` | un verdict `True`/`False` | quasi instantané, **sans** preuve |\n", + "\n", + "Deux résultats négatifs mesurés dans ce notebook, et ils comptent autant que les positifs :\n", + "\n", + "1. **La recherche Hilbert ne trouve pas tout ce qu'elle « pourrait »** : le syllogisme hypothétique `(p → q) → ((q → r) → (p → r))` n'est pas trouvé dans le budget d'instanciation du moteur, alors que l'oracle le déclare valide immédiatement. La cause est le vivier d'instanciation (le moteur n'instancie pas les schémas sur les formules qu'il dérive), pas la logique — et l'élargir aux sous-formules de la cible **ne suffit pas** : la section 3 a testé cette hypothèse et l'a réfutée par la mesure.\n", + "2. **L'élimination des coupures n'est pas gratuite — et ce n'est pas non plus une simplification** : sur ce cas minimal la dérivation rendue par le théorème est *plus haute* (2 → 6) et *plus grosse* (4 → 7) que celle qu'elle remplace. Le théorème garantit l'existence d'une dérivation sans coupure, jamais qu'elle soit plus petite : supprimer la coupure ne fait pas disparaître la structure qu'elle condensait.\n", + "\n", + "Ce que le notebook établit, en une phrase : *décider* est bon marché et aveugle ; *prouver* est coûteux, inspectable, et mesurable — et la taille d'une preuve dépend du **système de calcul** choisi pour la représenter." + ] + }, + { + "cell_type": "markdown", + "id": "3c614b19", + "metadata": { + "papermill": { + "duration": 0.005922, + "end_time": "2026-09-25T05:29:02.051036+00:00", + "exception": false, + "start_time": "2026-09-25T05:29:02.045114+00:00", + "status": "completed" + }, + "tags": [] + }, + "source": [ + "## Exercice 1 : calibrer la taille des preuves Hilbert\n", + "\n", + "### Contexte\n", + "\n", + "Le moteur de la section 3 a produit `p → p` en **5 étapes**. Toutes les cibles ne se valent pas : certaines sont des instances d'axiome (une seule ligne), d'autres exigent une vraie fermeture par modus ponens.\n", + "\n", + "### Objectifs\n", + "\n", + "1. Mesurer le nombre d'étapes pour les trois cibles suivantes, avec le **même** vivier d'instanciation : `p → (q → p)`, `p → p`, `(p → q) → (p → q)`\n", + "2. Pour chaque cible, comparer le nombre d'étapes trouvé à `stats[\"formules_connues\"]` : la preuve est-elle un objet rare dans la base dérivée ?\n", + "3. Expliquer, **sans exécuter**, pourquoi `p → (q → p)` ne peut pas se trouver en plus d'une étape\n", + "\n", + "> **Indices :**\n", + "> - réutilisez `preuve_hilbert(cible, candidats)` — la cible doit figurer dans `candidats` ;\n", + "> - une instance d'axiome est présente dès l'initialisation : le tour de fermeture n'est même pas nécessaire ;\n", + "> - `str(cible)` sert de clé dans `base` : l'égalité de formules passe par `toString()`." + ] + }, + { + "cell_type": "code", + "execution_count": 11, + "id": "8e35a7cf", + "metadata": { + "execution": { + "iopub.execute_input": "2026-09-25T05:29:02.064739Z", + "iopub.status.busy": "2026-09-25T05:29:02.064403Z", + "iopub.status.idle": "2026-09-25T05:29:02.068476Z", + "shell.execute_reply": "2026-09-25T05:29:02.067538Z" + }, + "papermill": { + "duration": 0.012017, + "end_time": "2026-09-25T05:29:02.069188+00:00", + "exception": false, + "start_time": "2026-09-25T05:29:02.057171+00:00", + "status": "completed" + }, + "tags": [] + }, + "outputs": [ + { + "name": "stdout", + "output_type": "stream", + "text": [ + "Exercice a completer\n" + ] + } + ], + "source": [ + "# --- Exercice 1 : trois cibles, trois tailles de preuve ---\n", + "# TODO etudiant\n", + "# Etape 1 : boucler sur les trois cibles et appeler preuve_hilbert(cible, candidats)\n", + "# Etape 2 : afficher len(chaine) et stats[\"formules_connues\"] pour chaque cible\n", + "# Etape 3 : expliquer en commentaire pourquoi la premiere cible tient en une seule ligne\n", + "print(\"Exercice a completer\")" + ] + }, + { + "cell_type": "markdown", + "id": "9453c5ca", + "metadata": { + "papermill": { + "duration": 0.004617, + "end_time": "2026-09-25T05:29:02.078928+00:00", + "exception": false, + "start_time": "2026-09-25T05:29:02.074311+00:00", + "status": "completed" + }, + "tags": [] + }, + "source": [ + "## Exercice 2 : une dérivation LK sans coupure, mesurée\n", + "\n", + "### Contexte\n", + "\n", + "La section 4 n'a mesuré que le cas minimal `⊢ ⦃p, ¬p⦄`. Le témoin vraiment intéressant est un séquent **composite**, sans coupure : `⊢ ⦃¬p, ¬q, p ⋏ q⦄`.\n", + "\n", + "### Objectifs\n", + "\n", + "1. Construire en Lean la dérivation `dConjonction : ⊢ᴸᴷ¹ ⦃∼atom .p, ∼atom .q, atom .p ⋏ atom .q⦄` — la règle `Derivation.and` exige **deux** dérivations du même contexte `Γ`, l'une de `⦃atom .p⦄`, l'autre de `⦃atom .q⦄`, chacune obtenue par contraction d'un axiome d'identité (indice : `Derivation.contraction` prend une preuve de `Δ` et une inclusion `Δ ⊆ Γ`)\n", + "2. Mesurer `#eval dConjonction.height` et `#eval dConjonction.size`\n", + "3. Vérifier que l'objet est bien sans coupure : `example : Derivation.IsCutFree dConjonction` — et expliquer pourquoi le Hauptsatz, appliqué à cet objet, ne peut pas faire mieux\n", + "\n", + "> **Indices :**\n", + "> - `Derivation.and dp dq` attend `dp : ⊢ᴸᴷ¹ Γ + ⦃φ⦄` et `dq : ⊢ᴸᴷ¹ Γ + ⦃ψ⦄` avec le **même** `Γ` ;\n", + "> - l'axiome d'identité donne `⦃p, ¬p⦄` — le passer à `⦃¬p, ¬q, p⦄` est une **inclusion** de multi-ensembles (perte de `¬q`), donc une contraction ;\n", + "> - `IsCutFree` est une famille inductive : ses constructeurs suivent exactement les règles sans coupure (`identity`, `contraction`, `and`, `or`, …) — il n'existe aucun constructeur pour `cut`." + ] + }, + { + "cell_type": "code", + "execution_count": 12, + "id": "493e3dab", + "metadata": { + "execution": { + "iopub.execute_input": "2026-09-25T05:29:02.092494Z", + "iopub.status.busy": "2026-09-25T05:29:02.092114Z", + "iopub.status.idle": "2026-09-25T05:29:02.097342Z", + "shell.execute_reply": "2026-09-25T05:29:02.096332Z" + }, + "papermill": { + "duration": 0.012682, + "end_time": "2026-09-25T05:29:02.098142+00:00", + "exception": false, + "start_time": "2026-09-25T05:29:02.085460+00:00", + "status": "completed" + }, + "tags": [] + }, + "outputs": [ + { + "name": "stdout", + "output_type": "stream", + "text": [ + "Exercice a completer\n" + ] + } + ], + "source": [ + "# --- Exercice 2 : derivation LK composite sans coupure ---\n", + "# TODO etudiant\n", + "# Etape 1 : dConjonction via Derivation.and de deux contractions d'axiomes d'identite\n", + "# Etape 2 : out, rc = run_lean(LEAN_PREAMBLE + \"...\") ; assert rc == 0\n", + "# Etape 3 : mesurer height/size, puis expliquer le role de la contraction dans les inclusions\n", + "print(\"Exercice a completer\")" + ] + }, + { + "cell_type": "markdown", + "id": "47bfd999", + "metadata": { + "papermill": { + "duration": 0.006356, + "end_time": "2026-09-25T05:29:02.109223+00:00", + "exception": false, + "start_time": "2026-09-25T05:29:02.102867+00:00", + "status": "completed" + }, + "tags": [] + }, + "source": [ + "## Exercice 3 : lire les axiomes d'un théorème\n", + "\n", + "### Contexte\n", + "\n", + "`#print axioms` est l'instrument qui distingue deux versions du même théorème dans FFL : `constructiveHauptsatz` (computable) et `hauptsatz` (déclarée `noncomputable`). La différence n'est pas cosmétique — elle dit **ce sur quoi repose la preuve**.\n", + "\n", + "### Objectifs\n", + "\n", + "1. Écrire un snippet Lean qui imprime `#print axioms` pour `Derivation.Canonical.constructiveHauptsatz` **et** pour `Derivation.Canonical.hauptsatz`\n", + "2. Comparer les deux listes : quel axiome apparaît dans l'une et pas dans l'autre ?\n", + "3. Exécuter `#eval dCoupure.height` **après** avoir remplacé `constructiveHauptsatz` par `hauptsatz` dans l'extraction du témoin — que se passe-t-il, et pourquoi ?\n", + "\n", + "> **Indices :**\n", + "> - `#print axioms` accepte un nom pleinement qualifié : `#print axioms FFL.FirstOrder.Derivation.Canonical.hauptsatz` ;\n", + "> - un terme `noncomputable` ne peut pas être évalué par `#eval` : l'erreur le dit ;\n", + "> - la question 3 se répond en lisant le message d'erreur, pas en le contournant." + ] + }, + { + "cell_type": "code", + "execution_count": 13, + "id": "806ff8a7", + "metadata": { + "execution": { + "iopub.execute_input": "2026-09-25T05:29:02.123882Z", + "iopub.status.busy": "2026-09-25T05:29:02.123539Z", + "iopub.status.idle": "2026-09-25T05:29:02.128629Z", + "shell.execute_reply": "2026-09-25T05:29:02.127596Z" + }, + "papermill": { + "duration": 0.013442, + "end_time": "2026-09-25T05:29:02.129477+00:00", + "exception": false, + "start_time": "2026-09-25T05:29:02.116035+00:00", + "status": "completed" + }, + "tags": [] + }, + "outputs": [ + { + "name": "stdout", + "output_type": "stream", + "text": [ + "Exercice a completer\n" + ] + } + ], + "source": [ + "# --- Exercice 3 : comparer les axiomes des deux Hauptsatz ---\n", + "# TODO etudiant\n", + "# Etape 1 : ecrire le snippet Lean avec les deux #print axioms\n", + "# Etape 2 : afficher la sortie ; identifier l'axiome supplementaire de la version noncomputable\n", + "# Etape 3 : tenter #eval sur un terme extrait de hauptsatz et lire l'erreur du noyau\n", + "print(\"Exercice a completer\")" + ] + }, + { + "cell_type": "markdown", + "id": "3d36d2bd", + "metadata": { + "papermill": { + "duration": 0.005643, + "end_time": "2026-09-25T05:29:02.141480+00:00", + "exception": false, + "start_time": "2026-09-25T05:29:02.135837+00:00", + "status": "completed" + }, + "tags": [] + }, + "source": [ + "***\n", + "\n", + "## Conclusion\n", + "\n", + "Ce notebook a posé **une** question — comment calcule-t-on une preuve ? — à trois moteurs, et mesuré leurs réponses sur la même micro-théorie `{p, q, r}` :\n", + "\n", + "- **Hilbert** fournit l'objet le plus élémentaire : une suite de formules, chacune justifiée par un axiome ou un modus ponens. Sa recherche a un coût mesurable, et son vivier d'instanciation en est le paramètre dominant — un résultat négatif du notebook (`(p → q) → ((q → r) → (p → r))` non trouvé) le montre honnêtement.\n", + "- **LK** fournit l'objet le plus structuré : un arbre, dont la **hauteur** et la **taille** se mesurent, et dont la règle de coupure est l'analogue structurel du modus ponens. L'élimination des coupures est un théorème du noyau Lean (`constructiveHauptsatz`), qui rend la dérivation transformée **et** le témoin `IsCutFree`.\n", + "- **Les oracles** (`SimplePlReasoner`, `SatReasoner`) fournissent la réponse la plus rapide — et aucune preuve. Ce sont eux qui vérifient, étape par étape, que la preuve Hilbert trouvée ne dérive que des tautologies.\n", + "\n", + "La leçon transversale : *la taille d'une preuve n'est pas une propriété du théorème, mais du système de calcul qui la représente*. `p → p` coûte cinq formules à Hilbert, un nœud à LK, et zéro à l'oracle — trois façons de « savoir » la même chose.\n", + "\n", + "### Aller plus loin\n", + "\n", + "- **Tweety-02d** — le laboratoire FOL croisé (Tweety répond, Lean certifie) dont ce notebook est le prolongement structurel ;\n", + "- **Tweety-5e** — trois formules-témoins lues par trois moteurs (Tweety, recomptage Python, kernel Lean) ;\n", + "- **Tweety-3b** — le laboratoire modal : schémas `K`/`T`/`4`/`5` énumérés sur 512 cadres Kripke puis certifiés par le pont `FormalLogic.ModalBridge` ;\n", + "- **Foundation (FFL)** — `Foundation/FirstOrder/Hauptsatz.lean`, d'où vient `constructiveHauptsatz`, et `Foundation/FirstOrder/Basic/CutFree.lean` pour `IsCutFree` ;\n", + "- **Lean — série SymbolicAI** — les tactiques qui construisent ces arbres à la main (niveau 1 à 5)." + ] + } + ], + "metadata": { + "kernelspec": { + "display_name": "Python 3 (ipykernel)", + "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": 1029.319699, + "end_time": "2026-09-25T05:29:02.484223+00:00", + "environment_variables": {}, + "exception": null, + "input_path": "Tweety-02e-Preuves-Hilbert-Gentzen-Lean.ipynb", + "output_path": "Tweety-02e-Preuves-Hilbert-Gentzen-Lean.ipynb", + "parameters": {}, + "start_time": "2026-09-25T05:11:53.164524+00:00", + "version": "2.7.0" + } + }, + "nbformat": 4, + "nbformat_minor": 5 +}