Tweety-5e — Laboratoire propositionnel : validité, preuve et contre-modèle

Navigation: ← Tweety-5d | Index | Tweety-2 | Lean-3 |

Ce notebook est le companion transversal de Tweety-2 (la pratique du raisonner propositionnel) et de Lean-3 (les preuves interactives) : il fait traverser à trois formules-témoins les quatre niveaux d’articulation décrits dans l’EPIC #15066 — tranche A (laboratoire propositionnel).

Objectifs pédagogiques

  1. Distinguer satisfiable, valide et prouvable — trois questions que le langage courant confond, sur les mêmes formules.
  2. Exécuter le raisonneur Tweety (SAT4J, mondes possibles) : il répond (OUI/NON, un témoin), il n’explique pas.
  3. Interroger les objets formels de Foundation (FFL) — la formalisation Formalized Formal Logic : Formula, valuations, axiomes classiques (Peirce, LEM) — et constater une limite du pin épinglé : le module de complétude de Tait n’y exporte aucune déclaration (section 3).
  4. Certifier dans le kernel Lean natif : un théorème prouvé sur toutes les valuations (pas seulement les 8 mondes énumérés), et un contre-modèle transporté — le témoin calculé par Tweety, revérifié par Lean.

Prérequis

  • Tweety-1-Setup exécuté (JVM, Tweety/libs).
  • Le pilote FFL Foundation cloné dans WSL au commit épinglé 21318c7ee3b608c10366da82c4208b0d38a07402 (la cellule de la section 3 vérifie et documente l’installation).

Durée estimée : 40 minutes

Outils — trois lectures d’une même formule

Lecture Outil Ce qu’il rend Ce qu’il ne rend pas
Exécution Tweety 1.28 via JPype (SAT4J) verdicts OUI/NON, modèles, contre-modèles calculés une preuve — le témoin, pas la raison
Contrôle croisé Python brut recomptage indépendant des mondes un moteur de raisonnement
Certification Lean 4 + Foundation (FFL) au commit épinglé des objets : Formula, val, IsTautology, Axioms.LEM un contre-modèle calculé — il vérifie ce qu’on lui transporte

Le couple (Tweety, Lean) est le motif établi par Tweety-5b (sémantique grounded certifiée) et Tweety-5d (Z3 → témoin → certificat) : calculer d’un côté, certifier de l’autre, et confronter les deux.

# --- Initialisation JVM Tweety ---
print("--- Verification JVM Tweety ---")
jvm_ready = False

import pathlib

import jpype

LIB_DIR = pathlib.Path("libs")
if not LIB_DIR.exists() or not list(LIB_DIR.glob("*.jar")):
    raise FileNotFoundError(
        "dossier libs/ introuvable -- executer le notebook depuis "
        "MyIA.AI.Notebooks/SymbolicAI/Tweety/ (voir Tweety-1-Setup)"
    )

jar_files = sorted(LIB_DIR.glob("*.jar"))
try:
    jpype.startJVM(classpath=[str(j) for j in jar_files], convertStrings=False)
    import jpype.imports
    jpype.imports.registerDomain("org")
    jvm_ready = True
    print(f"JVM demarree avec {len(jar_files)} JAR(s) : {[j.name for j in jar_files]}")
except Exception as e:
    print(f"Erreur demarrage JVM: {e}")
--- Verification JVM Tweety ---
JVM demarree avec 1 JAR(s) : ['org.tweetyproject.tweety-7a-java8-shade.jar']

Interprétation : ce qui tourne

La JVM charge le JAR shaded de Tweety (org.tweetyproject.tweety-7a-java8-shade.jar) — une distribution autonome. Deux pièges mesurés lors de la préparation de ce notebook :

  1. PlParser vit dans org.tweetyproject.logics.pl.**parser** (pas .syntax), et PossibleWorld dans .**semantics** ;
  2. satisfies est surchargé (PlFormula / Formula / Collection) : jpype exige un cast explicite JObject(f, PlFormula) — sans lui, TypeError: Ambiguous overloads.

1. Le fragment commun : trois formules-témoins

On fixe un fragment à trois atomes {a, b, c} (8 mondes possibles) et trois formules-témoins, une par verdict attendu :

Clé Formule Verdict attendu Ce qu’elle témoigne
SYL (a => b) => ((b => c) => (a => c)) valide (8/8) la transitivité de l’implication — un théorème
ORB a \|\| b satisfiable non valide (6/8) le contre-exemple : vrai souvent, pas toujours
CONTR a && !a insatisfiable (0/8) la contradiction — aucun monde ne la sauve

