[EPIC] Formalized Formal Logic — articuler les séries Tweety et Lean

[jsboige]

Formalized Formal Logic — articuler la série Tweety et la série Lean

Intention

Construire un parcours transversal où Tweety exécute et compare des systèmes logiques, tandis que Lean expose leurs syntaxes, sémantiques et métathéorèmes comme objets certifiés.

Le corpus de référence est l’organisation active Formalized Formal Logic, et non un import monolithique du fork découvert initialement. Le parcours doit rendre visible la différence entre :

1. demander à un raisonneur si une formule est satisfaite ou dérivable ;
2. définir formellement syntaxe, preuve et sémantique ;
3. certifier correction, complétude, décidabilité ou impossibilité ;
4. transporter un témoin calculé par Tweety/SPASS/solveur vers un petit vérificateur Lean.

Cette articulation complète les ponts déjà livrés dans Tweety :

• Tweety-5b-Lean-Argumentation : sémantique grounded certifiée ;
• Tweety-5d-Stable-Synthesis-Lean : générateur Z3 → témoin → certificat Lean ;
• série Lean 1–5 : types, propositions, quantificateurs et tactiques.

Elle ne remplace pas l’Epic #15062, qui reste centré sur les jeux-programmes, FairBot et la coopération one-shot.

Source de vérité et provenance

Dépôts canoniques actifs

Dépôt	Rôle	État mesuré le 2026-09-07
FormalizedFormalLogic/Foundation	infrastructure logique, propositionnel, FOL, arithmétique, arithmétisation, incomplétude, théorie des ensembles	Apache-2.0, 199 modules Lean, Lean 4.33.1
FormalizedFormalLogic/ModalLogic	logiques modales, sémantiques de Kripke et de voisinage, calculs et zoos	Apache-2.0, 689 modules Lean, Lean 4.31.0 ; dépend de Foundation/master
FormalizedFormalLogic/ProvabilityLogic	GL et apparentées, calculs Hilbert/Gentzen, Kripke, recherche de preuves, réalisations arithmétiques/Solovay	Apache-2.0, 98 modules Lean, Lean 4.33.1 ; dépend de Foundation/master
FormalizedFormalLogic/InterpretabilityLogic	logique d’interprétabilité et sémantique de Veltman	Apache-2.0, 69 modules, Lean 4.31.0 ; maturité hétérogène, majorité sous InterpretabilityLogicArchive/

