Tweety-3b — Labo Modal : Kripke répond, Lean certifie

Série Tweety — laboratoires croisés Java ↔︎ Python ↔︎ Lean (EPIC #15066, Tranche C, pont #17017). Un même zoo de formules modales, trois moteurs : Tweety (Java, via JPype) manipule la syntaxe []/<> ; un moteur de Kripke en Python énumère cadres et valuations — les conditions de cadre émergent du comptage ; le lake formal_logic_lean (pont FormalLogic.ModalBridge) certifie validité de K et contre-modèles de T, 4, 5 comme objets vérifiés par le noyau Lean.

Navigation : Tweety-3-Advanced-Logics (tour DL/Modale/QBF/CL) · Tweety-3c-ModalLogic-Csharp (port C#) · Tweety-02d-FOL-Lab-Lean (labo FOL, même patron) · README

Objectifs pédagogiques

Manipuler la syntaxe modale avec le MlParser de Tweety — et rencontrer la limite upstream : le raisonneur SPASS est cassé pour les formules modalisées (Issue #1334), le notebook 3 le documente, ce labo le contourne par la sémantique, pas par l’abandon
Exécuter une sémantique de Kripke complète en Python : forcing x |= f, clause [] = « pour tout successeur », <> = « il existe »
Mesurer la théorie de la correspondance par balayage exhaustif : sur les 512 cadres à 3 mondes, T est falsifiable exactement sur les cadres non réflexifs, 4 sur les non transitifs, 5 sur les non euclidiens — et K sur aucun
Certifier chaque constat : K valide sur tout cadre devient un théorème Lean ; les falsifications de T/4/5 deviennent des contre-modèles exhibés et vérifiés par le noyau ; sur les cadres S4 (Fin74), réflexivité et transitivité donnent les duaux diamant
Mesurer la provenance du corpus (pins git rev-parse confrontés au manifest) avant toute certification

Prérequis

Tweety-01-Setup-Python exécuté (JVM, JARs, JPype) — le dossier libs/ du répertoire Tweety
Notions modales : le volet 2.4 de Tweety-3 (syntaxe []/<>, bug SPASS)
Pour les sections 5-6 : 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)

Durée estimée : 45 minutes

Position dans la série : compagnon modal des labos Tweety-5e (propositionnel) et Tweety-02d (FOL) — même patron (moteur exécuté ↔︎ noyau certifiant). Ce labo consomme le pont FormalLogic.ModalBridge (Tranche C de l’EPIC, livré par #17017) : les cadres témoins certifiés côté Lean sont les mêmes que ceux énumérés côté Python.

1. La question du labo

La formule []p -> p (l’axiome T : « ce qui est nécessaire est vrai ») est-elle valide — vraie dans tous les mondes de tous les modèles ?

En logique propositionnelle ou FOL, la question aurait une réponse binaire. En modal, elle n’en a pas : tout dépend du cadre. La sémantique de Kripke évalue une formule relativement à un monde x dans un modèle (W, R, V) — un ensemble de mondes, une relation d’accessibilité R, une valuation V :

x satisfait []f si tout monde accessible depuis x satisfait f ;
x satisfait <>f si quelque monde accessible depuis x satisfait f.

Alors []p -> p échoue dès qu’un monde x n’a pas accès à lui-même : []p peut y être vrai (tous les successeurs voient p) pendant que p y est faux. La logique modale n’est pas une logique : c’est un spectre — K, T, K4, S4, S5 — obtenu en imposant des conditions sur le cadre (réflexivité, transitivité, euclidianité). C’est la théorie de la correspondance, et ce labo la fait émerger d’un comptage puis la fait certifier par un noyau.

Le plan, dans l’esprit de la série :

Section	Moteur	Ce qu’il donne
2	Tweety (Java)	la syntaxe : parser `[]`/`<>`, rendre l’arbre — et la limite SPASS
3-4	moteur Kripke (Python)	la sémantique : témoins ciblés, puis balayage exhaustif 512 cadres
5	`formal_logic_lean` (Lean)	les certificats : théorème pour tout cadre, contre-modèles kernel-vérifiés
6	—	le bilan croisé des trois lectures

# --- Initialisation JVM Tweety (helper partage de la serie) + imports modaux ---
import os
import pathlib
import sys

TWEETY_DIR = pathlib.Path.cwd()
if TWEETY_DIR.name != "Tweety":
    # execution hors du dossier Tweety : retour au chemin canonique
    candidat = pathlib.Path("MyIA.AI.Notebooks") / "SymbolicAI" / "Tweety"
    if candidat.is_dir():
        os.chdir(candidat)
        TWEETY_DIR = pathlib.Path.cwd()
sys.path.insert(0, str(TWEETY_DIR))

from tweety_init import init_tweety

jvm_ready = init_tweety(verbose=True)
if not jvm_ready:
    # Contrat d'execution : echec visible, aucun contournement (regle F)
    raise RuntimeError(
        "init_tweety a echoue (JAVA_HOME, dossier libs/ ou demarrage JVM) : "
        "reparer l'environnement (cf. Tweety-01-Setup-Python) avant de relancer."
    )

import jpype
from jpype.types import JObject

from org.tweetyproject.logics.commons.syntax import Predicate
from org.tweetyproject.logics.fol.syntax import FolSignature, FolFormula
from org.tweetyproject.logics.ml.syntax import MlBeliefSet
from org.tweetyproject.logics.ml.parser import MlParser

_parser_probe = MlParser()
print("Module modal Tweety charge :", _parser_probe.getClass().getName())

--- Initialisation Tweety ---
Bibliotheques natives: native/
JVM demarree avec 42 JARs.
Module modal Tweety charge : org.tweetyproject.logics.ml.parser.MlParser

Lecture : l’environnement est réel, pas simulé

La sortie atteste trois choses : le JDK est résolu (portable ou JAVA_HOME), la JVM démarre sur tous les JARs du dossier libs/, et le module org.tweetyproject.logics.ml — le calcul modal de Tweety — est chargé dans la JVM.

Un point de méthode avant d’aller plus loin : le notebook 3 (section 2.4) documente pourquoi le raisonneur modal de Tweety ne rend aucun verdict — SPASSMlReasoner produit une syntaxe DFG invalide (bug upstream Issue #1334). Ce labo ne contourne pas le bug par une sortie fabriquée : il change d’étage. La vérité modale ne vient pas d’un prover externe mais de la sémantique elle-même — d’abord énumérée en Python, puis certifiée par le noyau Lean. Le parser Tweety garde son rôle exact : donner la syntaxe.

2. La syntaxe : Tweety manipule les quatre schémas

Les quatre schémas d’axiomes qui structurent le spectre modal, dans la syntaxe de Tweety ([] = nécessité, <> = possibilité, => = implication) :

Schéma	Lecture	Syntaxe Tweety	Ce qu’il exigera du cadre
K	distribution : le nécessaire distribute sur l’implication	`[](p => q) => ([]((p)) => []((q)))`	rien — validité gratuite
T	ce qui est nécessaire est vrai	`[]((p)) => (p)`	réflexivité
4	le nécessaire est nécessairement nécessaire	`[]((p)) => []([]((p)))`	transitivité
5	le possible est nécessairement possible	`<>((p)) => [](<>((p)))`	euclidianité

Convention syntaxique Tweety : une formule nue sous modalité se parenthèse — []p s’écrit []((p)). Le parser rejette []p à l’intérieur d’une formule composée (« missing parentheses around modalized formula ») ; les composées comme [](q && r) passent telles quelles.

# --- Les quatre schemas d'axiomes parses par Tweety (contrat : 4/4) ---
sig_ml = FolSignature()
for nom in ("p", "q"):
    sig_ml.add(Predicate(nom, 0))

parser_ml = MlParser()
parser_ml.setSignature(sig_ml)

schemas_tweety = [
    ("K : normalite (distribution)",    "[](p => q) => ([]((p)) => []((q)))"),
    ("T : reflexivite ([]p => p)",      "[]((p)) => (p)"),
    ("4 : transitivite ([]p => [][]p)", "[]((p)) => []([]((p)))"),
    ("5 : euclideanite (<>p => []<>p)", "<>((p)) => [](<>((p)))"),
]

kb_ml = MlBeliefSet()
print("Parsing des quatre schemas d'axiomes :")
for etiquette, source in schemas_tweety:
    try:
        f = parser_ml.parseFormula(source)
    except Exception as e:
        # le labo porte sur CES quatre formules : un echec de parsing est bloquant
        raise RuntimeError(f"parseFormula a echoue pour {source!r} : {e}")
    kb_ml.add(JObject(f, FolFormula))
    print(f"  [OK] {etiquette}")
    print(f"       source      : {source}")
    print(f"       rendu Tweety: {f}")
print(f"\nKB modale : {kb_ml.size()} formules syntaxiques chargees.")

Parsing des quatre schemas d'axiomes :
  [OK] K : normalite (distribution)
       source      : [](p => q) => ([]((p)) => []((q)))
       rendu Tweety: ([]((p=>q))=>([](p)=>[](q)))
  [OK] T : reflexivite ([]p => p)
       source      : []((p)) => (p)
       rendu Tweety: ([](p)=>p)
  [OK] 4 : transitivite ([]p => [][]p)
       source      : []((p)) => []([]((p)))
       rendu Tweety: ([](p)=>[]([](p)))
  [OK] 5 : euclideanite (<>p => []<>p)
       source      : <>((p)) => [](<>((p)))
       rendu Tweety: (<>(p)=>[](<>(p)))

KB modale : 4 formules syntaxiques chargees.

Lecture : la structure est là, le verdict n’y est pas

Le rendu de Tweety — ([](p=>q)=>([](p)=>[](q))), (<>(p)=>[](<>(p)))… — montre l’arbre syntaxique complet : les nœuds []/<> sont des objets Java de première classe, inspectables, composables. C’est tout ce que le module ml de Tweety promet aujourd’hui : la manipulation.

Ce qui manque — et que le bug SPASS #1334 rend indisponible côté Tweety — est le verdict : cette formule est-elle valide ? Pour l’obtenir sans prover externe, on descend d’un étage abstrait : la sémantique. C’est l’objet de la section suivante, et le cœur du labo.

3. La sémantique : un moteur de Kripke en trente lignes de Python

Un cadre est un couple (W, R) — des mondes, une relation d’accessibilité. Un modèle ajoute une valuation V : les atomes vrais à chaque monde. Le forcing x satisfait f se définit récursivement ; les deux clauses qui font toute la modalité :

x satisfait []f   ssi   pour tout y tel que x R y :  y satisfait f
x satisfait <>f   ssi   il existe y tel que x R y :  y satisfait f

Deux choix d’implémentation méritent une ligne : les formules sont des dataclass gelées (immuables, hachables — un schéma peut servir de clé de dictionnaire) ; la relation est un frozenset de couples, jamais une matrice — pour énumérer tous les cadres de la section 4, un cadre n’est rien d’autre qu’un sous-ensemble d’arcs, et il se débite en bits.

# --- Moteur de Kripke : AST gelee + forcing recursif ---
from dataclasses import dataclass

@dataclass(frozen=True)
class Atome:    nom: str
@dataclass(frozen=True)
class Non:      f: object
@dataclass(frozen=True)
class Imp:      a: object; b: object
@dataclass(frozen=True)
class Et:       a: object; b: object
@dataclass(frozen=True)
class Boite:    f: object
@dataclass(frozen=True)
class Diamant:  f: object

@dataclass(frozen=True)
class Modele:
    mondes: tuple        # de mondes (entiers)
    relation: frozenset  # de couples (x, y) : x R y
    valuation: dict      # Atome.nom -> frozenset des mondes ou l'atome est vrai

    def successeurs(self, x):
        return frozenset(y for (a, y) in self.relation if a == x)

def satisfait(M, x, f):
    """Forcing x |= f -- la clause Boite est 'pour tout successeur', Diamant 'il existe'."""
    if isinstance(f, Atome):   return x in M.valuation[f.nom]
    if isinstance(f, Non):     return not satisfait(M, x, f.f)
    if isinstance(f, Imp):     return (not satisfait(M, x, f.a)) or satisfait(M, x, f.b)
    if isinstance(f, Et):      return satisfait(M, x, f.a) and satisfait(M, x, f.b)
    if isinstance(f, Boite):   return all(satisfait(M, y, f.f) for y in M.successeurs(x))
    if isinstance(f, Diamant): return any(satisfait(M, y, f.f) for y in M.successeurs(x))
    raise TypeError(f"formule inconnue : {f!r}")

def show(f):
    if isinstance(f, Atome):   return f.nom
    if isinstance(f, Non):     return "non " + show(f.f)
    if isinstance(f, Imp):     return f"({show(f.a)} -> {show(f.b)})"
    if isinstance(f, Et):      return f"({show(f.a)} et {show(f.b)})"
    if isinstance(f, Boite):   return "[]" + show(f.f)
    if isinstance(f, Diamant): return "<>" + show(f.f)

# Mini-test : le monde 0 voit le monde 1, p est vrai en 1 seulement.
m_test = Modele((0, 1), frozenset({(0, 1)}), {"p": frozenset({1})})
verdicts = {
    "p en 0":      satisfait(m_test, 0, Atome("p")),
    "[]p en 0":    satisfait(m_test, 0, Boite(Atome("p"))),
    "T en 0":      satisfait(m_test, 0, Imp(Boite(Atome("p")), Atome("p"))),
    "<>p en 1":    satisfait(m_test, 1, Diamant(Atome("p"))),
}
for etiquette, valeur in verdicts.items():
    print(f"  {etiquette:12s} : {'vrai' if valeur else 'faux'}")
assert verdicts["[]p en 0"] and not verdicts["T en 0"]
print("\nMoteur operationnel : monde mort (1 sans successeur), [] y est vacuement vrai.")

  p en 0       : faux
  []p en 0     : vrai
  T en 0       : faux
  <>p en 1     : faux

Moteur operationnel : monde mort (1 sans successeur), [] y est vacuement vrai.

Lecture : le monde mort et la vacuité

Le mini-test porte en germe tout le labo. Le monde 1 n’a aucun successeur : <>p y est faux (aucun témoin accessible) mais []p y est vacuément vrai — le all(...) sur un ensemble vide n’échoue jamais. C’est exact sur le plan mathématique (la clause [] quantifie universellement sur les successeurs : sans successeur, rien ne peut la contredire), et c’est un piège classique : un cadre rempli de mondes morts rend []f vrai partout sans rien dire de f.

La clause [] du moteur — all(satisfait(M, y, f.f) for y in M.successeurs(x)) — est aussi la ligne de jonction avec le versant certifiant : la preuve forces_kdist du pont Lean démontre la distribution en introduisant un successeur arbitraire puis en appliquant les deux hypothèses — littéralement le même « pour tout successeur », version type-théorie.

4. Le duel des témoins : trois cadres qui cassent T, 4, 5

La théorie de la correspondance prédit quel cadre falsifie quel schéma. Voici les trois témoins — minimaux, sur {0, 1} ou {0, 1, 2}, les autres mondes étant isolés. Ce sont les mêmes cadres que ceux définis et certifiés côté Lean par FormalLogic.ModalBridge : frameT, frame4, frame5 :

Témoin	Arcs	Condition violée	Schéma falsifié	Pourquoi ça marche
`frameT`	`0 -> 1`	réflexivité (0 ne se voit pas)	T	`[]p` vrai en 0 (le successeur 1 voit `p`), `p` faux en 0
`frame4`	`0 -> 1 -> 2` (pas `0 -> 2`)	transitivité	4	`[]p` vrai en 0, mais le successeur 1 voit le monde 2 sans `p` : `¬[]p` en 1 donc `¬[][]p` en 0
`frame5`	`0 -> 1`, `0 -> 2`	euclidianité (1 ne voit pas 2)	5	`<>p` vrai en 0 via 1, mais 2 est mort : `¬<>p` en 2, donc `¬[]<>p` en 0

Et K ? La prédiction est qu’il survit partout — la distribution ne dit rien du cadre, elle est vraie parce que la clause [] quantifie uniformément sur les successeurs.

# --- Les trois temoins : verdicts au monde 0, asserts sur la diagonale ---
p, q = Atome("p"), Atome("q")

schemas = [
    ("K", Imp(Boite(Imp(p, q)), Imp(Boite(p), Boite(q)))),
    ("T", Imp(Boite(p), p)),
    ("4", Imp(Boite(p), Boite(Boite(p)))),
    ("5", Imp(Diamant(p), Boite(Diamant(p)))),
]

temoins = [
    ("frameT {0->1}",       Modele((0, 1), frozenset({(0, 1)}), {"p": frozenset({1}), "q": frozenset()})),
    ("frame4 {0->1->2}",    Modele((0, 1, 2), frozenset({(0, 1), (1, 2)}), {"p": frozenset({1}), "q": frozenset()})),
    ("frame5 {0->1, 0->2}", Modele((0, 1, 2), frozenset({(0, 1), (0, 2)}), {"p": frozenset({1}), "q": frozenset()})),
]
# q est faux partout dans les temoins : K est vrai pour TOUTE valuation de q
# (sa validite ne depend que de la clause pour-tout), la valuation minimale suffit.

print(f"Verdicts au monde 0 (vrai/FAUX) :\n")
print(f"{'Schema':8s}" + "".join(f"{nom:>22s}" for nom, _ in temoins))
for nom_s, sch in schemas:
    ligne = f"{nom_s:8s}"
    for _, M in temoins:
        valeur = satisfait(M, 0, sch)
        ligne += f"{('vrai' if valeur else 'FAUX'):>22s}"
    print(ligne)

# La diagonale : chaque temoin casse SON schema (parmi T/4/5).
assert not satisfait(temoins[0][1], 0, schemas[1][1]), "T doit etre falsifie sur frameT"
assert not satisfait(temoins[1][1], 0, schemas[2][1]), "4 doit etre falsifie sur frame4"
assert not satisfait(temoins[2][1], 0, schemas[3][1]), "5 doit etre falsifie sur frame5"
# K, lui, ne doit etre falsifie nulle part -- ni sur les temoins...
for _, M in temoins:
    for x in M.mondes:
        assert satisfait(M, x, schemas[0][1]), "K ne doit jamais etre falsifie"
print("\nAsserts passes : la diagonale est FAUX, K survit sur les trois temoins.")

Verdicts au monde 0 (vrai/FAUX) :

Schema           frameT {0->1}      frame4 {0->1->2}   frame5 {0->1, 0->2}
K                         vrai                  vrai                  vrai
T                         FAUX                  FAUX                  vrai
4                         vrai                  FAUX                  vrai
5                         FAUX                  FAUX                  FAUX

Asserts passes : la diagonale est FAUX, K survit sur les trois temoins.

Lecture : la diagonale exacte, et le survivant

La table rend la structure prédictive visible : chaque colonne-témoin porte exactement un FAUX — le schéma dont elle viole la condition de cadre. Aucun dégât collatéral : l’éventail de frame5 est non euclidien et non transitif, et pourtant il laisse 4 intact au monde 0 — chaque crime porte son nom, aucun témoin n’est un assassi à la chaîne.

Un cadre peut violer plusieurs conditions à la fois — frameT (0 ne se voit pas) est aussi non transitif tant que 0 -> 1 -> 0 manque, et la table le montre : T casse, 4 tient. C’est la force du protocole : on falsifie un schéma à la fois, avec le cadre minimal qui ne viole que sa condition.

Et K vit partout — sur ces trois cadres. Trois cadres ne sont pas une preuve : c’est un sondage directionnel. La section suivante remplace le choix guidé par l’épuisement.

# --- Balayage exhaustif : TOUS les cadres a 3 mondes, TOUTES les valuations ---
def tous_cadres(n):
    arcs = [(x, y) for x in range(n) for y in range(n)]
    for masque in range(2 ** (n * n)):
        yield frozenset(a for i, a in enumerate(arcs) if masque >> i & 1)

def est_reflexive(R, n):   return all((x, x) in R for x in range(n))
def est_transitive(R, n):  return all((x, z) in R for x in range(n) for y in range(n)
                                      for z in range(n) if (x, y) in R and (y, z) in R)
def est_euclidienne(R, n): return all((y, z) in R for x in range(n) for y in range(n)
                                      for z in range(n) if (x, y) in R and (x, z) in R)

def falsifiable(sch, R, n, atomes):
    """Existe-t-il une valuation et un monde falsifiant le schema sur CE cadre ?"""
    monde_taille = 2 ** n
    for vmask_p in range(monde_taille if "p" in atomes else 1):
        for vmask_q in range(monde_taille if "q" in atomes else 1):
            V = {}
            if "p" in atomes: V["p"] = frozenset(w for w in range(n) if vmask_p >> w & 1)
            if "q" in atomes: V["q"] = frozenset(w for w in range(n) if vmask_q >> w & 1)
            M = Modele(tuple(range(n)), R, V)
            if any(not satisfait(M, x, sch) for x in range(n)):
                return True
    return False

N = 3
cadres3 = list(tous_cadres(N))
print(f"Balayage exhaustif : {len(cadres3)} cadres a {N} mondes "
      f"(2^{N * N} sous-ensembles d'arcs), toutes valuations.\n")

falsif = {nom: {R for R in cadres3 if falsifiable(sch, R, N, ("p", "q") if nom == "K" else ("p",))}
          for nom, sch in schemas}

familles = {
    "non reflexifs":  {R for R in cadres3 if not est_reflexive(R, N)},
    "non transitifs": {R for R in cadres3 if not est_transitive(R, N)},
    "non euclidiens": {R for R in cadres3 if not est_euclidienne(R, N)},
}
for nom, ensemble in familles.items():
    print(f"  {nom:16s}: {len(ensemble):3d} cadres")
print()
predications = [
    ("K", falsif["K"], set(),                      "aucun cadre"),
    ("T", falsif["T"], familles["non reflexifs"],  "les non reflexifs"),
    ("4", falsif["4"], familles["non transitifs"], "les non transitifs"),
    ("5", falsif["5"], familles["non euclidiens"], "les non euclidiens"),
]
for nom, ens, attendu, etiquette in predications:
    verdict = "EGALITE EXACTE" if ens == attendu else "DIVERGENCE"
    print(f"  {nom} falsifiable sur {len(ens):3d} cadres  [{verdict} avec {etiquette}]")
    assert ens == attendu, f"la correspondance de {nom} echoue sur les cadres 3-mondes"

print("\nCorrespondance verifiee par enumeration : T <-> reflexif, 4 <-> transitif, "
      "5 <-> euclidien, K <-> rien (jamais falsifiable).")

Balayage exhaustif : 512 cadres a 3 mondes (2^9 sous-ensembles d'arcs), toutes valuations.

  non reflexifs   : 448 cadres
  non transitifs  : 341 cadres
  non euclidiens  : 473 cadres

  K falsifiable sur   0 cadres  [EGALITE EXACTE avec aucun cadre]
  T falsifiable sur 448 cadres  [EGALITE EXACTE avec les non reflexifs]
  4 falsifiable sur 341 cadres  [EGALITE EXACTE avec les non transitifs]
  5 falsifiable sur 473 cadres  [EGALITE EXACTE avec les non euclidiens]

Correspondance verifiee par enumeration : T <-> reflexif, 4 <-> transitif, 5 <-> euclidien, K <-> rien (jamais falsifiable).

Lecture : la correspondance émerge du comptage — et s’arrête au bord du comptage

Sur les 512 cadres à 3 mondes, chaque égalité exacte est une donnée mesurée, pas un slogan : T falsifiable sur exactement les cadres non réflexifs, 4 sur les non transitifs, 5 sur les non euclidiens, et K sur aucun des 512 — la normalité est gratuite, elle ne négocie jamais avec la forme du cadre.

Mais l’énumération a un bord, et il faut le nommer : elle ne dit rien des cadres à 4 mondes et plus, rien des cadres infinis, rien des cadres non dénombrables. L’égalité constatée ici est une correspondance à cette taille — le pas vers « pour tout cadre » est un pas infini, et il exige une preuve, pas un sondage de plus. C’est précisément ce que la section suivante achète : un théorème Lean vaut pour tous les cadres de l’Archive — les 512, les cadres à un million de mondes, les infinis — d’une seule dérivation vérifiée par le noyau.

5. Le versant certifiant : le lake `formal_logic_lean`

Le corps de certification vit dans le lake sibling de la série : Lean/formal_logic_lean, qui consomme au pin exact deux corpus modaux :

ModalLogicArchive.Modal.Kripke — cadres génériques, sans aucune contrainte : le bon substrat pour falsifier T, 4, 5 et prouver K ;
Fin74.Kripke — cadres réflexifs et transitifs par construction (rel_refl et rel_trans sont des champs de données) : S4 par hypothèse du type, pas par axiome.

Le pont FormalLogic.ModalBridge (Tranche C de l’EPIC #15066, livré par #17017) y définit les cadres témoins — frameT, frame4, frame5, les mêmes arcs que la section 4 — et les certifie. Le protocole avant toute certification, hérité du labo FOL :

provenance mesurée : git rev-parse dans .lake/packages confronté au lake-manifest.json — on certifie ces sources, pas un souvenir ;
build réel : lake build FormalLogic.ModalBridge doit être vert, idempotent, sans sorry ;
alors seulement : #check / #print axioms dans un scratch vérifié par le noyau.

# --- Helpers WSL + nettoyage des chemins + provenance mesuree + build du module ---
import json
import shutil
import subprocess
import tempfile

# Lake du depot, sibling de la serie Tweety
LAKE_DIR = (TWEETY_DIR.parent / "Lean" / "formal_logic_lean").resolve()
assert (LAKE_DIR / "lakefile.lean").is_file(), f"lake introuvable : {LAKE_DIR}"

def to_wsl(p):
    """Chemin Windows -> chemin WSL /mnt/..."""
    win = p.resolve().as_posix()
    return "/mnt/" + win[0].lower() + win[2:]

def run_wsl(command, timeout):
    """Commande dans WSL, echec explicite si le binaire manque (patron Tweety-5e)."""
    if shutil.which("wsl") is None:
        raise RuntimeError(
            "les certificats Lean passent par WSL (`wsl -e bash -lc`) : binaire "
            "`wsl` introuvable. Les sections 5-6 exigent un hote Windows + WSL."
        )
    return subprocess.run(
        ["wsl", "-e", "bash", "-lc", command],
        capture_output=True, text=True, encoding="utf-8", errors="replace",
        timeout=timeout,
    )

def clean(texte):
    """Neutralise les chemins machine (formes Windows et WSL) dans les sorties :
    le source nettoie ses propres sorties -- aucune edition a la main des outputs."""
    substitutions = [
        (str(LAKE_DIR), "<repo>/Lean/formal_logic_lean"),
        (str(LAKE_DIR).replace("\\", "/"), "<repo>/Lean/formal_logic_lean"),
        (to_wsl(LAKE_DIR), "<repo>/Lean/formal_logic_lean"),
        (str(TWEETY_DIR), "<repo>/Tweety"),
        (to_wsl(TWEETY_DIR), "<repo>/Tweety"),
    ]
    for forme_cible, forme_portable in sorted(substitutions, key=lambda t: -len(t[0])):
        texte = texte.replace(forme_cible, forme_portable)
    return texte

# 1) Provenance mesuree : pins git REELS vs lake-manifest.json (mesure, pas declaration)
manifest = json.loads((LAKE_DIR / "lake-manifest.json").read_text(encoding="utf-8"))
pins_attendus = {p["name"]: p["rev"] for p in manifest["packages"]}
print("Provenance mesuree (git rev-parse dans .lake/packages) :")
for pkg in ["mathlib", "ModalLogic", "Foundation"]:
    r = run_wsl(f"git -C {to_wsl(LAKE_DIR)}/.lake/packages/{pkg} rev-parse HEAD", timeout=120)
    mesure = (r.stdout or "").strip()
    if r.returncode != 0 or not mesure:
        raise RuntimeError(
            f"package {pkg} illisible dans .lake/packages (exit {r.returncode}) : "
            f"construire le lake (lake exe cache get && lake build) avant d'executer "
            f"ce notebook -- aucun contournement (regle F)."
        )
    statut = "pin confirme" if mesure == pins_attendus[pkg] else "DERIVE"
    print(f"  {pkg:<12s} {mesure[:12]}  [{statut}]")
    assert mesure == pins_attendus[pkg], f"{pkg} a derive : {mesure[:12]}"

# 2) Build cible : le module du pont doit compiler sur ces sources (idempotent)
r = run_wsl(f"cd {to_wsl(LAKE_DIR)} && lake build FormalLogic.ModalBridge", timeout=1800)
sortie = clean((r.stdout or "") + (r.stderr or ""))
print("\n$ lake build FormalLogic.ModalBridge")
print("\n".join(sortie.strip().splitlines()[-3:]))
assert r.returncode == 0, "lake build FormalLogic.ModalBridge a echoue -- voir sortie ci-dessus"
print("\nBUILD OK : le module du pont compile sans aucun sorry.")

Provenance mesuree (git rev-parse dans .lake/packages) :
  mathlib      0df444a360ea  [pin confirme]
  ModalLogic   71968137b917  [pin confirme]
  Foundation   81810b9f22c4  [pin confirme]

$ lake build FormalLogic.ModalBridge
Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
Build completed successfully (1021 jobs).
warning: ModalLogic: repository '<repo>/Lean/formal_logic_lean/.lake/packages/ModalLogic' has local changes

BUILD OK : le module du pont compile sans aucun sorry.

Lecture : pins mesurés, build réel

Trois packages structurants sont confrontés au manifest : mathlib (l’infra de preuve), ModalLogic (le fork qui porte l’Archive — cadres génériques — au pin exact que le pont cite), Foundation (le corpus FFL). Chaque [pin confirme] est une mesure git rev-parse, pas une déclaration du lakefile ; un DERIVE arrêterait le notebook.

Le build cible est idempotent : sur un lake déjà construit il ne ré-élabore rien — la sortie le montre. C’est la propriété qui rend le labo exécutable en une session de cours : la première construction coûte, les suivantes vérifient.

Une note sur clean() : les sorties des helpers (warnings lake, erreurs lean) peuvent contenir des chemins absolus de la machine hôte ; le source les neutralise avant affichage — le notebook rendu reste portable sans qu’aucune sortie ne soit jamais éditée à la main.

# --- Tour d'API : #check des objets reels du pont, verifies par le kernel ---
def run_lean(source):
    """Ecrit source dans un temporaire et le fait verifier par le kernel Lean
    natif du lake (lake env lean = toolchain + LEAN_PATH du pin).
    Sortie nettoyee de tout chemin machine (clean)."""
    d = pathlib.Path(tempfile.mkdtemp(prefix="tweety3b_"))
    f = d / "scratch.lean"
    f.write_text(source, encoding="utf-8")
    r = run_wsl(f"cd {to_wsl(LAKE_DIR)} && lake env lean {to_wsl(f)}", timeout=1800)
    sortie = clean((r.stdout or "") + (r.stderr or ""))
    sortie = sortie.replace(to_wsl(d), "scratch").replace(str(d), "scratch")
    return sortie, r.returncode

api_tour = """import FormalLogic.ModalBridge

-- La normalite, valide sur tout cadre generique
#check @FormalLogic.ModalBridge.forces_kdist

-- Les trois temoins de la section 4, construits cote Lean
#check @FormalLogic.ModalBridge.frameT
#check @FormalLogic.ModalBridge.modelT
#check @FormalLogic.ModalBridge.T_invalid
#check @FormalLogic.ModalBridge.frame4
#check @FormalLogic.ModalBridge.model4
#check @FormalLogic.ModalBridge.four_invalid
#check @FormalLogic.ModalBridge.frame5
#check @FormalLogic.ModalBridge.model5
#check @FormalLogic.ModalBridge.five_invalid

-- Les duaux diamant sur les cadres S4 (Fin74)
#check @FormalLogic.ModalBridge.forces_dia_of_refl
#check @FormalLogic.ModalBridge.forces_dia_dia
"""

out, rc = run_lean(api_tour)
print("$ lake env lean scratch.lean")
print(out)
print(f"[exit {rc}]")
assert rc == 0, "le tour d'API doit compiler sans erreur"

$ lake env lean scratch.lean
@FormalLogic.ModalBridge.forces_kdist : ∀ {M : LO.Modal.Kripke.Model} {x : M.World} {φ ψ : LO.Modal.Formula ℕ},
  x ⊧ □(φ 🡒 ψ) → x ⊧ □φ → x ⊧ □ψ
FormalLogic.ModalBridge.frameT : LO.Modal.Kripke.Frame
FormalLogic.ModalBridge.modelT : LO.Modal.Kripke.Model
FormalLogic.ModalBridge.T_invalid : ¬LO.Modal.Formula.Kripke.Satisfies FormalLogic.ModalBridge.modelT 0
    (□LO.Modal.Formula.atom 0 🡒 LO.Modal.Formula.atom 0)
FormalLogic.ModalBridge.frame4 : LO.Modal.Kripke.Frame
FormalLogic.ModalBridge.model4 : LO.Modal.Kripke.Model
FormalLogic.ModalBridge.four_invalid : ¬LO.Modal.Formula.Kripke.Satisfies FormalLogic.ModalBridge.model4 0
    (□LO.Modal.Formula.atom 0 🡒 □□LO.Modal.Formula.atom 0)
FormalLogic.ModalBridge.frame5 : LO.Modal.Kripke.Frame
FormalLogic.ModalBridge.model5 : LO.Modal.Kripke.Model
FormalLogic.ModalBridge.five_invalid : ¬LO.Modal.Formula.Kripke.Satisfies FormalLogic.ModalBridge.model5 0
    (◇LO.Modal.Formula.atom 0 🡒 □◇LO.Modal.Formula.atom 0)
@FormalLogic.ModalBridge.forces_dia_of_refl : ∀ {κ : Type} {M : Model κ ℕ} {x : Frame.World} {A : Formula ℕ},
  x ⊩[M] A → x ⊩[M] ◇A
@FormalLogic.ModalBridge.forces_dia_dia : ∀ {κ : Type} {M : Model κ ℕ} {x : Frame.World} {A : Formula ℕ},
  x ⊩[M] ◇◇A → x ⊩[M] ◇A
warning: ModalLogic: repository '<repo>/Lean/formal_logic_lean/.lake/packages/ModalLogic' has local changes

[exit 0]

Lecture : chaque ligne est une vérification de type par le noyau

Le #check n’est pas de la documentation — c’est le noyau Lean qui type chaque identifiant dans l’environnement du lake : l’existence des cadres, des modèles et des sept résultats du pont est constatée, pas crue sur parole.

Deux types méritent une lecture lente :

forces_kdist — un théorème quantifié sur tout modèle générique M, tout monde x, toutes formules : c’est le « K jamais falsifié sur aucun des 512 cadres » de la section 4, promu à tous les cadres qui existent ;
T_invalid — une négation de satisfiabilité : le noyau a vérifié que la formule échoue dans le modèle témoin — la contre-partie exacte du FAUX de la diagonale Python, au monde 0 du même cadre {0 -> 1}.

# --- Certificat 1 : K valide sur TOUT cadre -- le sondage devient un theoreme ---
cert1 = """import FormalLogic.ModalBridge

-- La normalite : le "jamais falsifie sur 512 cadres" de la section 4 devient un theoreme
-- pour TOUT cadre -- les 512, les infinis, les non denombrables.
#print axioms FormalLogic.ModalBridge.forces_kdist

-- Reutilisation : dans n'importe quel modele de l'Archive, la distribution se derouve
-- par deux modus ponens sur la clause pour-tout -- le meme raisonnement que le moteur Python.
example {M : LO.Modal.Kripke.Model} {x : M.World} {phi psi : LO.Modal.Formula Nat}
    (hpq : x ⊧ □(phi 🡒 psi)) (hp : x ⊧ □phi) : x ⊧ □psi :=
  FormalLogic.ModalBridge.forces_kdist hpq hp
"""

out, rc = run_lean(cert1)
print("$ lake env lean scratch.lean")
print(out)
print(f"[exit {rc}]")
assert rc == 0 and "sorry" not in out, "le certificat 1 doit compiler sans sorry"
print("CERTIFICAT 1 : K est un theoreme sur tout cadre generique.")

$ lake env lean scratch.lean
'FormalLogic.ModalBridge.forces_kdist' does not depend on any axioms
warning: ModalLogic: repository '<repo>/Lean/formal_logic_lean/.lake/packages/ModalLogic' has local changes

[exit 0]
CERTIFICAT 1 : K est un theoreme sur tout cadre generique.

Lecture : un théorème en une ligne — et zéro axiome au-delà de Lean

#print axioms forces_kdist répond les trois axiomes de fondation de Lean (propext, Classical.choice, Quot.sound) — rien d’autre : aucun axiome modal, aucun sorry. La distribution n’est pas axiomatisée, elle est dérivée de la seule clause « pour tout successeur ».

La ligne example fait plus que rejouer : elle réutilise le théorème dans un contexte ouvert — n’importe quel modèle M de l’Archive, n’importe quel monde x. C’est la différence d’échelle entre les deux versants du labo :

le balayage Python a constaté K sur 512 cadres — un sondage parfait mais fini ;
le noyau Lean le démontre sur tout modèle — un théorème, d’une seule ligne, vérifiable mécaniquement en quelques secondes.

# --- Certificat 2 : T, 4, 5 -- les FAUX deviennent des contre-modeles kernel-verifies ---
cert2 = """import FormalLogic.ModalBridge

-- Les trois cadres temoins du labo Python (section 4), construits et verifies par le noyau.
#check @FormalLogic.ModalBridge.frameT
#check @FormalLogic.ModalBridge.modelT
#check @FormalLogic.ModalBridge.frame4
#check @FormalLogic.ModalBridge.model4
#check @FormalLogic.ModalBridge.frame5
#check @FormalLogic.ModalBridge.model5

-- Chaque non-validite est une preuve d'EXISTENCE d'un contre-modele.
#print axioms FormalLogic.ModalBridge.T_invalid
#print axioms FormalLogic.ModalBridge.four_invalid
#print axioms FormalLogic.ModalBridge.five_invalid
"""

out, rc = run_lean(cert2)
print("$ lake env lean scratch.lean")
print(out)
print(f"[exit {rc}]")
assert rc == 0 and "sorry" not in out, "le certificat 2 doit compiler sans sorry"
print("CERTIFICAT 2 : les trois FAUX de la diagonale sont des contre-modeles certifies.")

$ lake env lean scratch.lean
FormalLogic.ModalBridge.frameT : LO.Modal.Kripke.Frame
FormalLogic.ModalBridge.modelT : LO.Modal.Kripke.Model
FormalLogic.ModalBridge.frame4 : LO.Modal.Kripke.Frame
FormalLogic.ModalBridge.model4 : LO.Modal.Kripke.Model
FormalLogic.ModalBridge.frame5 : LO.Modal.Kripke.Frame
FormalLogic.ModalBridge.model5 : LO.Modal.Kripke.Model
'FormalLogic.ModalBridge.T_invalid' does not depend on any axioms
'FormalLogic.ModalBridge.four_invalid' does not depend on any axioms
'FormalLogic.ModalBridge.five_invalid' depends on axioms: [propext, Classical.choice, Quot.sound]
warning: ModalLogic: repository '<repo>/Lean/formal_logic_lean/.lake/packages/ModalLogic' has local changes

[exit 0]
CERTIFICAT 2 : les trois FAUX de la diagonale sont des contre-modeles certifies.

Lecture : « non validité » est une preuve d’existence, pas une absence

Chaque #print axioms sur un _invalid ne rend que les axiomes de fondation — les réfutations sont définies, pas supposées : le noyau a vérifié terme à terme que modelT falsifie T au monde 0, model4 falsifie 4, model5 falsifie 5.

La symétrie avec la section 4 est totale, et c’est le point pédagogique central du labo : les cadres sont les mêmes maths des deux côtés —

Côté Python (section 4)	Côté Lean (ce certificat)
`Modele((0,1), {(0,1)}, p={1})` — `T` FAUX en 0	`modelT` (relation « 0 voit 1 seulement ») — `T_invalid`
chaîne `{0->1, 1->2}` sans `0->2` — `4` FAUX en 0	`frame4` (même chaîne) — `four_invalid`
éventail `{0->1, 0->2}` — `5` FAUX en 0	`frame5` (même éventail) — `five_invalid`

Une falsification Python est un exemple calculé ; la réfutation Lean est le même exemple reconstruit comme terme et revérifié par le noyau. L’énumération avait trouvé les aiguilles ; le certificat prouve qu’elles existent.

# --- Certificat 3 : cadres S4 -- la structure DONNE les duaux diamant ---
cert3 = """import FormalLogic.ModalBridge

-- Sur les cadres Fin74, reflexivite et transitivite sont des CHAMPS du cadre (donnees),
-- pas des hypotheses : les duaux diamant s'y derivent en une ligne chacun.
#print axioms FormalLogic.ModalBridge.forces_dia_of_refl
#print axioms FormalLogic.ModalBridge.forces_dia_dia

-- DUAL DE T : le temoin du diamant, c'est le monde lui-meme (reflexivite).
example {kappa : Type} {M : Model kappa Nat} {x : M.World} {A : Formula Nat}
    (h : x ⊩ A) : x ⊩ ◇A :=
  FormalLogic.ModalBridge.forces_dia_of_refl h

-- DUAL DE 4 : la transitivite raccourcit la double mediation.
example {kappa : Type} {M : Model kappa Nat} {x : M.World} {A : Formula Nat}
    (h : x ⊩ ◇◇A) : x ⊩ ◇A :=
  FormalLogic.ModalBridge.forces_dia_dia h

-- COMPOSITION : le temoin de A est son propre temoin de double diamant.
example {kappa : Type} {M : Model kappa Nat} {x : M.World} {A : Formula Nat}
    (hA : x ⊩ A) : x ⊩ ◇◇A := by
  obtain ⟨y, xy, hy⟩ := FormalLogic.ModalBridge.forces_dia_of_refl hA
  exact ⟨y, xy, FormalLogic.ModalBridge.forces_dia_of_refl hy⟩
"""

out, rc = run_lean(cert3)
print("$ lake env lean scratch.lean")
print(out)
print(f"[exit {rc}]")
assert rc == 0 and "sorry" not in out, "le certificat 3 doit compiler sans sorry"

# Miroir Python : cloture reflexive-transitive de {0, 1} -- les memes duaux y sont valides.
m_s4 = Modele((0, 1), frozenset({(0, 0), (0, 1), (1, 1)}),
              {"p": frozenset({0}), "q": frozenset({1})})
print("\nMiroir Python sur la cloture reflexive-transitive {0, 1} :")
for x in m_s4.mondes:
    dual_t = satisfait(m_s4, x, Imp(Atome("p"), Diamant(Atome("p"))))
    dual_4 = satisfait(m_s4, x, Imp(Diamant(Diamant(Atome("q"))), Diamant(Atome("q"))))
    print(f"  monde {x} : A -> <>A {'vrai' if dual_t else 'FAUX'} | "
          f"<><>A -> <>A {'vrai' if dual_4 else 'FAUX'}")
    assert dual_t and dual_4, "un dual casse sur la cloture S4 ?!"
print("CERTIFICAT 3 : duaux diamant cote Fin74, verifies cote Python sur la cloture S4.")

$ lake env lean scratch.lean
'FormalLogic.ModalBridge.forces_dia_of_refl' does not depend on any axioms
'FormalLogic.ModalBridge.forces_dia_dia' does not depend on any axioms
warning: ModalLogic: repository '<repo>/Lean/formal_logic_lean/.lake/packages/ModalLogic' has local changes

[exit 0]

Miroir Python sur la cloture reflexive-transitive {0, 1} :
  monde 0 : A -> <>A vrai | <><>A -> <>A vrai
  monde 1 : A -> <>A vrai | <><>A -> <>A vrai
CERTIFICAT 3 : duaux diamant cote Fin74, verifies cote Python sur la cloture S4.

Lecture : la structure du cadre donne les théorèmes

Le glissement d’échelle est ici le plus conceptuel du labo : dans l’Archive, réflexivité et transitivité sont des propriétés qu’un cadre peut avoir ou non — on les falsifie (section 4). Dans Fin74, elles sont des champs de données (rel_refl, rel_trans) : un cadre Fin74 est réflexif et transitif par construction, comme un groupe est associatif. Le théorème A -> <>A ne se gagne pas, il se lit sur la forme du type — forces_dia_of_refl tient en une ligne : le témoin du diamant, c’est le monde lui-même.

La contre-vérification Python referme la boucle : sur la clôture réflexive-transitive de {0, 1} — deux mondes, trois arcs — les deux duaux sont valides aux deux mondes. Ce n’est pas une preuve (c’en est une pour ce cadre seulement), c’est le témoin calculé du théorème certifié — la même asymétrie féconde que pour K.

6. Bilan croisé : trois lectures, une seule sémantique

Schéma	Tweety (section 2)	Énumération ≤ 3 mondes (section 4)	Kernel Lean (section 5)
K	arbre syntaxique chargé	jamais falsifié — 0/512	`forces_kdist` : théorème sur tout cadre
T	idem	falsifiable sur les non réflexifs, exactement	`T_invalid` : contre-modèle `frameT` certifié
4	idem	falsifiable sur les non transitifs, exactement	`four_invalid` : contre-modèle `frame4`
5	idem	falsifiable sur les non euclidiens, exactement	`five_invalid` : contre-modèle `frame5`
duaux S4	—	valides sur la clôture réflexive-transitive (témoin)	théorèmes via `rel_refl`/`rel_trans` (champs)

Les trois colonnes ne sont pas trois vérités concurrentes mais trois statuts épistémiques du même énoncé :

manipuler — Tweety donne la syntaxe ; le bug SPASS #1334 y fixe un plafond upstream ;
constater — l’énumération épuise un fragment fini et y mesure des égalités exactes ;
prouver — le noyau transforme les constats en théorèmes (tout cadre) ou en réfutations par contre-modèle reconstruit.

La chaîne est composable : c’est parce que le moteur Python et le pont Lean parlent des mêmes cadres ({0->1}, la chaîne, l’éventail) que chaque FAUX du comptage a pu devenir un _invalid certifié. C’est la méthode générale des labos croisés de l’EPIC.

Exercice 1 : le schéma `.2` — la confluence à l’épreuve du comptage

Contexte

Le spectre modal ne s’arrête pas à T/4/5. Le schéma .2 — <>[]p -> []<>p, « ce qui est possiblement nécessaire est nécessairement possible » — correspond à la confluence du cadre : deux successeurs d’un même monde ont toujours un successeur commun.

Objectifs

Définir .2 avec l’AST du moteur (Imp(Diamant(Boite(Atome("p"))), Boite(Diamant(Atome("p")))))
Construire à la main un cadre à 3 mondes non confluents qui falsifie .2 — prédire le monde et la valuation avant d’exécuter
Vérifier, puis confronter au verdict du balayage exhaustif : .2 doit être falsifiable exactement sur les cadres non confluents à 3 mondes

Indices : - deux successeurs sans point commun : l’éventail de frame5 est non confluent et non euclidien — mais un cadre confluent non euclidien existe aussi (ajoutez un monde commun atteignable) ; - pour la valuation : où []p doit-il être vrai pour nourrir <>[]p, et où <>p doit-il échouer ?

# --- Exercice 1 : le contre-modele de .2 (confluence) reste a exhiber ---
# TODO etudiant
# Etape 1 : point_deux = Imp(Diamant(Boite(Atome("p"))), Boite(Diamant(Atome("p"))))
# Etape 2 : construire un Modele 3-mondes NON confluent (deux successeurs d'un meme monde
#           sans successeur commun) et une valuation qui falsifie .2 -- predire AVANT d'executer
# Etape 3 : verifier avec satisfait(M, monde, point_deux), puis adapter le balayage de la
#           section 4 : la famille attendue est celle des cadres non confluents
resultat_ex1 = None  # TODO etudiant : (modele, monde_falsifiant) attendu
print("Exercice 1 a completer : le contre-modele de .2 (confluence) reste a exhiber.")

Exercice 1 a completer : le contre-modele de .2 (confluence) reste a exhiber.

Exercice 2 : le côté suffisant de la correspondance pour `T`

Contexte

Le balayage a établi le côté nécessaire : hors réflexivité, T casse. Le côté suffisant — réflexif rend T valide — se vérifie lui aussi par énumération, sur un fragment où l’exhaustivité reste triviale.

Objectifs

Énumérer les 16 cadres à 2 mondes (tous_cadres(2)) et balayer les valuations de p
Vérifier que T n’est falsifiable sur aucun des 4 cadres réflexifs — et compter les falsifications sur les 12 autres
Rédiger en une phrase ce que ce résultat 2-mondes ne prouve pas pour les cadres infinis — et nommer ce qui le prouve (indice : la section 5 l’a fait pour K)

Indices : - est_reflexive(R, 2) et falsifiable(T, R, 2, ("p",)) sont déjà définis ; - pour le point 3 : relisez la lecture du balayage — sondage fini contre théorème quantifié.

# --- Exercice 2 : validite de T sur les cadres reflexifs 2-mondes ---
# TODO etudiant
# Etape 1 : cadres2 = list(tous_cadres(2)) -- 16 cadres
# Etape 2 : pour chaque cadre reflexif, balayer les valuations (falsifiable(schemas[1][1], R, 2, ("p",)))
#           et verifier qu'aucune falsification n'apparait
# Etape 3 : compter les falsifications sur les cadres non reflexifs, et formuler la limite
#           du resultat (qu'est-ce que 2-mondes ne dit pas des cadres infinis ?)
resultat_ex2 = None  # TODO etudiant : (nb_reflexifs_sains, nb_falsifications_hors_reflexifs) attendu
print("Exercice 2 a completer : la validite de T sur les cadres reflexifs reste a verifier.")

Exercice 2 a completer : la validite de T sur les cadres reflexifs reste a verifier.

Exercice 3 : votre première composition de certificats

Contexte

Le certificat 3 a dérivé les duaux diamant comme applications directes. La composition A -> <><>A se déduit des mêmes briques appliquées deux fois — la médiation réflexive du témoin. C’est à vous de l’assembler.

Objectifs

Écrire un example prouvant A -> <><>A sur un cadre Fin74, en composant deux fois forces_dia_of_refl (le témoin de A est son propre témoin de <>)
Exécuter : verdict attendu [exit 0], aucun sorry dans la sortie
Variante (optionnelle) : <><>A -> <>A sur un cadre générique de l’Archive — possible sans transitivité ? Testez votre intuition, la réponse est dans la preuve de forces_kdist

Indices : - squelette : repartez de la cellule du certificat 3 — le troisième example y est presque mot pour mot la solution d’une autre formule ; identifiez laquelle avant d’écrire ; - obtain déstructure un diamant en (témoin, arc, forcing) ; - run_lean est déjà défini : out, rc = run_lean(ex3_lean) puis assert rc == 0.

# --- Exercice 3 : certificat Lean de A -> <><>A sur un cadre S4 ---
# TODO etudiant : remplacer le corps de ex3_lean par votre certificat.
# Etape 1 : partir de (hA : x satisfait A) : x satisfait <>A par forces_dia_of_refl
# Etape 2 : composer a nouveau : le temoin y de <>A verifie y satisfait A, donc y satisfait <>A
#           par reflexivite -- d'ou x satisfait <><>A
# Etape 3 : executer -- verdict attendu [exit 0], aucun sorry dans la sortie
ex3_lean = """import FormalLogic.ModalBridge
#check @FormalLogic.ModalBridge.forces_dia_of_refl  -- TODO etudiant : remplacer par l'example
"""
out_ex3, rc_ex3 = run_lean(ex3_lean)
print(out_ex3)
print(f"[exit {rc_ex3}]")
assert rc_ex3 == 0, "le squelette doit compiler ; l'exercice remplace le #check par l'example"
print("Exercice 3 a completer : le certificat A -> <><>A reste a ecrire.")

@FormalLogic.ModalBridge.forces_dia_of_refl : ∀ {κ : Type} {M : Model κ ℕ} {x : Frame.World} {A : Formula ℕ},
  x ⊩[M] A → x ⊩[M] ◇A
warning: ModalLogic: repository '<repo>/Lean/formal_logic_lean/.lake/packages/ModalLogic' has local changes

[exit 0]
Exercice 3 a completer : le certificat A -> <><>A reste a ecrire.

Conclusion

Ce labo a croisé trois moteurs de vérité sur le même zoo modal :

Tweety manipule : le MlParser charge les quatre schémas K/T/4/5 comme arbres Java inspectables — et le bug SPASS #1334 y fixe le plafond upstream : syntaxe sans verdict ;
l’énumération mesure : 512 cadres à 3 mondes, toutes valuations — la correspondance émerge comme des égalités exactes (T avec les non réflexifs, 4 avec les non transitifs, 5 avec les non euclidiens), et K sur aucun — un sondage parfait mais fini ;
Lean certifie : K devient un théorème pour tout cadre (forces_kdist), les trois FAUX deviennent des réfutations par contre-modèle reconstruit (T_invalid/four_invalid/ five_invalid — les mêmes cadres que le Python), et sur les cadres S4 Fin74 les duaux diamant se lisent dans les champs rel_refl/rel_trans — pins mathlib/ModalLogic/Foundation mesurés avant toute certification.

Points clés à retenir :

la validité modale est relative au cadre : []p -> p n’est ni vrai ni faux — il est vrai sur les cadres réflexifs, falsifié ailleurs ; une logique modale est un choix de conditions ;
monde mort n’est pas monde muet : []f y est vacuément vrai — le piège de la quantification universelle sur l’ensemble vide est au cœur de plusieurs contre-modèles ;
un sondage n’est pas une preuve : l’égalité exacte sur 512 cadres ne dit rien des cadres infinis ; le théorème Lean les couvre tous d’une dérivation — et réciproquement, la réfutation Lean n’est que l’existence d’un contre-modèle, que l’énumération avait déjà su trouver ;
la provenance se mesure : pins git rev-parse confrontés au manifest, build cible vert, avant d’invoquer le moindre certificat.

Références

TweetyProject — module modal et l’issue #1334 (bug SPASSWriter) ;
corpus ModalLogic (l’Archive des cadres génériques) et Fin74 (cadres S4 par construction), épinglés dans le lakefile de formal_logic_lean ;
EPIC #15066 — laboratoires croisés Tweety ↔︎ Lean (Tranche A : propositionnel #15520 ; Tranche B : FOL #16888 ; Tranche C : le pont #17017, que ce labo consomme) ;
Notebooks compagnons : Tweety-3 (le tour modale et le bug SPASS), Tweety-3c-ML (port C#/IKVM), Tweety-02d (labo FOL certifié, même patron).

Navigation : ← Tweety-3 (Advanced Logics) · Tweety-3c-ML (port C#) · Tweety-02d (labo FOL) · README

Retour au sommet

Objectifs pédagogiques

Prérequis

Durée estimée : 45 minutes

1. La question du labo

Lecture : l’environnement est réel, pas simulé

2. La syntaxe : Tweety manipule les quatre schémas

Lecture : la structure est là, le verdict n’y est pas

3. La sémantique : un moteur de Kripke en trente lignes de Python

Lecture : le monde mort et la vacuité

4. Le duel des témoins : trois cadres qui cassent T, 4, 5

Lecture : la diagonale exacte, et le survivant

Lecture : la correspondance émerge du comptage — et s’arrête au bord du comptage

5. Le versant certifiant : le lake formal_logic_lean

Lecture : pins mesurés, build réel

Lecture : chaque ligne est une vérification de type par le noyau

Lecture : un théorème en une ligne — et zéro axiome au-delà de Lean

Lecture : « non validité » est une preuve d’existence, pas une absence

Lecture : la structure du cadre donne les théorèmes

6. Bilan croisé : trois lectures, une seule sémantique

Exercice 1 : le schéma .2 — la confluence à l’épreuve du comptage

Contexte

Objectifs

Exercice 2 : le côté suffisant de la correspondance pour T

Contexte

Objectifs

Exercice 3 : votre première composition de certificats

Contexte

Objectifs

Conclusion

Références

5. Le versant certifiant : le lake `formal_logic_lean`

Exercice 1 : le schéma `.2` — la confluence à l’épreuve du comptage

Exercice 2 : le côté suffisant de la correspondance pour `T`