Tweety-02e — Calculs de preuve : Hilbert, séquents, Hauptsatz

Série Tweety — laboratoires croisés Java ↔︎ Lean (EPIC #15066, Tranche D). Une même question — comment calcule-t-on une preuve ? — posée à trois moteurs : le système de Hilbert (axiomes + modus ponens) et les oracles de Tweety (Java, via JPype) qui décident, le calcul des séquents LK de Gentzen dont l’élimination des coupures est un théorème du noyau Lean dans le lake formal_logic_lean (corpus FFL épinglé).

Navigation : Tweety-02d-FOL-Lab-Lean (labo FOL) · Tweety-5e-Propositional-Lab-Lean (labo propositionnel) · Tweety-02-Basic-Logics-Python (PL exécutée) · README

Objectifs pédagogiques

Vérifier les trois schémas d’axiomes de Hilbert par deux oracles réels (SimplePlReasoner, SatReasoner) — et comprendre pourquoi « tautologie » est un verdict, pas une preuve
Construire une preuve de Hilbert par chaînage avant (instanciation des schémas + modus ponens), et mesurer son coût : instances générées, formules dérivées, applications de MP
Mesurer les deux régimes de preuve dans le calcul des séquents LK : hauteur et taille d’un arbre, avec et sans coupure
Invoquer le Hauptsatz comme un théorème — Derivation.Canonical.constructiveHauptsatz rend la dérivation sans coupure et le témoin IsCutFree, vérifiés par le noyau Lean
Lire un résultat négatif honnêtement : la recherche Hilbert ne trouve pas tout ce que l’oracle décide — le vivier d’instanciation, pas la logique, en est la cause

Prérequis

Tweety-01-Setup-Python exécuté (JVM, JARs, JPype) — le dossier libs/ du répertoire Tweety
Notions propositionnelles : Tweety-02 (connecteurs, satisfaisabilité)
Pour les sections 4-5 : 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 : troisième labo croisé de l’EPIC #15066, après le propositionnel (Tweety-5e, Tranche A) et le FOL (Tweety-02d, Tranche B) — même patron moteur exécuté ↔︎ noyau certifiant, mais le sujet n’est plus le verdict d’un raisonneur : c’est l’objet preuve lui-même, mesuré dans deux calculs différents.

1. La question du labo

Trois traditions répondent à « pourquoi cette formule est-elle vraie ? » de trois façons irréductibles l’une à l’autre.

Hilbert : on fixe des schémas d’axiomes et une règle, le modus ponens. Une preuve est une liste finie de formules ; les axiomes sont vrais par décret, chaque étape est justifiée par MP. Trouver une preuve = chercher dans l’espace des formules dérivables — coûteux, mais chaque objet produit est vérifiable ligne à ligne, sans sémantique.
Gentzen (LK) : on fixe des règles d’inférence qui transforment des séquents (multi-ensembles de formules). Une preuve est un arbre. La règle de coupure (cut) a la même puissance que MP, mais elle coupe un arbre en deux : elle raccourcit les preuves et complique leur lecture. Le Hauptsatz de Gentzen dit que toute coupure peut être éliminée — la preuve grandit, mais devient « analytique » : chaque formule y est sous-formule de la conclusion.
Oracle sémantique : on demande à un solveur si la formule est valide (ici SimplePlReasoner — résolution — et SatReasoner, adossé à Sat4j). La réponse arrive vite, mais elle ne contient aucune preuve — c’est un verdict, pas un témoin.

Ce notebook mesure les trois, sur la même micro-théorie propositionnelle {p, q, r}.

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

TWEETY_DIR = pathlib.Path.cwd()
if TWEETY_DIR.name != "Tweety":
    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 (JDK portable, dossier libs/ ou demarrage JVM) : "
        "reparer l'environnement (cf. Tweety-01-Setup-Python) avant de relancer."
    )

import jpype
from jpype import JClass

Proposition = JClass("org.tweetyproject.logics.pl.syntax.Proposition")
Implication = JClass("org.tweetyproject.logics.pl.syntax.Implication")
Negation = JClass("org.tweetyproject.logics.pl.syntax.Negation")
Conjunction = JClass("org.tweetyproject.logics.pl.syntax.Conjunction")
PlBeliefSet = JClass("org.tweetyproject.logics.pl.syntax.PlBeliefSet")
PlFormula = JClass("org.tweetyproject.logics.pl.syntax.PlFormula")
SimplePlReasoner = JClass("org.tweetyproject.logics.pl.reasoner.SimplePlReasoner")
SatReasoner = JClass("org.tweetyproject.logics.pl.reasoner.SatReasoner")

p, q, r = Proposition("p"), Proposition("q"), Proposition("r")
LETTRES = [p, q, r]

simple = SimplePlReasoner()
sat = SatReasoner()
vide = PlBeliefSet()
print("SimplePlReasoner installe :", simple.isInstalled())
print("SatReasoner installe      :", sat.isInstalled())

--- Initialisation Tweety ---
JDK portable: zulu17.50.19-ca-jdk17.0.11-win_x64
Bibliotheques natives: native/
JVM demarree avec 42 JARs.
SimplePlReasoner installe : True
SatReasoner installe      : True

Lecture : deux oracles réels, pas une simulation

SimplePlReasoner implémente la résolution au premier ordre sur le fragment propositionnel ; SatReasoner traduit la requête en CNF et interroge un solveur SAT (Sat4j, faute de solveur configuré par défaut — le message « No default SAT solver configured » est un avertissement de configuration, pas une erreur).

Les deux isInstalled() à True sont le contrôle d’environnement : la suite du notebook interroge ces objets, et si la JVM ou les JARs manquaient, l’exécution s’arrêterait ici plutôt que de produire des verdicts inventés.

2. Les axiomes de Hilbert, vérifiés par l’oracle

Le système de Łukasiewicz tient en trois schémas :

#	Schéma
A1	`p → (q → p)`
A2	`(p → (q → r)) → ((p → q) → (p → r))`
A3	`(¬p → ¬q) → (q → p)`