La syntaxe est partagée et sérialisable : la même chaine sert de source à Tweety (parsing JPype) et à l’émetteur Lean (traduction vers les constructeurs Formula de FFL).

# --- 1. Le fragment commun : trois formules-temoins ---
ATOMES = ["a", "b", "c"]

FORMULES = {
    "SYL": "(a => b) => ((b => c) => (a => c))",
    "ORB": "a || b",
    "CONTR": "a && !a",
}

# Emetteur Lean : traduit la syntaxe Tweety vers les constructeurs FFL.Formula
# sur alpha = Fin 3  (0 = a, 1 = b, 2 = c). Les operateurs FFL correspondants :
#   =>  devient  🡒 (imp)   ||  devient  ⋎ (or)   &&  devient  ⋏ (and)   !  devient  ∼ (neg)
def to_lean(formula: str) -> str:
    s = formula
    out, i = [], 0
    while i < len(s):
        if s.startswith("=>", i):
            out.append(" 🡒 ")
            i += 2
        elif s.startswith("||", i):
            out.append(" ⋎ ")
            i += 2
        elif s.startswith("&&", i):
            out.append(" ⋏ ")
            i += 2
        elif s[i] == "!":
            out.append("∼")
            i += 1
        elif s[i].isalpha():
            j = i
            while j < len(s) and s[j].isalpha():
                j += 1
            out.append(f"(.atom {ATOMES.index(s[i:j])})")
            i = j
        else:
            out.append(s[i])
            i += 1
    return "".join(out)

for k, f in FORMULES.items():
    print(f"{k:6s} tweety={f!r:40s} lean={to_lean(f)}")
SYL    tweety='(a => b) => ((b => c) => (a => c))'     lean=((.atom 0)  🡒  (.atom 1))  🡒  (((.atom 1)  🡒  (.atom 2))  🡒  ((.atom 0)  🡒  (.atom 2)))
ORB    tweety='a || b'                                 lean=(.atom 0)  ⋎  (.atom 1)
CONTR  tweety='a && !a'                                lean=(.atom 0)  ⋏  ∼(.atom 0)

Lecture : ce que chaque formule va révéler

  • SYL est le syllogisme hypothétique. Prédiction : les 8 mondes la satisfont. Si c’est vrai, ce n’est pas un hasard : une preuve existe, et la section 4 la construit dans Lean — sur toutes les valuations, y compris celles qu’aucune énumération finie ne visite.
  • ORB est le témoin du contre-exemple. Prédiction : 6 mondes la satisfont, 2 la falsifient. Ces deux mondes sont des contre-modèles calculés ; la section 5 en transporte un vers Lean.
  • CONTR est la contradiction. Prédiction : 0 monde. L’insatisfiabilité n’est pas « très difficile » : elle est totale.

Les prédictions sont écrites avant l’exécution : c’est elles qu’on va confronter aux trois lectures.

2. Première lecture : Tweety énumère les mondes

Le premier niveau est le plus simple à exécuter : demander au raisonneur. On énumère les \(2^3 = 8\) mondes possibles de la signature, on évalue chaque formule dans chaque monde, et on lit les verdicts — sans jamais demander pourquoi.

# --- 2. Premiere lecture : Tweety enumere les mondes ---
if not jvm_ready:
    raise RuntimeError("JVM Tweety non demarree (cellule d'initialisation)")

from jpype.types import JObject

PlFormula = jpype.JClass("org.tweetyproject.logics.pl.syntax.PlFormula")
from org.tweetyproject.logics.pl.parser import PlParser
from org.tweetyproject.logics.pl.semantics import PossibleWorld
from org.tweetyproject.logics.pl.syntax import PlSignature, Proposition

parser = PlParser()
sig = PlSignature()
for p in ATOMES:
    sig.add(Proposition(p))

worlds = PossibleWorld.getAllPossibleWorlds(sig)
print(f"Signature {{{', '.join(ATOMES)}}} : {len(worlds)} mondes possibles")

parsed = {k: parser.parseFormula(f) for k, f in FORMULES.items()}

# Table de verite : satisfaction de chaque formule dans chaque monde
world_strs = sorted(str(w) for w in worlds.iterator())
verdicts = {k: {} for k in parsed}  # world_str -> bool
for w in worlds.iterator():
    ws = str(w)
    for k, f in parsed.items():
        verdicts[k][ws] = bool(w.satisfies(JObject(f, PlFormula)))

print(f"{'monde':>10s} | " + " | ".join(f"{k:>5s}" for k in parsed))
for ws in world_strs:
    row = ["  1  " if verdicts[k][ws] else "  0  " for k in parsed]
    print(f"{ws:>10s} | " + " | ".join(row))