L’upstream Foundation a extrait ProvabilityLogic le 2026-07-02 (#829) puis la logique modale le 2026-07-22 (#852). Un audit actuel doit donc suivre ces dépôts séparés, pas l’ancien arbre monolithique.

Statut du fork tosiaki/Foundation-SetTheory

Le fork tosiaki/Foundation-SetTheory est divergent, pas simplement « en retard » : comparaison GitHub FormalizedFormalLogic/Foundation:master...tosiaki:master mesurée à 26 commits en avance / 75 en retard, base commune e014827ec89d….

• Ses commits propres concernent surtout la théorie des ensembles, la récursion et des refactors associés ; ils peuvent contenir une contribution spécialisée utile.
• Il reste sur Lean v4.28.0-rc1 et conserve l’ancien arbre monolithique (590 modules).
• Il n’est donc ni la source canonique générale, ni une dépendance à adopter telle quelle.

Règle de provenance : tout pilote part du dépôt FFL actif correspondant. Le fork tosiaki n’est consulté que pour un résultat propre explicitement identifié, avec comparaison au merge-base et verdict séparé.

Déconflit avec le corpus CoursIA

• Tweety-2 couvre déjà la pratique de la logique propositionnelle et du premier ordre avec solveurs.
• Tweety-2b-Semantics-Csharp couvre déjà les mondes possibles propositionnels.
• Tweety-2c-FOL-Csharp consomme déjà le vrai stack FOL Tweety via IKVM.
• Tweety-3 et Tweety-3-ModalLogic-Csharp couvrent déjà la logique modale côté raisonneur.
• Tweety-4 couvre déjà incohérence/révision de croyances ; cet Epic n’en fait pas une formalisation AGM complète.
• Tweety-5b/5d ont déjà établi le patron « calculer/générer, puis certifier ».
• Lean 1–5 enseigne déjà les primitives de preuve, mais pas encore la métalogique comme domaine formalisé.

Nouvel apport : une même formule et un même petit modèle traversent les deux séries, depuis l’exécution Tweety jusqu’au métathéorème Lean, avec des contrôles croisés falsifiables.

Parcours proposé

Tranche A — laboratoire propositionnel : validité, preuve et contre-modèle

Créer un companion transversal de Tweety-2 / Lean-3 :

• choisir un fragment fini et une syntaxe commune sérialisable ;
• calculer tables de vérité, satisfaisabilité et contre-modèles avec Tweety ;
• définir/interroger les objets correspondants de Foundation/Propositional ;
• montrer sur les mêmes formules la différence satisfiable, valid, provable ;
• certifier au moins un théorème et un contre-modèle dans Lean ;
• contrôle négatif : une formule satisfiable mais non valide.

Le notebook doit utiliser le vrai raisonneur Tweety et un kernel Lean natif ; aucune réimplémentation jouet ne remplace ces deux moteurs.

Tranche B — FOL : dérivation, modèle et complétude

Companion transversal de Tweety-2/2c et Lean-4 :

• syntaxe FOL, substitution, théorie, structure et satisfaction ;
• même micro-théorie exécutée par EProver/Tweety puis représentée en Lean ;
• témoin modèle ou dérivation transporté dans un format minimal ;
• visite certifiée de Foundation/FirstOrder/Completeness/CounterModel.lean, de Foundation/FirstOrder/Hauptsatz.lean et de la traduction de Gödel–Gentzen ;
• distinguer soigneusement complétude sémantique de Gödel et théorèmes d’incomplétude arithmétique.

Le théorème général de complétude est consommé/interrogé ; il n’est pas redémontré dans CoursIA.

Tranche C — logique modale : du raisonneur aux cadres de Kripke

Companion transversal de Tweety-3 / Tweety-3-ModalLogic-Csharp :

• exécuter des formules discriminant K, T, K4, S4 et S5 ;
• représenter explicitement cadres, valuations et accessibilité ;
• relier chaque axiome à une propriété du cadre ;
• construire un contre-modèle calculé côté Tweety/SPASS et le revérifier côté Lean ;
• exploiter FormalizedFormalLogic/ModalLogic pour les calculs, sémantiques, filtration et résultats de correction/complétude disponibles ;
• présenter le « zoo » comme carte certifiée des relations de force, pas comme simple image.

Acceptance Prong-B : au moins deux logiques doivent produire des verdicts différents sur la même formule ou le même cadre.

Tranche D — calculs de preuve : Hilbert, séquents et élimination des coupures

Créer un atelier métalogique adossé à Lean :

• comparer preuve à la Hilbert, séquents de Gentzen et recherche automatique ;
• illustrer la différence entre une dérivation et sa vérification ;
• consommer Foundation/FirstOrder/Hauptsatz.lean et les calculs Tait/Gentzen ;
• mesurer sur un petit corpus taille/profondeur de preuves avant/après normalisation lorsque l’API le permet ;
• relier explicitement ce travail à Lean-7/8/10 (génération de preuves, agents, LeanDojo), sans confondre un moteur de recherche avec une preuve certifiée.

Tranche E — calculabilité, diagonalisation et limites

Créer un arc Lean autonome, prérequis de #15062 L2/L3 mais valable indépendamment :

• machines/relations calculables, prédicats récursivement énumérables et problème de l’arrêt ;
• lemme diagonal et point fixe arithmétisé (Foundation/FirstOrder/Bootstrapping/FixedPoint.lean) ;
• incomplétude depuis l’indécidabilité (Incompleteness/Halting.lean) ;
• Gödel I/II, Gödel–Rosser, Löb et indéfinissabilité de la vérité de Tarski ;
• démonstrations courtes par #check/#print axioms et petits témoins exécutables, sans prétendre reproduire toute l’arithmétisation.

Exigence pédagogique : séparer quatre énoncés souvent amalgamés — indécidabilité de FOL, problème de l’arrêt, incomplétude d’une théorie arithmétique, indéfinissabilité de la vérité.

Tranche F — logique de prouvabilité GL, pont explicite vers #15062

Pilote sur FormalizedFormalLogic/ProvabilityLogic :

• syntaxe modale de prouvabilité et axiome de Löb ;
• sémantique de Kripke de GL ;
• comparer calculs Hilbert, Gentzen et recherche labellisée ;
• interroger le point fixe GL et les interprétations/phrases de Solovay disponibles ;
• fournir à [EPIC] Math for AI Safety — jeux-programmes, coopération transparente et prouvabilité Lean #15062 une interface consommateur minimale pour FairBot, sans dupliquer son notebook jeux-programmes.

Cette tranche est le seul pont obligatoire vers #15062. L’Epic présent reste fondationnel ; #15062 porte l’application aux jeux.

Tranche G — zoos de logiques comme cartographie exécutable

À partir des zoos FFL :

• extraire un sous-graphe borné de relations de force entre systèmes ;
• vérifier dans Lean les arêtes utilisées ;
• faire prédire aux étudiants une inclusion puis chercher un contre-modèle ou une séparation ;
• relier les choix de logique à des capacités de raisonnement d’agents, sans anthropomorphiser les opérateurs modaux.

Sortie attendue : une visualisation issue de données certifiées et ≥3 exercices, pas une galerie statique.

Pilotes d’intégration Lean — trois verdicts, dépôt par dépôt

Aucun dépôt FFL n’est vendorisé d’emblée. Pour chaque tranche qui en dépend :

1. fresh clone au commit exact ;
2. lake exe cache get puis build sur le pin déclaré ;
3. mesurer le graphe d’import de l’API minimale ;
4. tester la compatibilité avec le toolchain CoursIA courant ;
5. auditer licence, sorry/axiomes et maintenance ;
6. rendre un verdict IMPORTABLE, CONSUMER_PINNÉ, PORT_BORNÉ ou RÉFÉRENCE_SEULE.

Ordre recommandé au 2026-09-07 :

1. Foundation 4.33.1 — meilleur candidat, aligné sur Mathlib 4.33.1 ;
2. ProvabilityLogic 4.33.1 — pertinent pour GL/[EPIC] Math for AI Safety — jeux-programmes, coopération transparente et prouvabilité Lean #15062, mais dépend aussi de LeanTypst et de branches mouvantes ;
3. ModalLogic 4.31.0 — forte valeur Tweety, migration à mesurer ;
4. InterpretabilityLogic 4.31.0 — RÉFÉRENCE_SEULE par défaut tant que l’API non-archive n’est pas suffisante ;
5. tosiaki/Foundation-SetTheory 4.28-rc1 — uniquement pilote spécialisé sur ses commits propres de théorie des ensembles.

Seuil de sortie par pilote : arrêter en RÉFÉRENCE_SEULE si l’intégration exige un fork permanent, plus de 3 modules adaptés / 1000 lignes, un nouveau sorry, ou une dépendance non maintenue sans bénéfice pédagogique directement démontré.

Ce qui relève d’un suivi séparé

Ces richesses sont réelles mais ne doivent pas gonfler le pont Tweety ↔ Lean :

• théorie des ensembles Z/ZF/ZFC, univers et récursion — éventuel Epic dédié ;
• second ordre et logique linéaire — futurs arcs propres si besoin pédagogique établi ;
• logique d’interprétabilité complète et sémantique de Veltman — référence avancée, non obligatoire ;
• argument ontologique de Gödel — hors périmètre de cet Epic ;
• port intégral des 590 modules du fork — explicitement exclu.

Critères d’acceptation globaux

• Tranches A, B et C : chaque pont exécute un moteur Tweety/tiers réel et un consommateur Lean natif sur les mêmes objets.
• Au moins un théorème et un contre-modèle sont vérifiés indépendamment dans chaque tranche A–C.
• Tranche D distingue recherche, dérivation et vérification, avec métriques sur un corpus borné.
• Tranche E sépare explicitement arrêt, indécidabilité, incomplétude et vérité.
• Tranche F fournit le socle GL consommable par [EPIC] Math for AI Safety — jeux-programmes, coopération transparente et prouvabilité Lean #15062 sans dupliquer les jeux-programmes.
• Chaque claim de métathéorie cite le module et le théorème FFL exacts ; aucun claim dérivé du README seul.
• Chaque dépendance a un commit pin exact et un verdict d’intégration mesuré.
• Aucun nouveau sorry; proof-integrity et #print axioms couvrent les déclarations exposées.
• Notebooks exécutés avec outputs réels, ≥3 exercices chacun, README Lean et Tweety mis à jour sans régénérer manuellement le catalogue.
• Le fork tosiaki n’est utilisé que pour un résultat propre qualifié contre l’upstream.

Découpage attendu

Une sous-issue atomique par tranche A–G, plus une sous-issue pilote par dépôt FFL réellement consommé. Les claims sont partitionnés par notebook/lake. L’Epic peut fermer avec A+B+C+E, un verdict mesuré sur Foundation, et au moins un des pilotes D/F/G ; les autres tranches peuvent devenir des suivis nommés.

[jsboige]

Grain: DEEP/notebook-lean — lane myia-po-2024:CoursIA — prev: LIGHT/docs #15579

[CLAIMED] lane myia-po-2024:CoursIA -- Tranche A : laboratoire propositionnel (validite, preuve, contre-modele), notebook companion Tweety-2 <-> Lean-3 -- precede du pilote d'integration Foundation (FFL, Lean 4.33.1) : clone frais au commit exact, build sur pin, verdict IMPORTABLE/CONSUMER_PINNE/PORT_BORNE/REFERENCE_SEULE avant toute consommation -- paths: MyIA.AI.Notebooks/SymbolicAI/Tweety/Tweety-5e-Propositional-Lab-Lean.ipynb -- See #15066 (contribution partielle EPIC, jamais Closes)

[jsboige]

Grain: DEEP/notebook-lean — lane myia-po-2026:CoursIA-2 — prev: MED/lean #16328

[CLAIMED] lane myia-po-2026:CoursIA-2 -- Tranche E : arc Lean autonome calculabilite/diagonalisation/limites (halting, point fixe, Goedel I/II+Rosser, Loeb, Tarski) via le lac formal_logic_lean existant (CONSUMER_PINNE Foundation+ProvabilityLogic, pins #15563/#15923 inchangés) -- nouveau notebook Lean-34, consommation par #check/#print axioms + temoins executables, sans re-demontrer l'arithmetisation -- paths: MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-34-Calculabilite-et-Limites.ipynb -- See #15066 (contribution partielle EPIC, jamais Closes)

[jsboige]

Tranche E livrée : PR #16356 — notebook Lean-34-Calculabilite-et-Limites.ipynb (kernel python3, 11 cellules code exécutées sans erreur) + ligne README. Build formal_logic_lean des 8 modules cibles rc=0 (1226 jobs), 4 audits lake env lean (#check + #print axioms sur les 12 théorèmes — axiomes standard du noyau uniquement). Claim de issuecomment-5687441499 honoré.

[jsboige]

Grain: DEEP/notebook-lean — lane myia-po-2024:CoursIA — prev: MED/guard #16839

[CLAIMED] lane myia-po-2024:CoursIA -- Tranche C : laboratoire modal Tweety-3 <-> FFL ModalLogic (formules discriminantes K/T/K4/S4/S5, cadres de Kripke, contre-modeles calcules Tweety puis reverifies Lean, Prong-B deux verdicts differents sur la meme formule) -- paths: MyIA.AI.Notebooks/SymbolicAI/Tweety/Tweety-3b-Modal-Lab-Lean.ipynb, MyIA.AI.Notebooks/SymbolicAI/Lean/formal_logic_lean/** -- 2026-09-20T09:57Z

Precede du pilote d'integration ModalLogic (EPIC : aucun depot FFL n'est vendorise d'embla) : clone frais au commit exact 9c485ca95e35, build sur le pin consommateur v4.33.1 du lake formal_logic_lean, verdict mesure IMPORTABLE/CONSUMER_PINNE/PORT_BORNE/REFERENCE_SEULE avant toute ecriture de notebook.

[jsboige]

Mesure : le pin ModalLogic 9c485ca95e35 ne build pas sous le stack du pilote

Worktree pilote (ffl-modal-lab), lakefile avec mathlib en dernier (revs transitives inherited vérifiées dans le manifest : plausible b7eb3304aeae, batteries 4488d40d070b, Qq 92c15be17b7c, proofwidgets 4be2e3d5087e), mathlib 0df444a360ea + lake exe cache get OK (8690 fichiers), toolchain leanprover--lean4---v4.33.1 :

lake build FormalLogic.ModalBridge
error: ModalLogicArchive/Modal/LogicSymbol.lean:347:65: unsolved goals
error: ModalLogicArchive/Modal/LogicSymbol.lean:430:65: unsolved goals
Some required targets logged failures:
- ModalLogicArchive.Vorspiel.AdjunctiveSet
- ModalLogicArchive.Logic.Semantics
- ModalLogicArchive.Modal.LogicSymbol
BUILD_RC_PIPESTATUS=1 (2026-09-20T12:34:33Z)

Goal bloquant (430:65) : map (fun x => ◇^[n]x) [φ] = [◇^[n]φ] — le composant ModalLogicArchive du pin ne compile pas tel quel sous 4.33.1 / mathlib 0df444a.

Conséquence pour Tweety-3b : le notebook ne peut pas consommer FormalLogic.ModalBridge tant que la target ne build pas. Pistes, dans l'ordre que j'investigue :

1. resserrer la dépendance — l'échec est dans les cibles required transitives ; si ModalBridge n'a besoin réellement que d'une sous-partie du pin qui compile, exiger uniquement celle-ci ;
2. patch local des trois cibles cassées dans le lake compagnon (fork du pin dans le worktree pilote) ;
3. re-pin ModalLogic sur une rev qui compile sous 4.33.1.

Premier run mort silencieusement pendant lake update (690 s de décompression prises pour un freeze) — relance idempotente qui a produit la mesure ci-dessus ; pas de OOM, mémoire saine après.

[jsboige]

[REPLY] lane myia-po-2024:CoursIA — suite du verdict build FAIL : les pistes 1 et 3 sont mortes (mesuré), la piste 2 est engagée et presque verte.

Piste 3 (re-pin upstream) — MORTE

FormalizedFormalLogic/ModalLogic : origin/main toujours lean-toolchain v4.31.0 (mesuré 2026-09-20, dernier push 2026-08-01), 14 branches = toutes nbhd-*/zoo-* pré-bump, 0 PR ouverte. Il n'existe aucune rev compilant sous 4.33.1.

Piste 1 (import plus étroit) — MORTE

Fermeture transitive mesurée depuis ModalBridge.lean : Kripke.Basic → Modal.Logic.Basic → Modal.Formula.Basic → **Modal.LogicSymbol** (le fichier aux 2 preuves cassées) — public import, aucun contournement. Fin74.Kripke.Basic est propre mais n'exonère pas la chaîne Archive.

Piste 2 (fork + patch local) — ENGAGÉE

Fork créé : MyIntelligenceAgency/ModalLogic, branche coursia-v4.33.1-compat = upstream 9c485ca95e35 + corrections de drift 4.33.1, zéro changement sémantique :

1. Modal/LogicSymbol.lean:347,430 — by dsimp [boxItr] laisse un résidu définitionnel map f [φ] = [f φ] → by simp [boxItr] (fermé via List.map_cons/nil). Vert vérifié au build (143 s).
2. Vorspiel/AdjunctiveSet.lean:26,41 — cause racine mesurée au probe : mathlib v4.33.1 a retiré les instances HasSubset (Set α)/HasSubset (Finset α) (la notation ⊆ s'elabore desormais en LE.le via Set.instLE/Preorder.toLE) → la classe AdjunctiveSet (qui étend HasSubset α) échoue avec Fields missing: Subset. Fix : instances locales ⟨Set.Subset⟩ / ⟨(· ≤ ·)⟩.
3. Logic/Semantics.lean:219 — setOf_iff : drift simp, fix en cours.

Le lakefile du pilote épingle le fork au SHA exact (commentaire documente la provenance). Conséquence pour Tweety-3b : dès que FormalLogic.ModalBridge build, l'assemblage notebook reprend (patron #16888 Tweety-02d).