avec une règle d’inférence : de φ et φ → ψ, conclure ψ (modus ponens).

Ces trois schémas sont choisis : rien ne dit a priori qu’ils sont valides. On commence donc par demander aux deux oracles si chacun est une tautologie — la preuve, elle, viendra de la syntaxe.

# --- Les trois schemas d'axiomes, soumis aux deux oracles (aucune preuve encore) ---
A1 = Implication(p, Implication(q, p))
A2 = Implication(Implication(p, Implication(q, r)),
                 Implication(Implication(p, q), Implication(p, r)))
A3 = Implication(Implication(Negation(p), Negation(q)), Implication(q, p))
AXIOMES = [A1, A2, A3]

for i, A in enumerate(AXIOMES, 1):
    print(f"A{i}: {A}")
    print(f"     SimplePlReasoner = {simple.query(vide, A)}   SatReasoner = {sat.query(vide, A)}")

# Le meme objet formule est reutilise partout : l'API d'acces aux sous-formules
# servira au moteur de recherche (section 3).
exemple = Implication(p, q)
print("\nImplication.getFirstFormula() :", exemple.getFirstFormula())
print("Implication.getSecondFormula():", exemple.getSecondFormula())
print("Negation.getFormula()         :", Negation(p).getFormula())

A1: (p=>(q=>p))
     SimplePlReasoner = True   SatReasoner = True
A2: ((p=>(q=>r))=>((p=>q)=>(p=>r)))
     SimplePlReasoner = True   SatReasoner = True
A3: ((!p=>!q)=>(q=>p))
     SimplePlReasoner = True   SatReasoner = True

Implication.getFirstFormula() : p
Implication.getSecondFormula(): q
Negation.getFormula()         : p

Lecture : « tautologie » est un verdict sémantique

Les six True ci-dessus ne sont pas des preuves — ce sont des décisions. Un oracle répond à la question « la formule est-elle conséquence de la base vide ? » en explorant les valuations ; il ne produit aucun objet que l’on puisse inspecter, transmettre ou vérifier indépendamment.

C’est exactement la limite que le reste du notebook comble : construire des objets-preuve, puis les mesurer.

3. Chercher une preuve : chaînage avant

Une preuve de Hilbert est une suite finie de formules F1 … Fn où chaque Fi est :

une instance d’un schéma d’axiome sur des formules quelconques, ou
la conclusion d’un modus ponens appliqué à deux formules déjà présentes.

Le moteur ci-dessous fait exactement cela, en chaînage avant : il instancie les trois schémas sur un ensemble fini de candidats, puis applique MP jusqu’à saturation, tour après tour.

Ce que le moteur est, et ce qu’il n’est pas. C’est une construction pédagogique déclarée : Tweety n’expose pas de prouveur de Hilbert pour la logique propositionnelle (son Rule/RuleSet vise les programmes logiques, ses prouveurs SimplePlReasoner/SatReasoner décident). Ce moteur n’est donc pas un organe concurrent — il produit l’objet preuve que les oracles ne produisent pas, et chaque formule qu’il dérive est re-vérifiée par les oracles (section suivante). Le candidat target est inclus dans le vivier d’instanciation : sans lui, l’antécédent d’une instance d’axiome utile ne serait jamais engendré.

# --- Moteur de recherche : instanciation des schemas + chainage avant (modus ponens) ---
import time
from itertools import product


def instances_axiomes(candidats):
    """Toutes les instances des trois schemas sur `candidats`."""
    out = []
    for a in candidats:
        for b in candidats:
            out.append(Implication(a, Implication(b, a)))          # A1
    for a, b, c in product(candidats, repeat=3):
        out.append(Implication(Implication(a, Implication(b, c)),  # A2
                               Implication(Implication(a, b), Implication(a, c))))
    for a in candidats:
        for b in candidats:
            out.append(Implication(Implication(Negation(a), Negation(b)),
                                   Implication(b, a)))             # A3
    return out


def preuve_hilbert(cible, candidats, max_formules=200000):
    """Chainage avant borne : axiomes instancies, puis fermeture par modus ponens.

    Retourne (preuve, stats, base) ou la preuve est une liste de (formule, justification)
    dans l'ordre d'utilisation, et base l'index complet des formules derivees.
    """
    graines = instances_axiomes(candidats)
    base = {}
    frontiere = []
    for s in graines:
        k = str(s)
        if k not in base:
            base[k] = (s, "axiome", None)
            frontiere.append(s)
    cible_k = str(cible)
    mp = 0
    t0 = time.time()
    tour = 0
    while frontiere and len(base) < max_formules:
        tour += 1
        index = {k: v[0] for k, v in base.items()}
        nouveaux = []
        for f in frontiere:
            if not Implication.class_.isInstance(f):
                continue
            antecedent = str(f.getFirstFormula())
            if index.get(antecedent) is None:
                continue
            conclusion = f.getSecondFormula()
            kc = str(conclusion)
            if kc in base:
                continue
            base[kc] = (conclusion, "MP", (str(f), antecedent))
            nouveaux.append(conclusion)
            mp += 1
        frontiere = nouveaux
        if cible_k in base:
            break
    stats = {"instances_axiomes": len(graines), "formules_connues": len(base),
             "modus_ponens": mp, "tours": tour, "secondes": round(time.time() - t0, 3)}
    if cible_k not in base:
        return None, stats, base
    chaine, vus = [], set()

    def remonter(k):
        if k in vus:
            return
        f, genre, charge = base[k]
        if genre == "axiome":
            vus.add(k)
            chaine.append((k, "axiome"))
            return
        remonter(charge[0])
        remonter(charge[1])
        vus.add(k)
        chaine.append((k, "MP"))

    remonter(cible_k)
    return chaine, stats, base


print("Moteur pret :", instances_axiomes.__name__, "+", preuve_hilbert.__name__)