print()
for k in parsed:
    n = sum(1 for v in verdicts[k].values() if v)
    print(f"{k}: satisfaite dans {n}/{len(worlds)} mondes")
Signature {a, b, c} : 8 mondes possibles
     monde |   SYL |   ORB | CONTR
        [] |   1   |   0   |   0  
 [a, b, c] |   1   |   1   |   0  
    [a, b] |   1   |   1   |   0  
    [a, c] |   1   |   1   |   0  
       [a] |   1   |   1   |   0  
    [b, c] |   1   |   1   |   0  
       [b] |   1   |   1   |   0  
       [c] |   1   |   0   |   0  

SYL: satisfaite dans 8/8 mondes
ORB: satisfaite dans 6/8 mondes
CONTR: satisfaite dans 0/8 mondes

Interprétation : les trois verdicts côté exécution

Les comptes confirment les prédictions : 8/8, 6/8, 0/8. Trois états distincts, que le vocabulaire courant écrase dans un seul « vrai/faux » :

État Compte Lecture
valide 8/8 vrai dans tous les mondes — un théorème
satisfiable non valide 6/8 vrai dans certains — dépend du monde
insatisfiable 0/8 vrai dans aucun — contradiction

Et le contre-exemple est déjà là : les lignes 0 de ORB sont deux mondes calculés qui falsifient la formule. Un solveur ne les a pas « démontrés inexistants » : il les a trouvés.

# --- 2bis. Verdict SAT + contre-modele calcule + controle croise Python ---
from org.tweetyproject.logics.pl.reasoner import SimplePlReasoner

r = SimplePlReasoner()
empty_kb = parser.parseBeliefBase("")
print("--- Verdicts du raisonneur (KB vide : validite semantique) ---")
for k, f in parsed.items():
    print(f"{k}: le raisonneur dit 'valide' -> {bool(r.query(empty_kb, f))}")

# Contre-modeles calcules pour ORB (les lignes 0 de la table)
falsifiers = [ws for ws in world_strs if not verdicts["ORB"][ws]]
print(f"\nContre-modeles calcules de ORB : {falsifiers}")

# --- Controle croise : Python brut, ni Tweety ni Lean (troisieme lecture) ---
def parse_py(toks):
    """Analyseur descente recursive : implication (associee a droite) < ou < et < non < atome."""
    pos = 0

    def p_imp():
        nonlocal pos
        lhs = p_or()
        if pos < len(toks) and toks[pos] == "=>":
            pos += 1
            return ("imp", lhs, p_imp())
        return lhs

    def p_or():
        nonlocal pos
        lhs = p_and()
        while pos < len(toks) and toks[pos] == "||":
            pos += 1
            lhs = ("or", lhs, p_and())
        return lhs

    def p_and():
        nonlocal pos
        lhs = p_not()
        while pos < len(toks) and toks[pos] == "&&":
            pos += 1
            lhs = ("and", lhs, p_not())
        return lhs

    def p_not():
        nonlocal pos
        if pos < len(toks) and toks[pos] == "!":
            pos += 1
            return ("not", p_not())
        return p_atom()

    def p_atom():
        nonlocal pos
        t = toks[pos]
        pos += 1
        if t == "(":
            e = p_imp()
            assert toks[pos] == ")"
            pos += 1
            return e
        return ("atom", t)

    return p_imp()

def eval_py(ast, env):
    op = ast[0]
    if op == "atom":
        return env[ast[1]]
    if op == "not":
        return not eval_py(ast[1], env)
    if op == "and":
        return eval_py(ast[1], env) and eval_py(ast[2], env)
    if op == "or":
        return eval_py(ast[1], env) or eval_py(ast[2], env)
    return (not eval_py(ast[1], env)) or eval_py(ast[2], env)  # imp

def world_str_to_set(ws: str) -> set:
    inner = ws.strip("[]").strip()
    return set(inner.replace(" ", "").split(",")) - {""} if inner else set()

asts = {k: parse_py(f.replace("(", " ( ").replace(")", " ) ").replace("!", " ! ").split())
        for k, f in FORMULES.items()}
ok = True
for ws in world_strs:
    env = {a: (a in world_str_to_set(ws)) for a in ATOMES}
    for k in FORMULES:
        py = eval_py(asts[k], env)
        if py != verdicts[k][ws]:
            ok = False
            print(f"DIVERGENCE {k} sur monde {ws}: python={py} tweety={verdicts[k][ws]}")
