Lean-3b — Formalized Formal Logic : le laboratoire propositionnel (pont Tweety ↔︎ Lean)

Navigation : Index | Lean-3 (Propositions) << | Lean-4 (Quantifiers) >>

Companion transversal de Tweety-2 et de Lean-3 — premier maillon de l’Epic #15066 (Formalized Formal Logic).

Les quatre lectures d’une formule

Ce notebook fait traverser les mêmes formules à deux moteurs, pour rendre visible la différence entre :

  1. demander à un raisonneur si une formule est satisfaite ou dérivable — Tweety exécute ;
  2. définir formellement syntaxe, preuve et sémantique — la bibliothèque Formalized Formal Logic les pose comme objets ;
  3. certifier correction et complétude — les métathéorèmes deviennent des énoncés Lean vérifiés ;
  4. transporter un témoin calculé par le raisonneur vers le noyau — le contre-modèle de Tweety devient un théorème.

Formules témoins :

  • φPeirce := ((p → q) → p) → p — le schéma de Peirce : tautologie classique ;
  • φOr := p ∨ q — satisfiable mais non valide : le contrôle négatif.

Le versant certifié vit dans le lake formal_logic_lean/ (module FormalLogic/Bridge.lean, consommé en CONSUMER_PINNÉ au commit 81810b9f, verdict du pilote #15520).

Outils

  • Tweety (JVM via JPype, jar shaded ../Tweety/libs) : le raisonneur qui exécute — parsing, mondes possibles, satisfaction ;
  • le lake formal_logic_lean (toolchain Lean v4.33.1) : le noyau qui certifie — les mêmes formules comme objets FFL.Formula, la table de vérité comme petits théorèmes évalués par le noyau, la validité comme théorème.

Le fragment est fini et sérialisable : deux atomes p, q — l’AST Python ci-dessous est la source unique, déclinée vers les deux moteurs.

# --- Initialisation JVM Tweety (patron Tweety-2) ---
import os
import pathlib

import jpype
import jpype.imports

jvm_ready = False
if not os.environ.get("JAVA_HOME"):
    for jdk_path in [pathlib.Path("../Argument_Analysis/jdk-17-portable"),
                     pathlib.Path("../Tweety/jdk-17-portable")]:
        if jdk_path.exists():
            zulu_dirs = list(jdk_path.glob("zulu*"))
            if zulu_dirs:
                os.environ["JAVA_HOME"] = str(zulu_dirs[0].resolve())
                break

jar_files = []
for libs_dir in [pathlib.Path("../Tweety/libs"), pathlib.Path("../Argument_Analysis/libs")]:
    if libs_dir.exists():
        jar_files.extend(sorted(libs_dir.glob("*.jar")))
if not jar_files:
    print("Aucun JAR Tweety trouve (voir README de la serie Tweety : libs/ gitignore).")
else:
    classpath = os.pathsep.join(str(j.resolve()) for j in jar_files)
    try:
        jpype.startJVM(classpath=[classpath])
        jvm_ready = True
        print(f"JVM demarree, {len(jar_files)} JAR(s).")
    except Exception as e:
        print(f"JVM deja demarree ou erreur : {e}")
        jvm_ready = jpype.isJVMStarted()
print("jvm_ready =", jvm_ready)
JVM demarree, 41 JAR(s).
jvm_ready = True

1. La syntaxe commune — un AST, deux sérialisations

L’AST Python est la source unique : to_tweety produit la chaîne que le parser Tweety lit (p => q, !p, p || q, p && q) ; to_lean produit la construction FFL.Formula correspondante (Formula.atom 0 🡒 Formula.atom 1…). Les atomes sont les constructeurs Formula.atom (0 : Fin 2) et Formula.atom (1 : Fin 2) : FFL n’expose aucun littéral #0 — les deux moteurs reçoivent donc littéralement la même formule, pas deux copies réécrites à la main.

# --- AST commun + serialiseurs ---
from dataclasses import dataclass
from typing import Union

@dataclass(frozen=True)
class Atom:
    name: str
    idx: int  # index Lean (Fin 2) : p -> 0, q -> 1

@dataclass(frozen=True)
class Imp:
    a: "Fml"
    b: "Fml"

@dataclass(frozen=True)
class Or:
    a: "Fml"
    b: "Fml"

@dataclass(frozen=True)
class And:
    a: "Fml"
    b: "Fml"

@dataclass(frozen=True)
class Not:
    a: "Fml"

Fml = Union[Atom, Imp, Or, And, Not]

P, Q = Atom("p", 0), Atom("q", 1)

def to_tweety(f: Fml) -> str:
    if isinstance(f, Atom): return f.name
    if isinstance(f, Imp):  return f"({to_tweety(f.a)} => {to_tweety(f.b)})"
    if isinstance(f, Or):   return f"({to_tweety(f.a)} || {to_tweety(f.b)})"
    if isinstance(f, And):  return f"({to_tweety(f.a)} && {to_tweety(f.b)})"
    if isinstance(f, Not):  return f"!{to_tweety(f.a)}"
    raise TypeError(f)

def to_lean(f: Fml) -> str:
    if isinstance(f, Atom): return f"Formula.atom {f.idx}"
    if isinstance(f, Imp):  return f"({to_lean(f.a)} 🡒 {to_lean(f.b)})"
    if isinstance(f, Or):   return f"({to_lean(f.a)} ⋎ {to_lean(f.b)})"
    if isinstance(f, And):  return f"({to_lean(f.a)} ⋏ {to_lean(f.b)})"
    if isinstance(f, Not):  return f"∼{to_lean(f.a)}"
    raise TypeError(f)

phi_peirce = Imp(Imp(Imp(P, Q), P), P)   # ((p -> q) -> p) -> p
phi_or     = Or(P, Q)                      # p || q

for name, f in [("phiPeirce", phi_peirce), ("phiOr", phi_or)]:
    print(f"{name:10s} tweety: {to_tweety(f):24s} lean: {to_lean(f)}")
phiPeirce  tweety: (((p => q) => p) => p)   lean: (((Formula.atom 0 🡒 Formula.atom 1) 🡒 Formula.atom 0) 🡒 Formula.atom 0)
phiOr      tweety: (p || q)                 lean: (Formula.atom 0 ⋎ Formula.atom 1)

2. Le versant exécution — Tweety calcule

Les quatre mondes possibles de {p, q} (un monde = l’ensemble des propositions vraies) : chaque monde est une ligne de la table de vérité. Tweety évalue la satisfaction formule par monde — la table que tout étudiant écrit à la main, ici produite par le raisonneur.

# --- Table de verite par execution Tweety ---
assert jvm_ready, "JVM Tweety requise (cellule d'initialisation)"
from jpype import JObject

from org.tweetyproject.logics.pl.parser import PlParser
from org.tweetyproject.logics.pl.semantics import PossibleWorld
from org.tweetyproject.logics.pl.syntax import PlFormula, Proposition

pl_parser = PlParser()

def tweety_world(p_val: bool, q_val: bool) -> "PossibleWorld":
    w = PossibleWorld()
    if p_val: w.add(Proposition("p"))
    if q_val: w.add(Proposition("q"))
    return w

WORLDS = {
    "p=V,q=V": tweety_world(True, True),
    "p=V,q=F": tweety_world(True, False),
    "p=F,q=V": tweety_world(False, True),
    "p=F,q=F": tweety_world(False, False),
}

def tweety_table(f: Fml) -> dict:
    pf = pl_parser.parseFormula(to_tweety(f))
    rows = {label: bool(w.satisfies(JObject(pf, PlFormula))) for label, w in WORLDS.items()}
    rows["__valid__"] = all(v for k, v in rows.items() if not k.startswith("__"))
    rows["__satisfiable__"] = any(v for k, v in rows.items() if not k.startswith("__"))
    return rows

for name, f in [("phiPeirce", phi_peirce), ("phiOr", phi_or)]:
    t = tweety_table(f)
    lignes = " ; ".join(f"{k}={int(v)}" for k, v in t.items() if not k.startswith("__"))
    print(f"{name}: {lignes}")
    print(f"  satisfiable = {t['__satisfiable__']} | valid (tautologie) = {t['__valid__']}")
phiPeirce: p=V,q=V=1 ; p=V,q=F=1 ; p=F,q=V=1 ; p=F,q=F=1
  satisfiable = True | valid (tautologie) = True
phiOr: p=V,q=V=1 ; p=V,q=F=1 ; p=F,q=V=1 ; p=F,q=F=0
  satisfiable = True | valid (tautologie) = False

Extraire les témoins : contre-modèles et mondes satisfaisants

La table dit tout, mais le raisonneur sait aussi nommer les lignes : les mondes qui falsifient (contre-modèles — les témoins d’invalidité) et ceux qui satisfont (témoins de satisfiabilité). Ce sont exactement ces témoins que le versant Lean transformera en théorèmes.

# --- Contre-modele calcule par le raisonneur ---
t_or = tweety_table(phi_or)
countermodels = [k for k, v in t_or.items() if not k.startswith("__") and not v]
witness_satisfiable = [k for k, v in t_or.items() if not k.startswith("__") and v]
print("phiOr  contre-modeles :", countermodels)
print("phiOr  temoin satisfiabilite :", witness_satisfiable)
print("phiPeirce contre-modeles :",
      [k for k, v in tweety_table(phi_peirce).items() if not k.startswith("__") and not v] or "aucun")
phiOr  contre-modeles : ['p=F,q=F']
phiOr  temoin satisfiabilite : ['p=V,q=V', 'p=V,q=F', 'p=F,q=V']
phiPeirce contre-modeles : aucun

Lecture : ce que Tweety a dit — et ce qu’il ne dit pas

Tweety (exécution) statut
phiPeirce 4/4 mondes satisfont tautologie constatée
phiOr 3/4 mondes satisfont, p=F,q=F falsifie satisfiable, non valide constatés

Tweety constate : il a énuméré les mondes de ce fragment fini. Il ne dit rien de pourquoi la table suffit (exhaustivité), ne produit aucune preuve de phiPeirce, et son moteur n’est pas certifié. Ces trois lacunes sont exactement ce que le versant Lean referme.

3. Le versant certification — le lake formal_logic_lean

Le module FormalLogic/Bridge.lean contient les mêmes formules comme objets FFL.Formula (générées par to_lean ci-dessus) :

Côté notebook (Tweety) Côté lake (Lean)
monde p=V,q=V… valTT, valTF, valFT, valFF (Valuation := Fin 2 → Prop)
ligne de table peirce_row_TT… : chaque ligne est un petit théorème (simp [models_iff_val, val] — la sémantique FFL est Prop-valuée, pas décidable par decide)
« on a essayé tous les mondes » valuations_exhaustive : toute valuation est l’une des 4 lignes
tautologie constatée peirce_valid : ∀ v, v ⊧ φPeirce (théorème)
contre-modèle p=F,q=F or_not_valid : le témoin calculé devient certifié
p ∨ q satisfiable or_satisfiable (∃ v, v ⊧ φOr)
contrôle négatif or_not_universally_valid : satisfiable sans être valide
— (absent de Tweety) peirce_provable : le schéma est dérivable (FFL.Entailment.peirce)

Et les métathéorèmes qui donnent son sens à la table (consommés, jamais redémontrés) :

  • Foundation.Propositional.Boolean.Tait.soundness : T ⊢ φ → T ⊨[Valuation α] φ ;
  • Foundation.Propositional.Boolean.Tait.completeness! : T ⊨[Valuation α] φ → T ⊢ φ — c’est la complétude qui garantit que, pour ce fragment, une table exhaustive suffit à fonder la dérivabilité.
# --- Certification : build du lake (patron Tweety-5d) ---
import os
import subprocess

# Le lake vit en sous-dossier du dossier du notebook : le chemin WSL se dérive
# du cwd (wslpath), jamais en dur — le notebook reste exécutable depuis
# n'importe quel checkout (worktree ou clone post-merge).
LAKE_DIR = subprocess.run(
    ["wsl", "-e", "wslpath", "-a", os.getcwd()],
    capture_output=True, text=True, encoding="utf-8").stdout.strip() + "/formal_logic_lean"

r = subprocess.run(
    ["wsl", "-e", "bash", "-lc",
     f"cd {LAKE_DIR} && lake build FormalLogic.Bridge 2>&1 | tail -8; "
     "echo \"lake build rc=${PIPESTATUS[0]}\""],
    capture_output=True, text=True, encoding="utf-8", timeout=1800)
print(r.stdout.strip() or r.stderr.strip())
Build completed successfully (878 jobs).
lake build rc=0

Le noyau répond : audit des axiomes

Un théorème Lean ne dit pas seulement quoi est prouvé — #print axioms liste sur quoi il repose. Pour des théorèmes d’évaluation sur un fragment fini, l’attendu est l’axiome minimal : aucun sorry, aucune déclaration non constructive importée en contrebande.

# --- Audit des axiomes : le noyau repond ---
import tempfile

verify_src = (
    "import FormalLogic.Bridge\n"
    "#print axioms FormalLogic.Bridge.peirce_valid\n"
    "#print axioms FormalLogic.Bridge.or_not_valid\n"
    "#print axioms FormalLogic.Bridge.or_satisfiable\n"
    "#print axioms FormalLogic.Bridge.valuations_exhaustive\n"
    "#print axioms FormalLogic.Bridge.peirce_provable\n"
)
with tempfile.NamedTemporaryFile("w", suffix=".lean", delete=False,
                                 encoding="utf-8", newline="\n") as f:
    f.write(verify_src)
    verify_win = f.name
wsl_path = subprocess.run(
    ["wsl", "-e", "wslpath", "-a", verify_win.replace(chr(92), "/")],
    capture_output=True, text=True, encoding="utf-8").stdout.strip()

r = subprocess.run(
    ["wsl", "-e", "bash", "-lc",
     f"cd {LAKE_DIR} && lake env lean {wsl_path} 2>&1 | tail -10"],
    capture_output=True, text=True, encoding="utf-8", timeout=900)
print(r.stdout.strip() or r.stderr.strip())
pathlib.Path(verify_win).unlink(missing_ok=True)
'FormalLogic.Bridge.peirce_valid' depends on axioms: [propext, Classical.choice, Quot.sound]
'FormalLogic.Bridge.or_not_valid' depends on axioms: [propext, Quot.sound]
'FormalLogic.Bridge.or_satisfiable' depends on axioms: [propext, Quot.sound]
'FormalLogic.Bridge.valuations_exhaustive' depends on axioms: [propext, Classical.choice, Quot.sound]
'FormalLogic.Bridge.peirce_provable' does not depend on any axioms

Interprétation : la boucle se referme

  • Même formule : l’AST Python produit les deux encodages (to_tweety / to_lean) — aucun des deux n’est réécrit à la main.
  • Même table : les 4 mondes Tweety et les 4 valuations FFL se correspondent une à une, et valuations_exhaustive prouve que cette table à 4 lignes contient toutes les valuations du fragment — c’est lui qui transforme une énumération finie en preuve universelle.
  • Témoins transportés : le contre-modèle p=F,q=F calculé par Tweety est le témoin du théorème or_not_valid ; le monde satisfaisant devient or_satisfiable.
  • Au-delà de l’exécution : peirce_provable donne la dérivation (versant preuve), et completeness! (Tait) garantit que table et dérivation ne peuvent pas diverger sur ce fragment.

Dette assumée (même position que Tweety-5d) : Tweety n’est pas certifié — le transport préuve ↔︎ exécution repose sur la sérialisation commune, vérifiée ici sur deux formules, pas sur un pont formel. L’internalisation du raisonneur est un chantier séparé, pas un préalable.

4. Exercices

Exercice 1 — Trois atomes : (p ∧ q) → r est-elle valide ?

Ajoutez l’atome r (index Lean 2) à l’AST, étendez la table à 8 mondes et faites répondre Tweety. Vérifiez que le verdict est non valide et identifiez le contre-modèle le plus « petit ».

# Exercice a completer : atome r + table 8 mondes cote Tweety.
# R = Atom("r", 2)
# phi_pqr = Imp(And(P, Q), R)
# 1. etendre WORLDS aux 8 mondes de {p, q, r} ;
# 2. table + verdict Tweety (satisfiable ? valide ?) ;
# 3. afficher les contre-modeles.
print("Exercice a completer")
Exercice a completer

Exercice 2 — Énoncer la validité en Lean : (p → q) ∨ (q → p)

Cette disjonction est une tautologie classique (aucun monde ne la falsifie — vérifiez-le côté Tweety d’abord). Dans le style de peirce_valid : quelles quatre valuations suffisent, et quel théorème d’exhaustivité réutilise-t-on ? Écrivez l’énoncé or_imp_valid (la preuve suit le même schéma — vous pouvez la laisser commentée).

# Exercice a completer : enoncer (et demontrer) cote Lean.
# Dans le style de Bridge.lean (namespace `FormalLogic.Bridge`, apres `open FFL.Propositional`) :
# def phiOrImp : Formula Atom := (Formula.atom 0 🡒 Formula.atom 1) ⋎ (Formula.atom 1 🡒 Formula.atom 0)
# theorem or_imp_valid : ∀ v : Formula.Boolean.Valuation Atom, v ⊧ phiOrImp := by
#   intro v
#   rcases valuations_exhaustive v with rfl | rfl | rfl | rfl
#   · exact ...  -- une ligne par valuation (petit theoreme simp, cf. peirce_row_TT)
#   ...
print("Exercice a completer")
Exercice a completer

Exercice 3 — Une formule contingente

Trouvez une formule χ sur {p, q} telle que χ est satisfiable, χ non valide, et ¬χ satisfiable (une contingence). Vérifiez les trois verdicts avec Tweety, puis dites quel théorème du Bridge s’applique et lequel échoue pour χ — et pourquoi cela ne contredit pas completeness!.

# Exercice a completer : contingence cote Tweety + lecture cote Bridge.
# chi = ...  # votre formule
# t_chi = tweety_table(chi)          # satisfiable, non valide
# t_not_chi = tweety_table(Not(chi)) # negation satisfiable
# print(t_chi, t_not_chi)
print("Exercice a completer")
Exercice a completer

Conclusion — ce que le pont établit, et la suite

Sur ce fragment fini, l’arc complet tient : exécuter (Tweety produit table, satisfiabilité, contre-modèles), définir (FFL pose syntaxe et sémantique comme objets), certifier (chaque ligne est un théorème évalué, la validité un théorème, la dérivation un lemme), transporter (les témoins de l’un deviennent les théorèmes de l’autre). Les métathéorèmes soundness / completeness! (Tait) sont consommés — jamais redémontrés — et fondent l’accord des deux moteurs.

La suite de l’Epic #15066 élargit chaque versant :

  • Tranche B — FOL : dérivation, modèle, complétude (companion Tweety-2c / Lean-4) ;
  • Tranche C — logiques modales : du raisonneur aux cadres de Kripke (Tweety-3) ;
  • Tranche E — calculabilité et limites : diagonalisation, incomplétude.

Voir aussi : Tweety-5b et Tweety-5d — les ponts générateur→certificat qui ont établi le patron ; le lake formal_logic_lean/README.md pour le pin FFL et la mesure d’imports.

Retour au sommet