Moteur pret : instances_axiomes + preuve_hilbert

Première cible : `p → p`

C’est le plus petit théorème du système qui ne soit pas une instance d’axiome — le premier endroit où le modus ponens devient indispensable.

Une précision sur le contrat du moteur, visible dans sa signature : la cible cherchée doit figurer dans le vivier d’instanciation. Ce n’est pas un détail d’implémentation — c’est ce qui permet aux schémas d’axiomes de la mentionner, et c’est exactement ce que la contre-expérience de la section suivante va mettre en défaut.

# --- Cible 1 : p -> p, le plus petit theoreme non axiome du systeme ---
cible = Implication(p, p)
candidats = [p, q, r, cible] + [Implication(a, b) for a in LETTRES for b in LETTRES]
print(f"candidats d'instanciation : {len(candidats)}")
chaine, stats, base = preuve_hilbert(cible, candidats)
for i, (formule, justification) in enumerate(chaine, 1):
    print(f"  {i}. {formule}    [{justification}]")
print("cout de la recherche :", stats)

candidats d'instanciation : 13
  1. ((p=>((p=>p)=>p))=>((p=>(p=>p))=>(p=>p)))    [axiome]
  2. (p=>((p=>p)=>p))    [axiome]
  3. ((p=>(p=>p))=>(p=>p))    [MP]
  4. (p=>(p=>p))    [axiome]
  5. (p=>p)    [MP]
cout de la recherche : {'instances_axiomes': 2535, 'formules_connues': 2169, 'modus_ponens': 153, 'tours': 2, 'secondes': 0.028}

Lecture : cinq étapes, et ce qu’elles coûtent

La preuve trouvée est la preuve classique de p → p : deux instances de A2 et A1, deux modus ponens, et une instance de A1 en route. Cinq formules — c’est le prix syntaxique minimal dans ce système pour un théorème qui paraît trivial.

Le contraste avec la section précédente est le sujet du notebook : l’oracle répond True sur p → p en une fraction de milliseconde, mais ne dit pas pourquoi. Le moteur, lui, paie une recherche (les formules_connues et modus_ponens du dictionnaire stats) pour produire un objet inspectable — et ce coût dépend du vivier d’instanciation, pas seulement de la difficulté logique du théorème.

# --- Chaque formule de la preuve est re-verifiee par les DEUX oracles ---
# Une preuve Hilbert correcte ne contient que des tautologies : c'est verifiable
# etape par etape, independamment du moteur de recherche.
tautologies = {formule: simple.query(vide, base[formule][0]) for formule, _ in chaine}
for formule, verdict in tautologies.items():
    marque = "OK " if verdict else "ECHEC"
    print(f"[{marque}] {formule}")
assert all(tautologies.values()), "une etape de la preuve n'est pas une tautologie"
print("\noracle direct sur la cible :",
      "SimplePlReasoner =", simple.query(vide, cible), "| SatReasoner =", sat.query(vide, cible))
print("etapes de la preuve :", len(chaine))

[OK ] ((p=>((p=>p)=>p))=>((p=>(p=>p))=>(p=>p)))
[OK ] (p=>((p=>p)=>p))
[OK ] ((p=>(p=>p))=>(p=>p))
[OK ] (p=>(p=>p))
[OK ] (p=>p)

oracle direct sur la cible : SimplePlReasoner = True | SatReasoner = True
etapes de la preuve : 5

Ce que le moteur ne trouve pas

Le moteur de la section 3 a trouvé p → p. Cette cible était favorable : le vivier d’instanciation contient p et p → p, donc les schémas se déploient exactement ce qu’il faut.

Toutes les cibles ne se comportent pas ainsi. Prenons le syllogisme hypothétique — une formule que les deux oracles déclarent valide sans hésiter. Le même moteur, avec le même budget d’instanciation, va-t-il la dériver ?

C’est la contre-expérience de cette section : elle mesure une limite, et elle teste au passage l’hypothèse la plus naturelle pour l’expliquer.

# --- Contre-experience : une cible valide que le moteur ne trouve PAS ---
# Le moteur est borne par son vivier d'instanciation : `instances_axiomes` ne
# deploie les schemas que sur `candidats`, et le chainage n'y ajoute jamais les
# formules qu'il derive. Le syllogisme hypothetique est un theoreme du calcul :
# les deux oracles le declarent valide. Le moteur, lui, le derive-t-il ?
cible_syllogisme = Implication(
    Implication(p, q), Implication(Implication(q, r), Implication(p, r))
)


def vivier(sous_formules_supplementaires=()):
    """Meme recette de vivier que la section 3, plus d'eventuelles sous-formules."""
    pool = [p, q, r, cible_syllogisme] + [
        Implication(a, b) for a in LETTRES for b in LETTRES
    ]
    connues = {str(f) for f in pool}
    for f in sous_formules_supplementaires:
        if str(f) not in connues:
            pool.append(f)
            connues.add(str(f))
    return pool


print(f"cible                   : {cible_syllogisme}")
print(f"oracle SimplePlReasoner : {simple.query(vide, cible_syllogisme)}")
print(f"oracle SatReasoner      : {sat.query(vide, cible_syllogisme)}")

# Hypothese 1 : le vivier de la section 3 suffit.
candidats_etroit = vivier()
chaine_etroit, stats_etroit, _ = preuve_hilbert(cible_syllogisme, candidats_etroit)
print(f"\nvivier de la section 3  : |candidats|={len(candidats_etroit)} "
      f"trouvee={chaine_etroit is not None}")
print(f"  cout                  : {stats_etroit}")

# Hypothese 2 : il suffit d'y ajouter les sous-formules de la cible.
sous_formules = [
    Implication(p, q), Implication(q, r), Implication(p, r),
    Implication(Implication(q, r), Implication(p, r)),
]
candidats_elargi = vivier(sous_formules)
chaine_elargi, stats_elargi, _ = preuve_hilbert(cible_syllogisme, candidats_elargi)
print(f"\nvivier + sous-formules  : |candidats|={len(candidats_elargi)} "
      f"trouvee={chaine_elargi is not None}")
