Skip to content

feat(lean,#15066): pont modal Tweety<->FFL — FormalLogic.ModalBridge (tranche C) #17017

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
myia-ai-01 merged 1 commit into from
Sep 21, 2026
Merged

feat(lean,#15066): pont modal Tweety<->FFL — FormalLogic.ModalBridge (tranche C) #17017

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
5 changes: 5 additions & 0 deletions MyIA.AI.Notebooks/SymbolicAI/Lean/formal_logic_lean/FormalLogic.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -13,7 +13,12 @@ Modules consommateurs :
- `FormalLogic.GLBridge` — pilote Tranche F (#15916) : schéma de Löb, contrôle
négatif par contre-modèle fini, point fixe de de Jongh–Sambin et interprétation
arithmétique sous les conditions de Hilbert–Bernays–Löb.
- `FormalLogic.ModalBridge` — pilote Tranche C (#15066) : logiques modales via
`ModalLogic` (fork compat 4.33.1) — `K` valide sur tout cadre, contre-modèles
finis de `T`/`4`/`5` sur cadres témoins génériques, duaux diamant de `T`/`4`
sur les cadres S4 de Fin74.
-/

import FormalLogic.Bridge
import FormalLogic.GLBridge
import FormalLogic.ModalBridge
132 changes: 132 additions & 0 deletions MyIA.AI.Notebooks/SymbolicAI/Lean/formal_logic_lean/FormalLogic/ModalBridge.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,132 @@
/-
Pont modal Tweety <-> FFL ModalLogic (tranche C de l'EPIC #15066).

Consomme `ModalLogic` au pin exact du lakefile (pilote d'integration mesure) :
- `ModalLogicArchive.Modal.Kripke` (namespace `LO.Modal.Kripke`) : cadres de Kripke
GENERIQUES, sans aucune contrainte de reflexivite/transitivite — le bon substrat
pour discriminer K, T, K4, S5 ;
- `Fin74.Kripke` (definitions a la racine) : cadres reflexifs et transitifs
(S4 par construction), semantique de forcing `x ⊩ A`.

Aucun module upstream n'est vendu ou adapte ici : ce fichier ne fait qu'importer,
definir nos propres temoins finis et les certifier par le kernel.

Plan de la tranche C :
1. `K` (distribution) est valide sur tout cadre — la normalite semantique ;
2. `T` (□p → p), `4` (□p → □□p) et `5` (◇p → □◇p) ECHOUENT chacun sur un cadre
temoin qui viole exactement sa condition frame (irreflexif, non transitif,
non euclidien) — contre-modeles certifies par le kernel ;
3. sur les cadres `Fin74` (reflexifs et transitifs par construction), les duaux
diamant de `T` et `4` sont des theoremes — la structure du cadre les donne.

Choix d'ingenierie : les cadres temoins vivent sur `World := ℕ` et la relation
n'atteint que les mondes 0/1/2 — le contre-modele est le sous-cadre fini
{0,1} ou {0,1,2}, les autres mondes sont isoles (aucun arc). Frames et modeles
sont des `abbrev` (definitions reducibles) : l'elaboration des numeraux
`(0 : model.World)` traverse alors la projection `Model.World` jusqu'a `Nat.OfNat`,
ce qu'un `def` (semi-reductible) refuse. Les eonces portent `Satisfies model x φ`
(forme explicite) : la notation `x ⊧ φ` est polymorphe et ne resout pas le modele
depuis le seul type de `x`. Les deux packages declarent des types distincts
(`LO.Modal.Formula` vs `Formula` racine) : chaque section qualifie explicitement.
-/

import ModalLogicArchive.Modal.Kripke.Basic
import Fin74.Kripke.Basic

namespace FormalLogic.ModalBridge

/-! ## Cadres generiques (`LO.Modal.Kripke`) : ce qui ECHOUE

Un cadre de l'Archive est `<World, Rel>` sans aucune contrainte : on peut y elire
un monde irreflexif, une chaine non transitive, un eventail non euclidien. -/

section GenericFrames

variable {M : LO.Modal.Kripke.Model} {x : M.World} {φ ψ : LO.Modal.Formula ℕ}

/-- `K` (axiome de distribution) : valide sur tout cadre, sans hypothese de structure.
C'est la part de la logique modale que la semantique de Kripke donne gratuitement. -/
theorem forces_kdist (hpq : x ⊧ □(φ 🡒 ψ)) (hp : x ⊧ □φ) : x ⊧ □ψ := by
intro y hxy
exact hpq y hxy (hp y hxy)

/-- Cadre temoin de l'echec de `T` : relation `0 ≺ 1` uniquement (mondes sur ℕ,
les autres isoles). Le monde 0 est irreflexif : `□p` y est vrai (l'unique
successeur 1 verify p) mais `p` y est faux. -/
abbrev frameT : LO.Modal.Kripke.Frame := ⟨ℕ, fun a b => a = 0 ∧ b = 1⟩

abbrev modelT : LO.Modal.Kripke.Model := ⟨frameT, fun a w => a = 0 ∧ w = 1⟩

theorem T_invalid :
¬ (LO.Modal.Formula.Kripke.Satisfies modelT (0 : modelT.World) ((□(.atom 0)) 🡒 (.atom 0))) := by
intro h
have hp : LO.Modal.Formula.Kripke.Satisfies modelT (0 : modelT.World) (□(.atom 0)) :=
fun _ hy => hy
exact absurd (h hp).2 (by decide)

/-- Cadre temoin de l'echec de `4` : chaine `0 ≺ 1 ≺ 2` sans arc `0 ≺ 2`.
Au monde 0, l'unique successeur 1 verify p donc `□p` ; mais 1 a pour successeur 2
ou p echoue, donc `¬□p` en 1, donc `¬□□p` en 0. -/
abbrev frame4 : LO.Modal.Kripke.Frame := ⟨ℕ, fun a b => (a = 0 ∧ b = 1) ∨ (a = 1 ∧ b = 2)⟩

abbrev model4 : LO.Modal.Kripke.Model := ⟨frame4, fun a w => a = 0 ∧ w = 1⟩

theorem four_invalid :
¬ (LO.Modal.Formula.Kripke.Satisfies model4 (0 : model4.World) ((□(.atom 0)) 🡒 (□□(.atom 0)))) := by
intro h
have hp : LO.Modal.Formula.Kripke.Satisfies model4 (0 : model4.World) (□(.atom 0)) := by
intro y hy
rcases hy with ⟨_, hy1⟩ | ⟨h01, _⟩
· exact ⟨rfl, hy1⟩
· exact absurd h01 (by decide)
have hbad : LO.Modal.Formula.Kripke.Satisfies model4 (1 : model4.World) (□(.atom 0)) → False := by
intro h2
exact absurd (h2 (2 : model4.World) (Or.inr ⟨rfl, rfl⟩)).2 (by decide)
exact hbad (h hp (1 : model4.World) (Or.inl ⟨rfl, rfl⟩))

/-- Cadre temoin de l'echec de `5` : eventail `0 ≺ 1`, `0 ≺ 2` (non euclidien).
Au monde 0 : `◇p` via le successeur 1 ; mais le successeur 2 n'a aucun successeur,
donc `¬◇p` en 2, donc `¬□◇p` en 0. -/
abbrev frame5 : LO.Modal.Kripke.Frame := ⟨ℕ, fun a b => a = 0 ∧ (b = 1 ∨ b = 2)⟩

abbrev model5 : LO.Modal.Kripke.Model := ⟨frame5, fun a w => a = 0 ∧ w = 1⟩

theorem five_invalid :
¬ (LO.Modal.Formula.Kripke.Satisfies model5 (0 : model5.World) ((◇(.atom 0)) 🡒 (□◇(.atom 0)))) := by
intro h
-- `◇` n'est PAS definitionnellement un `∃` dans l'Archive : `Satisfies M x (◇φ)` se
-- reduit en `∼□∼φ`, une fleche. Toute destruction de `◇` passe par `dia_def`.
have hdia : LO.Modal.Formula.Kripke.Satisfies model5 (0 : model5.World) (◇(.atom 0)) :=
LO.Modal.Formula.Kripke.Satisfies.dia_def.mpr
⟨(1 : model5.World), ⟨rfl, Or.inl rfl⟩, ⟨rfl, rfl⟩⟩
have hbad : LO.Modal.Formula.Kripke.Satisfies model5 (2 : model5.World) (◇(.atom 0)) → False := by
intro h2
obtain ⟨y, hy, _⟩ := LO.Modal.Formula.Kripke.Satisfies.dia_def.mp h2
exact absurd hy.1 (by decide)
exact hbad (h hdia (2 : model5.World) ⟨rfl, Or.inr rfl⟩)

end GenericFrames

/-! ## Cadres S4 (`Fin74.Kripke`, definitions racine) : ce que la structure DONNE

Un cadre `Frame` de Fin74 porte `rel_refl` et `rel_trans` comme champs de donnees :
reflexivite et transitivite ne sont pas des hypotheses, elles sont le cadre.
Les duaux diamant de `T` (`A → ◇A`) et de `4` (`◇◇A → ◇A`) s'y derivent
en une ligne chacun. -/

section S4Frames

variable {κ : Type} {M : Model κ ℕ} {x : M.World} {A : Formula ℕ}

/-- Dual diamant de `T` : la reflexivite du cadre donne `A → ◇A`. -/
theorem forces_dia_of_refl (hA : x ⊩ A) : x ⊩ ◇A :=
⟨x, M.rel_refl x, hA⟩

/-- Dual diamant de `4` : la transitivite du cadre donne `◇◇A → ◇A`. -/
theorem forces_dia_dia (h : x ⊩ ◇◇A) : x ⊩ ◇A := by
obtain ⟨y, xy, ⟨z, yz, hz⟩⟩ := h
exact ⟨z, M.rel_trans xy yz, hz⟩

end S4Frames

end FormalLogic.ModalBridge
114 changes: 62 additions & 52 deletions MyIA.AI.Notebooks/SymbolicAI/Lean/formal_logic_lean/lake-manifest.json
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,27 +1,7 @@
{"version": "1.2.0",
"packagesDir": ".lake/packages",
"packages":
[{"url": "https://github.com/FormalizedFormalLogic/ProvabilityLogic.git",
"type": "git",
"subDir": null,
"scope": "",
"rev": "01628c51f618fd11f2f6b10c813f261f1d36c7a6",
"name": "ProvabilityLogic",
"manifestFile": "lake-manifest.json",
"inputRev": "01628c51f618fd11f2f6b10c813f261f1d36c7a6",
"inherited": false,
"configFile": "lakefile.toml"},
{"url": "https://github.com/FormalizedFormalLogic/Foundation.git",
"type": "git",
"subDir": null,
"scope": "",
"rev": "81810b9f22c49fbb32bd89c1e9737059d83a37e6",
"name": "Foundation",
"manifestFile": "lake-manifest.json",
"inputRev": "81810b9f22c49fbb32bd89c1e9737059d83a37e6",
"inherited": false,
"configFile": "lakefile.toml"},
{"url": "https://github.com/leanprover-community/mathlib4.git",
[{"url": "https://github.com/leanprover-community/mathlib4.git",
"type": "git",
"subDir": null,
"scope": "",
Expand All @@ -31,46 +11,36 @@
"inputRev": "v4.33.1",
"inherited": false,
"configFile": "lakefile.lean"},
{"url": "https://github.com/FormalizedFormalLogic/forgive",
{"url": "https://github.com/MyIntelligenceAgency/ModalLogic.git",
"type": "git",
"subDir": null,
"scope": "",
"rev": "32667a1902df73e5f27cdfcef57855e6b8b24d55",
"name": "Forgive",
"rev": "71968137b917a708c700047e1e6d3eb6cc4ed078",
"name": "ModalLogic",
"manifestFile": "lake-manifest.json",
"inputRev": "32667a1902df73e5f27cdfcef57855e6b8b24d55",
"inherited": true,
"inputRev": "71968137b917a708c700047e1e6d3eb6cc4ed078",
"inherited": false,
"configFile": "lakefile.toml"},
{"url": "https://github.com/SnO2WMaN/lean-typst.git",
{"url": "https://github.com/FormalizedFormalLogic/ProvabilityLogic.git",
"type": "git",
"subDir": null,
"scope": "",
"rev": "888d8656b06ebbd5d23688231ea0f78c93dbc556",
"name": "LeanTypst",
"rev": "01628c51f618fd11f2f6b10c813f261f1d36c7a6",
"name": "ProvabilityLogic",
"manifestFile": "lake-manifest.json",
"inputRev": "main",
"inherited": true,
"configFile": "lakefile.lean"},
{"url": "https://github.com/SnO2WMaN/axiom-audit",
"inputRev": "01628c51f618fd11f2f6b10c813f261f1d36c7a6",
"inherited": false,
"configFile": "lakefile.toml"},
{"url": "https://github.com/FormalizedFormalLogic/Foundation.git",
"type": "git",
"subDir": null,
"scope": "",
"rev": "827e715d39231df230cb5b1a200be07c151b323b",
"name": "«axiom-audit»",
"rev": "81810b9f22c49fbb32bd89c1e9737059d83a37e6",
"name": "Foundation",
"manifestFile": "lake-manifest.json",
"inputRev": "827e715d39231df230cb5b1a200be07c151b323b",
"inherited": true,
"inputRev": "81810b9f22c49fbb32bd89c1e9737059d83a37e6",
"inherited": false,
"configFile": "lakefile.toml"},
{"url": "https://github.com/leanprover/doc-gen4",
"type": "git",
"subDir": null,
"scope": "leanprover",
"rev": "e2af49a7b7e5e1a9224008c1f15e7aa4f58a4015",
"name": "«doc-gen4»",
"manifestFile": "lake-manifest.json",
"inputRev": "v4.33.1",
"inherited": true,
"configFile": "lakefile.lean"},
{"url": "https://github.com/leanprover-community/plausible",
"type": "git",
"subDir": null,
Expand Down Expand Up @@ -141,6 +111,46 @@
"inputRev": "main",
"inherited": true,
"configFile": "lakefile.toml"},
{"url": "https://github.com/FormalizedFormalLogic/forgive",
"type": "git",
"subDir": null,
"scope": "",
"rev": "32667a1902df73e5f27cdfcef57855e6b8b24d55",
"name": "Forgive",
"manifestFile": "lake-manifest.json",
"inputRev": "32667a1902df73e5f27cdfcef57855e6b8b24d55",
"inherited": true,
"configFile": "lakefile.toml"},
{"url": "https://github.com/SnO2WMaN/lean-typst.git",
"type": "git",
"subDir": null,
"scope": "",
"rev": "2158f3dec8911bc8cb1afc7fd1bc95b0e58d42fb",
"name": "LeanTypst",
"manifestFile": "lake-manifest.json",
"inputRev": "main",
"inherited": true,
"configFile": "lakefile.lean"},
{"url": "https://github.com/SnO2WMaN/axiom-audit",
"type": "git",
"subDir": null,
"scope": "",
"rev": "827e715d39231df230cb5b1a200be07c151b323b",
"name": "«axiom-audit»",
"manifestFile": "lake-manifest.json",
"inputRev": "827e715d39231df230cb5b1a200be07c151b323b",
"inherited": true,
"configFile": "lakefile.toml"},
{"url": "https://github.com/leanprover/doc-gen4",
"type": "git",
"subDir": null,
"scope": "leanprover",
"rev": "0bc516c1b9db83658d6475c40d9b1ed71219b921",
"name": "«doc-gen4»",
"manifestFile": "lake-manifest.json",
"inputRev": "v4.31.0",
"inherited": true,
"configFile": "lakefile.lean"},
{"url": "https://github.com/leanprover/lean4-cli",
"type": "git",
"subDir": null,
Expand All @@ -155,7 +165,7 @@
"type": "git",
"subDir": null,
"scope": "",
"rev": "6168b7549738a19bc837a1625c60c5d1e5dd8aeb",
"rev": "0be4df908d1a8e75b58961041e2b4973692623df",
"name": "leansqlite",
"manifestFile": "lake-manifest.json",
"inputRev": "main",
Expand All @@ -165,7 +175,7 @@
"type": "git",
"subDir": null,
"scope": "",
"rev": "37e7d8cb7316a88cd3e91208385c9ec6ae780019",
"rev": "a2e430a4c9d3ad24078b8581fe0162fc5b0c9a6c",
"name": "UnicodeBasic",
"manifestFile": "lake-manifest.json",
"inputRev": "main",
Expand All @@ -175,17 +185,17 @@
"type": "git",
"subDir": null,
"scope": "",
"rev": "852edafa268eb038a7158551fd580ee8433847b0",
"rev": "5d31b64fb703c5d77f6ef4d1fb958f9bdf1ea539",
"name": "BibtexQuery",
"manifestFile": "lake-manifest.json",
"inputRev": "master",
"inputRev": "nightly-testing",
"inherited": true,
"configFile": "lakefile.toml"},
{"url": "https://github.com/acmepjz/md4lean",
"type": "git",
"subDir": null,
"scope": "",
"rev": "31907cc18f48a95384f99cee5582c00fb39e0f67",
"rev": "6a3fb240133bcb7e1a066fdc784b3fdc304e3fc5",
"name": "MD4Lean",
"manifestFile": "lake-manifest.json",
"inputRev": "main",
Expand Down
18 changes: 15 additions & 3 deletions MyIA.AI.Notebooks/SymbolicAI/Lean/formal_logic_lean/lakefile.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -7,15 +7,27 @@ open Lake DSL
package «formal_logic_lean» where
leanOptions := #[⟨`autoImplicit, false⟩]

require mathlib from git
"https://github.com/leanprover-community/mathlib4.git" @ "v4.33.1"

require «Foundation» from git
"https://github.com/FormalizedFormalLogic/Foundation.git" @ "81810b9f22c49fbb32bd89c1e9737059d83a37e6"

require «ProvabilityLogic» from git
"https://github.com/FormalizedFormalLogic/ProvabilityLogic.git" @ "01628c51f618fd11f2f6b10c813f261f1d36c7a6"

-- Pilote d'integration ModalLogic (tranche C #15066) : upstream reste en Lean 4.31.0
-- (origin/main mesure au 2026-09-20, aucune branche/PR de compat), notre lake reste en toolchain 4.33.1.
-- Consomme donc le fork MyIntelligenceAgency/ModalLogic = upstream 9c485ca95e35 + 3 commits de
-- compat 4.33.1 (dsimp->simp sur 2 preuves ; restauration des instances HasSubset Set/Finset
-- retirees de mathlib v4.33.1 ; fermeture de setOf_iff apres deprecation de setOf) — aucun
-- changement semantique, diff public sur le fork.
-- NB : `require mathlib` reste en DERNIER (message de `lake exe cache get`) pour que les revs
-- transitives (plausible, batteries, Qq, proofwidgets) soient celles de mathlib v4.33.1 et non
-- celles du manifest 4.31 de ModalLogic.
require «ModalLogic» from git
"https://github.com/MyIntelligenceAgency/ModalLogic.git" @ "71968137b917a708c700047e1e6d3eb6cc4ed078"

require mathlib from git
"https://github.com/leanprover-community/mathlib4.git" @ "v4.33.1"

@[default_target]
lean_lib «FormalLogic» where
globs := #[.submodules `FormalLogic]
Loading