Skip to content

feat(lean): certify eight-system ModalZoo subcube #17642

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 2 commits into from
Sep 25, 2026
Merged

feat(lean): certify eight-system ModalZoo subcube #17642

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
bce58b6
feat(lean,#15066): certified modal zoo - FormalLogic.ModalZoo (Tranch…
jsboige Sep 23, 2026
a6be003
docs(lean): clarify ModalZoo countermodel count and build evidence
jsboige Sep 24, 2026
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
6 changes: 6 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 @@ -24,10 +24,16 @@ Modules consommateurs :
déduit du théorème de Löb **prouvé** par FFL (`ProvabilityAbstraction.löb_theorem`),
sans champ postulé, instancié sur la prouvabilité standard de `𝗣𝗔` ; paire de
FairBots de codes distincts par `exclusiveMultifixedpoint`.
- `FormalLogic.ModalZoo` — Tranche G (#15066) : zoo modal certifié sur le sous-cube
`K`, `KD`, `KT`, `KTB`, `K4`, `S4`, `KD45`, `S5` — profil exact d'axiomes de
chaque système (preuve de Hilbert dans un sens, contre-modèle de Kripke fini dans
l'autre), ordre `⪯` équivalent à l'inclusion des profils, diagramme de Hasse
(11 couvertures, 7 paires incomparables) certifié et exporté en JSON.
-/

import FormalLogic.Bridge
import FormalLogic.FolBridge
import FormalLogic.GLBridge
import FormalLogic.ModalBridge
import FormalLogic.FairBotLoeb
import FormalLogic.ModalZoo
Loading
Loading