print(f"  cout                  : {stats_elargi}")

# Controle : la MEME recette trouve bien p -> p (section 3) -- l'echec ci-dessus
# n'est donc pas un budget global trop court.
cible_controle = Implication(p, p)
candidats_controle = [p, q, r, cible_controle] + [
    Implication(a, b) for a in LETTRES for b in LETTRES
]
chaine_controle, stats_controle, _ = preuve_hilbert(cible_controle, candidats_controle)
print(f"\ncontrole p -> p         : trouvee={chaine_controle is not None} "
      f"etapes={len(chaine_controle)} "
      f"formules_connues={stats_controle['formules_connues']}")

cible                   : ((p=>q)=>((q=>r)=>(p=>r)))
oracle SimplePlReasoner : True
oracle SatReasoner      : True

vivier de la section 3  : |candidats|=13 trouvee=False
  cout                  : {'instances_axiomes': 2535, 'formules_connues': 2713, 'modus_ponens': 178, 'tours': 3, 'secondes': 0.031}

vivier + sous-formules  : |candidats|=14 trouvee=False
  cout                  : {'instances_axiomes': 3136, 'formules_connues': 3342, 'modus_ponens': 206, 'tours': 3, 'secondes': 0.032}

controle p -> p         : trouvee=True etapes=5 formules_connues=2169

Lecture : une limite structurelle, pas un budget trop court

Le verdict est net, et il faut le lire honnêtement : les deux oracles répondent True, le moteur répond False.

Ce n’est pas une contradiction — les trois moteurs ne répondent pas à la même question :

Moteur	Question posée	Réponse	Coût mesuré
`SimplePlReasoner` / `SatReasoner`	« cette formule est-elle valide ? »	oui, sans preuve	quasi instantané
Chaînage avant	« puis-je la dériver des axiomes ? »	non	~2 700 formules, ~180 MP, 3 tours

La cause est lisible dans le moteur lui-même : instances_axiomes ne déploie les schémas que sur candidats, et le chaînage n’y ajoute jamais les formules qu’il dérive. Le vivier reste figé à ce qu’on lui a donné au départ.

L’hypothèse naturelle — « il manque quelques formules, élargissons le vivier » — est testée et réfutée ici : avec les sous-formules de la cible ajoutées, le moteur ne trouve toujours pas. La borne est donc structurelle, pas quantitative.

Le contrôle le confirme par l’autre bout : avec le même budget, p → p est trouvée en 5 étapes. Le moteur n’est pas cassé — il est borné par la forme de sa recherche, et c’est précisément ce qu’un banc d’essai doit rendre visible plutôt que masquer.

4. Séquents de Gentzen : LK, la coupure, et le Hauptsatz

Le calcul des séquents raisonne sur des séquents Γ ⊢ Δ. Dans la version à un seul côté utilisée par FFL (Foundation for Formal Logic), un séquent est un multi-ensemble de formules ⦃φ₁, …, φₙ⦄ et la négation est primitive (atomes positifs p / négatifs ¬p). Les règles utiles ici :

Règle	Forme
identité	`⊢ ⦃p, ¬p⦄` pour un atome `p`
coupure (cut)	de `⊢ Γ + ⦃φ⦄` et `⊢ Δ + ⦃¬φ⦄`, conclure `⊢ Γ + Δ`
contraction	de `⊢ Δ` conclure `⊢ Γ` quand `Δ ⊆ Γ`
conjonction	de `⊢ Γ + ⦃φ⦄` et `⊢ Γ + ⦃ψ⦄`, conclure `⊢ Γ + ⦃φ ⋏ ψ⦄`
disjonction	de `⊢ Γ + ⦃φ, ψ⦄`, conclure `⊢ Γ + ⦃φ ⋎ ψ⦄`

Une dérivation est un arbre ; sa hauteur (Derivation.height) et sa taille (nombre de nœuds) sont deux mesures différentes du même objet. La coupure est l’analogue structurel du modus ponens : elle permet de réutiliser un lemme, au prix d’une formule qui n’est pas sous-formule de la conclusion.

Le Hauptsatz (théorème d’élimination des coupures) affirme que toute dérivation se transforme en une dérivation sans coupure de la même conclusion. FFL le fournit comme théorème Derivation.Canonical.constructiveHauptsatz, dont la sortie est un sous-type : la dérivation éliminée et le témoin IsCutFree.