print(f"\nControle croise Python/Tweety sur {len(world_strs)} mondes x {len(FORMULES)} formules : "
      f"{'CONVERGENT' if ok else 'DIVERGENT'}")
--- Verdicts du raisonneur (KB vide : validite semantique) ---
SYL: le raisonneur dit 'valide' -> True
ORB: le raisonneur dit 'valide' -> False
CONTR: le raisonneur dit 'valide' -> False

Contre-modeles calcules de ORB : ['[]', '[c]']

Controle croise Python/Tweety sur 8 mondes x 3 formules : CONVERGENT

Interprétation : le solveur répond, il n’explique pas

Le raisonneur (SAT4J sous le capot) rend les verdicts sémantiques : « valide → oui/non ». Trois lectures indépendantes (Tweety, recomptage Python brut, et bientôt Lean) convergent — c’est le contrôle croisé falsifiable exigé par l’EPIC : si l’une divergeait, le notebook tomberait en erreur plus loin.

Mais aucune de ces lectures ne dit pourquoi SYL est valide. « Je l’ai testé sur les 8 mondes » n’est pas une preuve — c’est un sondage. La différence devient explosive dès que le fragment grandit : à 30 atomes, l’énumération visite plus de \(10^9\) mondes ; à 100, plus que d’atomes dans l’univers visible. La preuve, elle, ne grandit pas avec le nombre de mondes : elle est un objet fini, vérifiable en temps borné. C’est ce que les sections 3–5 construisent.

3. Deuxième lecture : les objets formels de Foundation (FFL)