Où vit le code Lean de ce notebook. Le corpus FFL est consommé en CONSUMER_PINNÉ (verdict du pilote #15520) : aucun module upstream n’est vendé ni adapté. Les autres tranches de l’EPIC adossent leur versant Lean à un module de pont versionné dans formal_logic_lean/FormalLogic/ ; cette tranche ne touche pas au lake — ses deux fichiers d’index (FormalLogic.lean, README.md) sont sous claim actif d’une autre lane (check_lane_claim, verdict BLOCKED, 2026-09-25). Le langage PL, la mesure de taille et les deux dérivations sont donc définis dans le notebook et soumis au noyau par lake env lean : les objets du noyau invoqués (Derivation, cut, IsCutFree, constructiveHauptsatz) sont, eux, exactement ceux du corpus épinglé, et la cellule de provenance le mesure avant de compiler.

# --- Helpers WSL + provenance mesuree + build du module (patron Tweety-02d / 5e) ---
import json as _json
import shutil
import subprocess
import tempfile

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(chemin):
    """Chemin Windows -> chemin WSL /mnt/..."""
    win = chemin.resolve().as_posix()
    return "/mnt/" + win[0].lower() + win[2:]


def run_wsl(commande, 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 4-5 exigent un hote Windows + WSL."
        )
    return subprocess.run(
        ["wsl", "-e", "bash", "-lc", commande],
        capture_output=True, text=True, encoding="utf-8", errors="replace",
        timeout=timeout,
    )


# 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 = {paquet["name"]: paquet["rev"] for paquet in manifest["packages"]}
print("Provenance mesuree (git rev-parse dans .lake/packages) :")
for paquet in ["Foundation", "mathlib", "ProvabilityLogic"]:
    res = run_wsl(f"git -C {to_wsl(LAKE_DIR)}/.lake/packages/{paquet} rev-parse HEAD", timeout=120)
    mesure = (res.stdout or "").strip()
    if res.returncode != 0 or not mesure:
        raise RuntimeError(
            f"paquet {paquet} illisible dans .lake/packages (exit {res.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[paquet] else "DERIVE"
    print(f"  {paquet:<18s} {mesure[:12]}  [{statut}]")
    assert mesure == pins_attendus[paquet], f"{paquet} a derive : {mesure[:12]}"

# 2) Build cible : le module EXACT que ce notebook importe (idempotent)
CIBLE = "Foundation.FirstOrder.Hauptsatz"
res = run_wsl(f"cd {to_wsl(LAKE_DIR)} && lake build {CIBLE}", timeout=7200)
sortie = (res.stdout or "") + (res.stderr or "")
print(f"\n$ lake build {CIBLE}")
print("\n".join(sortie.strip().splitlines()[-3:]) or "(deja a jour)")
assert res.returncode == 0, f"lake build {CIBLE} a echoue -- voir sortie ci-dessus"
print(f"\nBUILD OK : {CIBLE} compile sur les pins ci-dessus.")

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

$ lake build Foundation.FirstOrder.Hauptsatz
info: Foundation/FirstOrder/Basic/BinderNotation.lean:805:0: “#0 = #1” : Semiformula ?m.16 ?m.17 ?m.18
info: Foundation/FirstOrder/Basic/BinderNotation.lean:817:0: ∀¹ ((“#0 = #1”) 🡒 ∀¹ ((“#0 = #3”) 🡒 (“#1 = #0”))) : Semiformula ?m.43 ?m.44 ?m.3
Build completed successfully (962 jobs).

BUILD OK : Foundation.FirstOrder.Hauptsatz compile sur les pins ci-dessus.

Lecture : provenance mesurée, build réel

Les trois rev-parse comparent le contenu réel de .lake/packages/ aux révisions déclarées dans lake-manifest.json : si un paquet dérivait (fetch manuel, fork divergent), l’assertion arrêterait le notebook. Mesurer plutôt que déclarer — sans ce contrôle, le notebook compilerait contre une révision inconnue tout en affichant la bonne.

Le lake build qui suit compile le module exact que les cellules suivantes importent (Foundation.FirstOrder.Hauptsatz) : c’est de lui que viennent Derivation, IsCutFree et constructiveHauptsatz. Le timeout est large (la première compilation du lake est longue — mathlib puis Foundation) ; les exécutions suivantes sont incrémentales.

# --- run_lean + tour d'API : les objets FFL reels, verifies par le noyau ---
def run_lean(source):
    """Ecrit source dans un temporaire et le fait verifier par le noyau Lean
    natif du lake (lake env lean = toolchain + LEAN_PATH du pin)."""
    dossier = pathlib.Path(tempfile.mkdtemp(prefix="tweety02e_"))
    fichier = dossier / "scratch.lean"
    fichier.write_text(source, encoding="utf-8")
    res = run_wsl(f"cd {to_wsl(LAKE_DIR)} && lake env lean {to_wsl(fichier)}", timeout=3600)
    return (res.stdout or "") + (res.stderr or ""), res.returncode


tour_api = """import Foundation.FirstOrder.Hauptsatz

open FFL FirstOrder

#check @FFL.FirstOrder.Derivation
#check @FFL.FirstOrder.Derivation.identity
#check @FFL.FirstOrder.Derivation.cut
#check @FFL.FirstOrder.Derivation.height
#check @FFL.FirstOrder.Derivation.IsCutFree
#check @FFL.FirstOrder.Derivation.Canonical.constructiveHauptsatz
#check FFL.FirstOrder.Sequent
#check FFL.FirstOrder.Proposition
"""

sortie, code_retour = run_lean(tour_api)
print(sortie)
print(f"[exit {code_retour}]")
assert code_retour == 0, "le tour d'API doit compiler sans erreur"

@Derivation : {L : Language} → Sequent L → Type u_1
@Derivation.identity : {L : Language} →
  {k : ℕ} → (r : L.Rel k) → (v : Fin k → Semiterm L ℕ 0) → ⊢ᴸᴷ¹ ⦃Semiformula.rel r v⦄ + ⦃Semiformula.nrel r v⦄
@Derivation.cut : {L : Language} →
  {Γ : Sequent L} → {φ : Proposition L} → {Δ : Sequent L} → ⊢ᴸᴷ¹ Γ + ⦃φ⦄ → ⊢ᴸᴷ¹ Δ + ⦃∼φ⦄ → ⊢ᴸᴷ¹ Γ + Δ
@Derivation.height : {L : Language} → {Δ : Sequent L} → ⊢ᴸᴷ¹ Δ → ℕ
@Derivation.IsCutFree : {L : Language} → {Γ : Sequent L} → ⊢ᴸᴷ¹ Γ → Prop
@Derivation.Canonical.constructiveHauptsatz : {L : Language} →
  [L.DecidableEq] → [L.Encodable] → {Γ : Sequent L} → ⊢ᴸᴷ¹ Γ → { d // d.IsCutFree }
FFL.FirstOrder.Sequent.{u_1} (L : Language) : Type u_1
FFL.FirstOrder.Proposition.{u_1} (L : Language) : Type u_1

[exit 0]

Lecture : ce que le noyau vient de vérifier

Chaque #check est une vérification de type : le noyau confirme que Derivation est bien une famille inductive indexée par les séquents, que cut prend deux dérivations et en rend une troisième, que height est une fonction de Derivation vers ℕ, et que constructiveHauptsatz rend un sous-type {d // IsCutFree d} — donc la dérivation et la preuve qu’elle est sans coupure, dans le même objet.

# --- Preambule Lean : langage propositionnel concret + deux derivations du meme sequent ---
LEAN_PREAMBLE = r'''
import Foundation.FirstOrder.Hauptsatz

open FFL FirstOrder Semiformula

namespace Tweety02e

/-- Trois lettres propositionnelles, comme relations d'arité 0. -/
inductive Letter : ℕ → Type
  | p : Letter 0
  | q : Letter 0
  | r : Letter 0
  deriving DecidableEq

@[reducible]
def PL : Language where
  Func := fun _ => PEmpty
  Rel := Letter

instance (k) : DecidableEq (PL.Func k) := fun a b => by rcases a

instance (k) : Encodable (PL.Func k) := IsEmpty.toEncodable

instance (k) : DecidableEq (PL.Rel k) := inferInstance

instance (k) : Encodable (PL.Rel k) where
  encode := fun x => match x with
    | .p => 0
    | .q => 1
    | .r => 2
  decode := fun n =>
    match k with
    | 0 =>
      match n with
      | 0 => some .p
      | 1 => some .q
      | 2 => some .r
      | _ => none
    | _ => none
  encodek := fun x => by
    match x with
    | .p => rfl
    | .q => rfl
    | .r => rfl

/-- Une lettre comme formule atomique. -/
abbrev atom (l : Letter 0) : Proposition PL :=
  Semiformula.rel l (fun i : Fin 0 => i.elim0)

open FFL.FirstOrder.Derivation

/-- Nombre de nœuds d'une dérivation LK (motifs qualifiés : `verum` est aussi
un constructeur de `Semiformula` ; appels récursifs par le nom nu, la notation
point cherchant d'abord dans `FFL.FirstOrder.Derivation`). -/
def size {Γ : Sequent PL} : ⊢ᴸᴷ¹ Γ → ℕ
  |    Derivation.identity _ _ => 1
  |       Derivation.cut dp dn => size dp + size dn + 1
  | Derivation.contraction d _ => size d + 1
  |           Derivation.verum => 1
  |            Derivation.or d => size d + 1
  |       Derivation.and dp dq => size dp + size dq + 1
  |           Derivation.all d => size d + 1
  |           Derivation.exs d => size d + 1

/-- Le séquent `p, ¬p` par l'axiome d'identité — sans coupure.
Le langage est nommé (`L := PL`) : `L` et `k` sont implicites dans
`Derivation.identity` et ne s'infèrent pas du type attendu. -/
def dIdentite : ⊢ᴸᴷ¹ ⦃atom .p, ∼atom .p⦄ :=
  Derivation.identity (L := PL) Letter.p (fun i : Fin 0 => i.elim0)

/-- Le même séquent, dérivé avec une coupure sur `¬p`.
La coupure se lit sur les types : la prémisse gauche est `Γ + ⦃φ⦄` avec
`φ := ¬p`, la droite est `Δ + ⦃¬φ⦄` avec `Δ := ⦃¬p⦄`. `eta` rend
précisément `⦃φ, ¬φ⦄`, donc la prémisse droite est `eta (¬p)` — et la
conclusion `Γ + Δ` retombe sur `⦃p, ¬p⦄`. Aucun `cast` n'est nécessaire :
`⬝ ▸ ⬝` est un `abbrev` sur `Eq.ndrec`, qui ne se réduit pas sous `#eval`
quand la preuve d'égalité n'est pas `rfl`. -/
def dCoupure : ⊢ᴸᴷ¹ ⦃atom .p, ∼atom .p⦄ :=
  Derivation.cut (Γ := ⦃atom .p⦄) (Δ := ⦃∼atom .p⦄) (φ := ∼atom .p)
    (Derivation.identity (L := PL) Letter.p (fun i : Fin 0 => i.elim0))
    (Derivation.eta (∼atom .p))

end Tweety02e
'''

mesures = LEAN_PREAMBLE + '''
open Tweety02e
#eval dIdentite.height
#eval dCoupure.height
#eval size dIdentite
#eval size dCoupure
'''
sortie, code_retour = run_lean(mesures)
print(sortie)
print(f"[exit {code_retour}]")
assert code_retour == 0, "le preambule Lean doit compiler sans erreur"

0
2
1
4

[exit 0]

Lecture : deux preuves du même séquent, deux mesures

Les quatre nombres imprimés mesurent le même énoncé ⊢ ⦃p, ¬p⦄ par deux objets différents :

la dérivation par identité est une feuille : hauteur 0, taille 1 ;
la dérivation par coupure coupe ¬p entre l’axiome d’identité et eta (¬p) (une identité sous une contraction) : hauteur 2, taille 4.

La coupure n’a rien ajouté à ce que l’identité donnait déjà — c’est une redondance structurelle, exactement ce que le Hauptsatz supprime. Sur des formules composites, la coupure n’est pas redondante : elle peut réduire la hauteur d’un arbre en réutilisant un lemme (c’est son intérêt), et l’élimination la paiera en taille.

# --- Elimination des coupures : le Hauptsatz comme THEOREME, pas comme procedure ---
elimination = LEAN_PREAMBLE + '''
open Tweety02e
open FFL.FirstOrder.Derivation

/-- La dérivation sans coupure produite par le Hauptsatz constructif. -/
def dSansCoupure : ⊢ᴸᴷ¹ ⦃atom .p, ∼atom .p⦄ :=
  (Derivation.Canonical.constructiveHauptsatz dCoupure).1

/-- Le temoin de non-coupure, extrait du meme theoreme (deuxieme composante). -/
example : Derivation.IsCutFree dSansCoupure :=
  (Derivation.Canonical.constructiveHauptsatz dCoupure).2

#eval dSansCoupure.height
#eval size dSansCoupure
#eval dCoupure.height
#eval size dCoupure
#print axioms Derivation.Canonical.constructiveHauptsatz
'''
sortie, code_retour = run_lean(elimination)
print(sortie)
print(f"[exit {code_retour}]")
assert code_retour == 0, "l'elimination des coupures doit compiler sans erreur"

6
7
2
4
'FFL.FirstOrder.Derivation.Canonical.constructiveHauptsatz' depends on axioms: [propext, Classical.choice, Quot.sound]

[exit 0]

Lecture : ce que le théorème rend, et ce qu’il coûte

constructiveHauptsatz ne renvoie pas une promesse : il renvoie la dérivation éliminée (dSansCoupure) et la preuve IsCutFree de celle-ci — les deux composantes du sous-type. Le #eval compare l’objet d’origine et l’objet transformé :

dérivation	hauteur	taille
`dIdentite` — axiome d’identité, sans coupure	0	1
`dCoupure` — avec coupure	2	4
`dSansCoupure` — rendue par le Hauptsatz	6	7

Le théorème n’est pas un optimiseur : sur cette instance il rend une dérivation plus haute (2 → 6) et plus grosse (4 → 7) que celle qu’il remplace. C’est le résultat attendu, et c’est le point pédagogique : le Hauptsatz garantit la suppression des coupures, jamais l’économie de l’arbre.

Le #print axioms complète la lecture en nommant ce sur quoi le théorème repose : propext, Classical.choice, Quot.sound. constructiveHauptsatz rend un témoin calculable — le #eval aboutit — mais sa preuve n’est pas sans axiomes : les trois axiomes classiques de Mathlib sont bien là.

Le point d’ensemble est que l’élimination des coupures est un théorème du noyau, pas un algorithme décrit dans un commentaire. Un étudiant peut l’invoquer, mesurer ses effets, et vérifier que la conclusion est inchangée — exactement comme on utilise un lemme de Mathlib.

5. Bilan croisé : trois calculs, trois mesures

Question	Moteur	Objet produit	Mesure du jour
« Pourquoi `p → p` ? »	Hilbert (axiomes + MP)	une liste de 5 formules justifiées	~2 500 instances d’axiomes, ~150 MP, quelques dizaines de ms
« Pourquoi `⊢ ⦃p, ¬p⦄` ? »	LK (séquents)	un arbre, avec ou sans coupure	identité 0/1 · coupure 2/4 · après élimination 6/7 (hauteur/taille)
« Est-ce valide ? »	`SimplePlReasoner` / `SatReasoner`	un verdict `True`/`False`	quasi instantané, sans preuve

Deux résultats négatifs mesurés dans ce notebook, et ils comptent autant que les positifs :

La recherche Hilbert ne trouve pas tout ce qu’elle « pourrait » : le syllogisme hypothétique (p → q) → ((q → r) → (p → r)) n’est pas trouvé dans le budget d’instanciation du moteur, alors que l’oracle le déclare valide immédiatement. La cause est le vivier d’instanciation (le moteur n’instancie pas les schémas sur les formules qu’il dérive), pas la logique — et l’élargir aux sous-formules de la cible ne suffit pas : la section 3 a testé cette hypothèse et l’a réfutée par la mesure.
L’élimination des coupures n’est pas gratuite — et ce n’est pas non plus une simplification : sur ce cas minimal la dérivation rendue par le théorème est plus haute (2 → 6) et plus grosse (4 → 7) que celle qu’elle remplace. Le théorème garantit l’existence d’une dérivation sans coupure, jamais qu’elle soit plus petite : supprimer la coupure ne fait pas disparaître la structure qu’elle condensait.

Ce que le notebook établit, en une phrase : décider est bon marché et aveugle ; prouver est coûteux, inspectable, et mesurable — et la taille d’une preuve dépend du système de calcul choisi pour la représenter.

Exercice 1 : calibrer la taille des preuves Hilbert

Contexte

Le moteur de la section 3 a produit p → p en 5 étapes. Toutes les cibles ne se valent pas : certaines sont des instances d’axiome (une seule ligne), d’autres exigent une vraie fermeture par modus ponens.

Objectifs

Mesurer le nombre d’étapes pour les trois cibles suivantes, avec le même vivier d’instanciation : p → (q → p), p → p, (p → q) → (p → q)
Pour chaque cible, comparer le nombre d’étapes trouvé à stats["formules_connues"] : la preuve est-elle un objet rare dans la base dérivée ?
Expliquer, sans exécuter, pourquoi p → (q → p) ne peut pas se trouver en plus d’une étape

Indices : - réutilisez preuve_hilbert(cible, candidats) — la cible doit figurer dans candidats ; - une instance d’axiome est présente dès l’initialisation : le tour de fermeture n’est même pas nécessaire ; - str(cible) sert de clé dans base : l’égalité de formules passe par toString().

# --- Exercice 1 : trois cibles, trois tailles de preuve ---
# TODO etudiant
# Etape 1 : boucler sur les trois cibles et appeler preuve_hilbert(cible, candidats)
# Etape 2 : afficher len(chaine) et stats["formules_connues"] pour chaque cible
# Etape 3 : expliquer en commentaire pourquoi la premiere cible tient en une seule ligne
print("Exercice a completer")

Exercice a completer

Exercice 2 : une dérivation LK sans coupure, mesurée

Contexte

La section 4 n’a mesuré que le cas minimal ⊢ ⦃p, ¬p⦄. Le témoin vraiment intéressant est un séquent composite, sans coupure : ⊢ ⦃¬p, ¬q, p ⋏ q⦄.

Objectifs

Construire en Lean la dérivation dConjonction : ⊢ᴸᴷ¹ ⦃∼atom .p, ∼atom .q, atom .p ⋏ atom .q⦄ — la règle Derivation.and exige deux dérivations du même contexte Γ, l’une de ⦃atom .p⦄, l’autre de ⦃atom .q⦄, chacune obtenue par contraction d’un axiome d’identité (indice : Derivation.contraction prend une preuve de Δ et une inclusion Δ ⊆ Γ)
Mesurer #eval dConjonction.height et #eval dConjonction.size
Vérifier que l’objet est bien sans coupure : example : Derivation.IsCutFree dConjonction — et expliquer pourquoi le Hauptsatz, appliqué à cet objet, ne peut pas faire mieux

Indices : - Derivation.and dp dq attend dp : ⊢ᴸᴷ¹ Γ + ⦃φ⦄ et dq : ⊢ᴸᴷ¹ Γ + ⦃ψ⦄ avec le même Γ ; - l’axiome d’identité donne ⦃p, ¬p⦄ — le passer à ⦃¬p, ¬q, p⦄ est une inclusion de multi-ensembles (perte de ¬q), donc une contraction ; - IsCutFree est une famille inductive : ses constructeurs suivent exactement les règles sans coupure (identity, contraction, and, or, …) — il n’existe aucun constructeur pour cut.

# --- Exercice 2 : derivation LK composite sans coupure ---
# TODO etudiant
# Etape 1 : dConjonction via Derivation.and de deux contractions d'axiomes d'identite
# Etape 2 : out, rc = run_lean(LEAN_PREAMBLE + "...") ; assert rc == 0
# Etape 3 : mesurer height/size, puis expliquer le role de la contraction dans les inclusions
print("Exercice a completer")

Exercice a completer

Exercice 3 : lire les axiomes d’un théorème

Contexte

#print axioms est l’instrument qui distingue deux versions du même théorème dans FFL : constructiveHauptsatz (computable) et hauptsatz (déclarée noncomputable). La différence n’est pas cosmétique — elle dit ce sur quoi repose la preuve.

Objectifs

Écrire un snippet Lean qui imprime #print axioms pour Derivation.Canonical.constructiveHauptsatz et pour Derivation.Canonical.hauptsatz
Comparer les deux listes : quel axiome apparaît dans l’une et pas dans l’autre ?
Exécuter #eval dCoupure.height après avoir remplacé constructiveHauptsatz par hauptsatz dans l’extraction du témoin — que se passe-t-il, et pourquoi ?

Indices : - #print axioms accepte un nom pleinement qualifié : #print axioms FFL.FirstOrder.Derivation.Canonical.hauptsatz ; - un terme noncomputable ne peut pas être évalué par #eval : l’erreur le dit ; - la question 3 se répond en lisant le message d’erreur, pas en le contournant.

# --- Exercice 3 : comparer les axiomes des deux Hauptsatz ---
# TODO etudiant
# Etape 1 : ecrire le snippet Lean avec les deux #print axioms
# Etape 2 : afficher la sortie ; identifier l'axiome supplementaire de la version noncomputable
# Etape 3 : tenter #eval sur un terme extrait de hauptsatz et lire l'erreur du noyau
print("Exercice a completer")

Exercice a completer

Conclusion

Ce notebook a posé une question — comment calcule-t-on une preuve ? — à trois moteurs, et mesuré leurs réponses sur la même micro-théorie {p, q, r} :

Hilbert fournit l’objet le plus élémentaire : une suite de formules, chacune justifiée par un axiome ou un modus ponens. Sa recherche a un coût mesurable, et son vivier d’instanciation en est le paramètre dominant — un résultat négatif du notebook ((p → q) → ((q → r) → (p → r)) non trouvé) le montre honnêtement.
LK fournit l’objet le plus structuré : un arbre, dont la hauteur et la taille se mesurent, et dont la règle de coupure est l’analogue structurel du modus ponens. L’élimination des coupures est un théorème du noyau Lean (constructiveHauptsatz), qui rend la dérivation transformée et le témoin IsCutFree.
Les oracles (SimplePlReasoner, SatReasoner) fournissent la réponse la plus rapide — et aucune preuve. Ce sont eux qui vérifient, étape par étape, que la preuve Hilbert trouvée ne dérive que des tautologies.

La leçon transversale : la taille d’une preuve n’est pas une propriété du théorème, mais du système de calcul qui la représente. p → p coûte cinq formules à Hilbert, un nœud à LK, et zéro à l’oracle — trois façons de « savoir » la même chose.

Aller plus loin

Tweety-02d — le laboratoire FOL croisé (Tweety répond, Lean certifie) dont ce notebook est le prolongement structurel ;
Tweety-5e — trois formules-témoins lues par trois moteurs (Tweety, recomptage Python, kernel Lean) ;
Tweety-3b — le laboratoire modal : schémas K/T/4/5 énumérés sur 512 cadres Kripke puis certifiés par le pont FormalLogic.ModalBridge ;
Foundation (FFL) — Foundation/FirstOrder/Hauptsatz.lean, d’où vient constructiveHauptsatz, et Foundation/FirstOrder/Basic/CutFree.lean pour IsCutFree ;
Lean — série SymbolicAI — les tactiques qui construisent ces arbres à la main (niveau 1 à 5).

Retour au sommet

Objectifs pédagogiques

Prérequis

Durée estimée : 45 minutes

1. La question du labo

Lecture : deux oracles réels, pas une simulation

2. Les axiomes de Hilbert, vérifiés par l’oracle

Lecture : « tautologie » est un verdict sémantique

3. Chercher une preuve : chaînage avant

Première cible : p → p

Lecture : cinq étapes, et ce qu’elles coûtent

Ce que le moteur ne trouve pas

Lecture : une limite structurelle, pas un budget trop court

4. Séquents de Gentzen : LK, la coupure, et le Hauptsatz

Lecture : provenance mesurée, build réel

Lecture : ce que le noyau vient de vérifier

Lecture : deux preuves du même séquent, deux mesures

Lecture : ce que le théorème rend, et ce qu’il coûte

5. Bilan croisé : trois calculs, trois mesures

Exercice 1 : calibrer la taille des preuves Hilbert

Contexte

Objectifs

Exercice 2 : une dérivation LK sans coupure, mesurée

Contexte

Objectifs

Exercice 3 : lire les axiomes d’un théorème

Contexte

Objectifs

Conclusion

Aller plus loin

Première cible : `p → p`