Le corpus Formalized Formal Logic formalise en Lean 4 les logiques elles-mêmes — syntaxe, sémantique, calculs, métathéorèmes. On interroge le dépôt Foundation, cloné dans WSL au commit épinglé 21318c7ee3b608c10366da82c4208b0d38a07402 (posture CONSUMER_PINNÉ : le pilote d’intégration — clone frais, lake exe cache get + lake build sur le pin — est documenté dans l’EPIC #15066 ; rien n’est vendorisé dans CoursIA).

Les objets que ce notebook consomme :

Objet FFL Rôle Analogie Tweety
Formula α (inductif) la syntaxe : atom, ⊥, 🡒, ⋏, ⋎ PlFormula et ses constructeurs
Boolean.Valuation α := α → Prop une valuation : chaque atome reçoit une proposition PossibleWorld (cas particulier décidable)
Formula.Boolean.val v φ la sémantique structurelle de φ sous v w.satisfies(f)
Formula.IsTautology φ φ valide pour toute valuation « 8/8 mondes » — mais sur un espace infini
Axioms.Peirce, Axioms.DNE, Axioms.LEM les schémas axiomatiques classiques — (Tweety n’a pas de versant syntaxique)
Boolean/Tait.lean ⚠️ stub sur ce pin : corps entièrement commenté (TODO: fix) — la complétude de Tait n’est pas importable le pont sémantique ↔︎ syntaxique reste hors de portée d’un importeur externe 
# --- 3. Tour d'API : #check sur les objets FFL (kernel Lean natif) ---
import pathlib
import shutil
import subprocess
import tempfile

FFL_COMMIT = "21318c7ee3b608c10366da82c4208b0d38a07402"  # pin attendu du clone pilote
FFL_LAKE = "~/ffl-foundation-pilot"  # clone du pilote, dans WSL


def run_wsl(command: str, timeout: int):
    """Lance une commande dans WSL, avec un echec explicite si `wsl` est absent.

    Les trois cellules de certification (sections 3, 4, 5) passent par WSL : sur
    un hote sans binaire `wsl`, un FileNotFoundError nu ne dit pas au lecteur que
    c'est la plateforme qui manque -- et non le notebook qui est faux.
    """
    if shutil.which("wsl") is None:
        raise RuntimeError(
            "les certificats Lean passent par WSL (`wsl -e bash -lc`) : binaire "
            "`wsl` introuvable sur cet hote. Les sections 3, 4 et 5 exigent un "
            "hote Windows + WSL ; les sections 1 et 2 (Tweety, controle croise "
            "Python) tournent partout."
        )
    return subprocess.run(
        ["wsl", "-e", "bash", "-lc", command],
        capture_output=True, text=True, encoding="utf-8", errors="replace",
        timeout=timeout,
    )


def ffl_head() -> str:
    """Mesure le HEAD REEL du clone pilote : le pin declare n'est pas une preuve."""
    r = run_wsl(f"git -C {FFL_LAKE} rev-parse HEAD", timeout=120)
    measured = (r.stdout or "").strip()
    if r.returncode != 0 or not measured:
        raise RuntimeError(
            f"clone pilote {FFL_LAKE} absent ou illisible "
            f"(`git rev-parse HEAD` -> exit {r.returncode}) : les certificats "
            f"n'auraient pas de provenance. Pin attendu : {FFL_COMMIT[:12]}."
        )
    return measured


measured_commit = ffl_head()
assert measured_commit == FFL_COMMIT, (
    f"le clone pilote a derive : mesure {measured_commit[:12]}, pin declare "
    f"{FFL_COMMIT[:12]}. Les deux certificats seraient compiles contre une "
    f"revision autre que celle annoncee -- realigner le clone "
    f"(`git -C {FFL_LAKE} checkout {FFL_COMMIT}`) ou mettre a jour le pin."
)
print(f"clone pilote verifie : {FFL_LAKE} @ {measured_commit[:12]} -- pin confirme")

api_tour = """import Foundation.Propositional.Formula.Basic
import Foundation.Propositional.Boolean.Basic
import Foundation.Propositional.Boolean.Tait
import Foundation.Propositional.Entailment.Cl

#check FFL.Propositional.Formula
#check FFL.Propositional.Boolean.Valuation
#check FFL.Propositional.Formula.Boolean.val
#check FFL.Propositional.Formula.Boolean.models_iff_val
#check FFL.Propositional.Formula.IsTautology
#check FFL.Axioms.Peirce
#check FFL.Axioms.LEM

-- Foundation.Propositional.Boolean.Tait s'importe SANS erreur, mais n'exporte
-- aucune declaration sur ce pin : son corps (lignes 11 a 225 du fichier) est un
-- unique commentaire bloc marque "TODO: fix". La completude de Tait
-- (T |= phi  ->  T |- phi) n'est donc PAS atteignable depuis un importeur.
"""


def run_lean(source: str):
    """Ecrit source dans un fichier temporaire et le fait verifier par le
    kernel Lean natif du lake FFL (lake env lean = toolchain + LEAN_PATH du pin)."""
    d = pathlib.Path(tempfile.mkdtemp(prefix="tweety5e_"))
    f = d / "scratch.lean"
    f.write_text(source, encoding="utf-8")
    winpath = f.resolve().as_posix()
    wslpath = "/mnt/" + winpath[0].lower() + winpath[2:]
    r = run_wsl(f"cd {FFL_LAKE} && lake env lean {wslpath}", timeout=1800)
    return (r.stdout or "") + (r.stderr or ""), r.returncode


out, rc = run_lean(api_tour)
print(f"$ lake env lean scratch.lean   (FFL @ {measured_commit[:12]} mesure, kernel natif)")
print(out)
print(f"[exit {rc}]")
clone pilote verifie : ~/ffl-foundation-pilot @ 21318c7ee3b6 -- pin confirme
$ lake env lean scratch.lean   (FFL @ 21318c7ee3b6 mesure, kernel natif)
FFL.Propositional.Formula.{u} (α : Type u) : Type u
FFL.Propositional.Boolean.Valuation.{u_2} (α : Type u_2) : Type u_2
FFL.Propositional.Formula.Boolean.val.{u_1} {α : Type u_1} (v : FFL.Propositional.Boolean.Valuation α) :
  FFL.Propositional.Formula α → Prop
FFL.Propositional.Formula.Boolean.models_iff_val.{u_1} {α : Type u_1} {v : FFL.Propositional.Boolean.Valuation α}
  {φ : FFL.Propositional.Formula α} : v ⊧ φ ↔ FFL.Propositional.Formula.Boolean.val v φ
FFL.Propositional.Formula.IsTautology.{u_1} {α : Type u_1} (φ : FFL.Propositional.Formula α) : Prop
FFL.Axioms.Peirce.{u_1} {F : Type u_1} [FFL.LogicalConnective F] (φ ψ : F) : F
FFL.Axioms.LEM.{u_1} {F : Type u_1} [FFL.LogicalConnective F] (φ : F) : F

[exit 0]

Lecture : ce que le #check établit

Chaque ligne est une vérification de type par le kernel Lean : ces objets existent, avec exactement ces types, dans le dépôt épinglé. En particulier :

  • Formula.Boolean.val a pour type Valuation α → Formula α → Prop — la sémantique est une fonction structurelle, pas une table ;
  • IsTautology φ se déplie en Valid (Boolean.Valuation α) φ — la validité est quantifiée sur toutes les valuations, un espace infini même pour trois atomes (une valuation y est une fonction vers Prop, pas un booléen) ;
  • Axioms.Peirce et Axioms.LEM sont des schémas axiomatiques : ((φ 🡒 ψ) 🡒 φ) 🡒 φ et φ ⋎ ∼φ — le versant syntaxique classique, celui que Tweety n’a pas.

Une limite mesurée sur ce pin — et pourquoi on la dit. La ligne import Foundation.Propositional.Boolean.Tait passe sans erreur, mais aucune déclaration de ce module n’est atteignable : le fichier Foundation/Propositional/Boolean/Tait.lean est un stub dont le corps entier (lignes 11 à 225) est un unique commentaire bloc marqué TODO: fix. La complétude de Tait — T ⊨ φ → T ⊢ φ, le pont sémantique ↔︎ syntaxique — n’est pas importable ici. Ce notebook le documente au lieu de l’invoquer : le côté syntaxique reste hors de portée, et l’API tour le montre plutôt que de le simuler.

Un détail structurel à retenir : Valuation et Formula sont deux branches sœurs de FFL.Propositional — la valuation n’est pas « dans » la formule, c’est un point de vue qu’on projette sur elle.

Provenance mesurée, pas déclarée. La cellule ci-dessus n’affiche pas le pin : elle interroge git -C ~/ffl-foundation-pilot rev-parse HEAD, compare la mesure au pin et échoue si le clone a dérivé — sans quoi le notebook pourrait compiler contre une autre révision tout en affichant la bonne. Ces trois cellules de certification passent par wsl : elles exigent un hôte Windows + WSL et le disent quand le binaire manque, plutôt que de rendre un FileNotFoundError nu. Les sections 1 et 2 (Tweety, contrôle croisé Python) tournent sur n’importe quel hôte.

4. Troisième lecture, certificat 1 : un théorème prouvé

Le syllogisme SYL a été observé 8/8. On va maintenant prouver — dans le kernel Lean, sur le type Formula (Fin 3) de FFL — qu’il est satisfait par toute valuation v : Fin 3 → Prop. La preuve déplie la sémantique val (les équations structurelles de FFL) pour réduire le but à de la logique propositionnelle pure sur v 0, v 1, v 2 — puis clôt par le kernel.

Un fait FFL rend cette forme obligatoire et non stylistique : la sémantique est Prop-valuée (val v φ : Prop), donc aucun decide n’est possible sur v ⊧ φ — une ligne de table n’est pas un booléen mais déjà un petit théorème. La preuve ci-dessous est la version quantifiée : le sondage des 8 mondes devient une quantification universelle, vérifiée par le kernel, et le terme de la preuve est un objet que n’importe qui peut rejouer.

# --- 4. Certificat 1 : SYL valide pour TOUTE valuation (proof, pas sondage) ---
cert1 = """import Foundation.Propositional.Formula.Basic
import Foundation.Propositional.Boolean.Basic

open FFL.Propositional

-- Le syllogisme hypothetique, sur les atomes 0 = a, 1 = b, 2 = c
def syl : Formula (Fin 3) :=
  (.atom 0 🡒 .atom 1) 🡒 ((.atom 1 🡒 .atom 2) 🡒 (.atom 0 🡒 .atom 2))

-- Toute valuation (un espace INFINI : Fin 3 -> Prop) satisfait syl.
-- Preuve : la semantique FFL se degrade en logique propositionnelle pure,
-- que le kernel verifie. Aucun denombrement de mondes n'intervient.
theorem syl_valid : ∀ v : Boolean.Valuation (Fin 3), v ⊧ syl := by
  intro v
  simp only [Formula.Boolean.models_iff_val, Formula.Boolean.val, syl]
  -- but restant : (v 0 → v 1) → (v 1 → v 2) → v 0 → v 2 -- syllogisme pur
  exact fun h01 h12 h0 => h12 (h01 h0)

#print axioms syl_valid
"""

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 (preuve sur toutes les valuations) : OK")
$ lake env lean scratch.lean
'syl_valid' depends on axioms: [propext]

[exit 0]
CERTIFICAT 1 (preuve sur toutes les valuations) : OK

Interprétation : preuve trouvée ≠ sondage exhaustif

∀ v : Fin 3 → Prop, v ⊧ syl — la quantification porte sur toutes les fonctions des atomes vers les propositions, pas sur 8 mondes. La ligne #print axioms rend la comptabilité d’axiomes du kernel : la preuve est close, sans sorry (seuls les axiomes structurels propext/Quot.sound apparaissent — la réduction v ⊧ φ ↔︎ val v φ en nécessite).

Les deux faces sont sémantiques toutes les deux : Tweety énumère les 8 mondes, Lean quantifie sur toutes les valuations. Le « oui » du solveur et le terme de preuve ci-dessus disent la même chose, par deux chemins indépendants — et un seul des deux reste bon à 100 atomes.

Les trois états, précision de vocabulaire. « Preuve trouvée » (un terme T ⊢ φ ou un ∀ v, v ⊧ φ clos) · « absence de preuve dans la borne » (un solveur borné qui rend inconnu) · « non-termination » (une recherche qui ne rend pas). En logique propositionnelle, la décidabilité garantit que la recherche termine toujours — les états 2 et 3 n’y apparaissent pas. Ils deviennent vivants en logique du premier ordre (tranche B de l’EPIC).

5. Certificat 2 : le contre-modèle transporté de Tweety vers Lean

Tweety a calculé les contre-modèles de ORB — la cellule 2bis les liste. On transporte le plus simple — le monde vide [] — vers Lean : la valuation v₀ := fun _ => False (aucun atome vrai) est la traduction exacte de ce monde. Le certificat prouve qu’elle falsifie a ⋎ b : la sémantique FFL se réduit à False ∨ False, que le kernel clôt.

L’aller-retour complet : calcul (Tweety) → sérialisation (le monde vide devient un terme Lean) → revérification (le kernel). Le témoin n’est pas recopié à la main : c’est un monde extrait de la table calculée qui est rejoué.

# --- 5. Certificat 2 : contre-modele transporte (temoin Tweety reverifie Lean) ---
# Le monde vide calcule par Tweety dans la cellule 2bis ([], aucun atome vrai)
chosen = "[]"
assert chosen in falsifiers, f"le temoin transporte doit etre un contre-modele calcule : {falsifiers}"

cert2 = """import Foundation.Propositional.Formula.Basic
import Foundation.Propositional.Boolean.Basic

open FFL.Propositional

def orb : Formula (Fin 3) := (.atom 0 ⋎ .atom 1)

-- Le monde vide de Tweety ([] = aucun atome vrai), transporte terme a terme.
def v0 : Boolean.Valuation (Fin 3) := fun _ => False

-- Certificat : cette valuation falsifie la formule. Le kernel degrade
-- val v0 orb en False ∨ False et le clot.
theorem v0_falsifies_orb : ¬ (v0 ⊧ orb) := by
  simp [Formula.Boolean.models_iff_val, Formula.Boolean.val, orb, v0]

-- Et le controle negatif : ORB n'est PAS une tautologie -- l'existence du
-- contre-modele certifie ci-dessus refute la validite.
example : ¬ Formula.IsTautology (orb) := by
  intro h
  exact v0_falsifies_orb (h v0)

#print axioms v0_falsifies_orb
"""

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 (contre-modele transporte) : OK")
$ lake env lean scratch.lean
'v0_falsifies_orb' depends on axioms: [propext, Quot.sound]

[exit 0]
CERTIFICAT 2 (contre-modele transporte) : OK

Interprétation : le témoin calculé, revérifié

La chaîne est complète : Tweety calcule le monde [] → le notebook le sérialise en v₀ = fun _ => False → le kernel Lean vérifie que cette valuation falsifie a ⋎ b. Le deuxième théorème (¬ IsTautology) est la contrepartie formelle du « 6/8 » : l’existence d’un contre-modèle certifié réfute la tautologie — c’est le contrôle négatif exigé par la tranche : satisfiable (des mondes rendent la formule vraie) et non valide (un monde la falsifie) sont établis séparément, par des témoins différents.

La division du travail est maintenant nette :

Question Tweety Lean
« Existe-t-il un contre-modèle ? » le calcule (chercher) le vérifie (vérifier)
« La formule est-elle valide ? » y répond par sondage (décidable ici) y répond par preuve (∀ v)
« Pourquoi ? » — le terme de preuve est la raison

6. Ce que ce laboratoire ne couvre pas — et où le regarder

  • provable au sens des calculs : on a prouvé la validité sémantique (∀ v, v ⊧ φ). Le versant syntaxique — la complétude de Tait (T ⊨ φ → T ⊢ φ), qui relierait les deux — est hors de portée sur ce pin : Foundation/Propositional/Boolean/Tait.lean y est un stub commenté (constat de la section 3). Construire la dérivation Tait/Hilbert elle-même, la mesurer, la normaliser — c’est une tranche ultérieure de l’EPIC.
  • FOL, modèles, complétude de Gödel : le même motif (exécuter → représenter → transporter le témoin) se rejoue au premier ordre — tranche B — où la décidabilité tombe et où « absence de preuve dans la borne » devient un état réel.
  • Logiques non classiques : Foundation porte aussi le versant intuitionniste (sémantiques de Heyting) — l’exercice 2 le touche du doigt : en logique intuitionniste, le tiers-exclu n’est plus valide, et le « même » laboratoire rendrait un verdict différent sur la même formule.
  • Énumération vs preuve à grande échelle : à 3 atomes, le sondage est honnête. Des fragments plus grands montreront des cas où seule la preuve reste praticable.

7. Exercices

Les trois exercices sont non résolus : les cellules de départ sont des stubs sans erreur volontaire — complétez-les.

Exercice 1 — Votre formule au tribunal des trois lectures

Choisissez une formule nouvelle sur le fragment {a, b, c} (ni SYL, ni ORB, ni CONTR) — par exemple (a => b) || (b => a), ou (a && b) => (a || c). Prédisez son compte de mondes avant d’exécuter, puis faites-la passer par les trois lectures : table Tweety, recomptage Python, et — si vous pensez qu’elle est valide — certificat Lean sur le modèle de la section 4. Votre prédiction a-t-elle survécu ?

# Exercice a completer : votre formule au tribunal des trois lectures.
# MA_FORMULE = "(a => b) || (b => a)"
# prediction = None  # votre compte attendu sur 8 mondes
# 1. Ajoutez-la a FORMULES et rejouez la cellule de la table de verite.
# 2. Confrontez la prediction au compte mesure.
# 3. Si vous la pensez valide : construisez le certificat (section 4).
print("Exercice a completer : voir commentaires.")
Exercice a completer : voir commentaires.

Exercice 2 — Le même schéma, une autre logique

Peirce := ((φ 🡒 ψ) 🡒 φ) 🡒 φ est un schéma classique : Foundation l’énonce (Axioms.Peirce) et le prouve dérivable dans tout système classique. En logique intuitionniste (sémantiques de Heyting), ce même schéma n’est pas dérivable.

Expliquez pourquoi la sémantique de Heyting (les valuations vivent dans une algèbre de Heyting, pas dans Prop) rend l’argument classique inutilisable, et ce que cela change pour la méthode de ce notebook : le sondage par mondes possibles correspond-il encore à la sémantique ? (Indice : dans Heyting, la sémantique n’est pas composée de « mondes » booléens — le PossibleWorld de Tweety n’a plus de contre-partie directe.)

# Exercice a completer : Peirce classique vs intuitionniste.
# 1. Relire le #check de FFL.Axioms.Peirce (section 3).
# 2. Consulter Foundation/Propositional/Heyting/Semantics.lean dans le depot FFL.
# 3. Rediger (en markdown, dans une nouvelle cellule) pourquoi le contre-modele
#    booleen n'existe plus en Heyting.
print("Exercice a completer : voir commentaires.")
Exercice a completer : voir commentaires.

Exercice 3 — Étendre le fragment : prédire le coût de l’énumération

Passez au fragment {a, b, c, d} (4 atomes, 16 mondes). Avant d’exécuter : combien de lignes aura la table ? Combien de tests satisfies ? Et pour 30 atomes — combien de mondes, et pourquoi la preuve de la section 4, elle, ne change pas de taille (à substitution des atomes près) ? Vérifiez la première prédiction en exécutant, et exprimez la seconde en puissances de 2.

# Exercice a completer : etendre le fragment a 4 atomes.
# ATOMES_4 = ["a", "b", "c", "d"]
# 1. Predire le nombre de mondes (une puissance de 2).
# 2. Rejouer l'enumeration (cellule de la table) sur la signature etendue.
# 3. Comparer au compte predit ; conclure sur la croissance de l'enumeration
#    vs la taille constante de la preuve.
print("Exercice a completer : voir commentaires.")
Exercice a completer : voir commentaires.

Conclusion — les quatre niveaux, parcourus sur trois formules

  1. Demander à un raisonneur : Tweety/SAT4J a répondu (verdicts, modèles, contre-modèles calculés) — il exécute.
  2. Définir formellement : Foundation (FFL) pose Formula, val, IsTautology — la logique comme objet mathématique.
  3. Certifier : le syllogisme prouvé sur toutes les valuations (∀ v), zéro sorry, axiomes comptés — le kernel garantit.
  4. Transporter un témoin : le monde vide calculé par Tweety, sérialisé, revérifié par Lean — calculer ici, certifier là.

Le companion s’arrête volontairement au propositionnel : la même architecture, poussée au premier ordre (tranche B), aux calculs de preuve et à la logique de prouvabilité, est le reste de l’EPIC #15066.

Retour au sommet