Tweety-02d — Labo FOL : Tweety répond, Lean certifie

Série Tweety — laboratoires croisés Java ↔︎ Lean (EPIC #15066, Tranche B, issue #16877). Un même syllogisme, deux moteurs : le raisonneur Tweety (Java, via JPype) exécute la logique du premier ordre sur une micro-théorie ; le lake formal_logic_lean (corpus FFL épinglé) certifie les mêmes verdicts comme théorèmes ou contre-modèles vérifiés par le noyau Lean.

Navigation : Tweety-02-Basic-Logics-Python (FOL exécutée) · Tweety-02c-FOL-CSharp (port C#) · Tweety-5e-Propositional-Lab-Lean (labo propositionnel) · README

Objectifs pédagogiques

Exécuter un raisonnement FOL réel avec Tweety (SimpleFolReasoner) sur une micro-théorie à deux individus
Distinguer conséquence (TRUE : la requête vaut dans tout modèle) et non-conséquence (FALSE : au moins un modèle falsifie) — sans jamais confondre FALSE avec « la négation est prouvée »
Voir échouer la fusion à témoin unique : deux existentiels conséquences dont la conjonction ne l’est pas, parce que les témoins sont distincts
Certifier chaque verdict côté Lean : conséquences sémantiques quantifiées sur toutes les structures, contre-modèle fini exhibé et revérifié par le noyau
Mesurer la provenance du corpus Formalized Formal Logic (pins git rev-parse) avant toute certification

Prérequis

Tweety-01-Setup-Python exécuté (JVM, JARs, JPype) — le dossier libs/ du répertoire Tweety
Notions FOL : Tweety-02 (prédicats, quantificateurs)
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 : compagnon FOL du labo propositionnel Tweety-5e — même patron (moteur exécuté ↔︎ noyau certifiant), un étage au-dessus en expressivité : quantificateurs, témoins, contre-modèles à plusieurs éléments.

1. La question du labo

Le syllogisme « tous les hommes sont mortels, Socrate est un homme, donc Socrate est mortel » est l’exemple hello-world de la FOL. Mais dès qu’on pose la bonne micro-théorie — deux individus, quatre prédicats — six requêtes intéressantes se présentent, et la sixième est un piège classique.

Ce labo aligne trois lectures indépendantes sur exactement la même théorie :

Tweety (JVM, SimpleFolReasoner) exécute : six verdicts TRUE/FALSE ;
un contrôle croisé Python énumère les 256 interprétations du domaine à deux individus ;
Lean (lake formal_logic_lean, corpus FFL épinglé) certifie : les TRUE deviennent des théorèmes quantifiés sur toutes les structures, les FALSE deviennent des contre-modèles exhibés.

La symétrie à retenir dès maintenant :

Verdict Tweety	Statut mathématique	Ce que Lean en fait
`TRUE`	conséquence sémantique `KB ⊨ φ`	théorème (preuve, toutes structures)
`FALSE`	non-conséquence `¬(KB ⊨ φ)`	contre-modèle fini exhibé et vérifié
—	négation `KB ⊨ ¬φ`	aucun rapport avec le `FALSE` ci-dessus : le monde est ouvert

La dernière ligne est l’erreur de lecture la plus répandue sur les raisonners FOL : nous y reviendrons après les exécutions, preuves en main.

# --- Initialisation JVM Tweety (helper partage de la serie) + imports FOL ---
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 (JDK portable, 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 Constant, Predicate, Variable
from org.tweetyproject.logics.fol.syntax import (
    FolBeliefSet, FolAtom, Implication, Conjunction,
    ForallQuantifiedFormula, ExistsQuantifiedFormula, FolFormula,
)
from org.tweetyproject.logics.fol.reasoner import SimpleFolReasoner, FolReasoner

reasoner = SimpleFolReasoner()
FolReasoner.setDefaultReasoner(reasoner)
print("Reasoner FOL actif :", reasoner.getClass().getName())

--- Initialisation Tweety ---
Bibliotheques natives: native/
JVM demarree avec 42 JARs.
Reasoner FOL actif : org.tweetyproject.logics.fol.reasoner.SimpleFolReasoner

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

La sortie atteste trois choses, mesurées et non déclarées :

la JVM démarre avec les JARs Tweety 1.30 du dossier libs/ (le helper les compte à l’initialisation), sur le JDK portable détecté automatiquement ;
le raisonneur actif est org.tweetyproject.logics.fol.reasoner.SimpleFolReasoner — le raisonneur d’énumération de Herbrand du module FOL de Tweety, celui-là même que le port C# du Tweety-02c exécute via IKVM ;
si l’un de ces éléments manque (JDK, JARs, JVM), la cellule précédente échoue explicitement : aucun chemin de ce notebook ne continue sans JVM réelle — pas de sortie fabriquée.

Classe importée	Rôle	Analogue FFL (section 4)
`Predicate` / `Constant` / `Variable`	signature : symboles et termes	`Language` (familles `Func`/`Rel` par arité)
`FolAtom`, `Implication`, `Conjunction`	constructeurs de formules	`Semiformula` (`rel`, `🡒`, `⋏`)
`ForallQuantifiedFormula`, `ExistsQuantifiedFormula`	quantification	`∀¹`, `∃¹`
`FolBeliefSet`	base de croyances	`Theory L` (un `Set` de phrases)
`SimpleFolReasoner`	répond `KB ⊨ φ ?` par énumération	`Consequence T σ` + `consequence_iff`

2. La micro-théorie : deux individus, quatre prédicats

Prédicat (arité 1)	Sens	Fait posé
`Homme(X)`	X est un homme	`Homme(socrate)`
`Mortel(X)`	X est mortel	— (dérivé par l’axiome)
`Grec(X)`	X est grec	`Grec(socrate)`
`Philosophe(X)`	X est philosophe	`Philosophe(platon)`

Constantes : socrate et platon — deux individus distincts, rien de plus. Axiome universel : ∀X (Homme(X) ⇒ Mortel(X)).

La base de croyances KB compte donc 4 formules : l’universel et trois faits.

Pourquoi cette théorie, et pas juste le syllogisme ? Parce qu’elle sépare deux témoins : le témoin de ∃X Grec(X) est socrate, celui de ∃X Philosophe(X) est platon — et rien, dans la KB, ne dit qu’un même individu porte les deux propriétés. C’est le piège de la fusion à témoin unique ∃X (Grec(X) ∧ Philosophe(X)), cœur pédagogique de ce labo. Les six requêtes :

#	Requête	Attendu	Pourquoi
1	`Mortel(socrate)`	TRUE	le syllogisme (universel + fait, modus ponens)
2	`Homme(platon)`	FALSE	contrôle négatif : aucun fait sur platon
3	`∃X Grec(X)`	TRUE	témoin : socrate
4	`∃X Philosophe(X)`	TRUE	témoin : platon
5	`∃X (Grec(X) ∧ Philosophe(X))`	FALSE	témoins distincts, aucun individu unifié
6	`∀X Mortel(X)`	FALSE	platon n’est pas homme : l’axiome ne s’applique pas

# --- Construction de la KB par l'API de constructeurs (FOL non typée, patron Tweety-02c) ---
Homme, Mortel, Grec, Philosophe = (
    Predicate(nom, 1) for nom in ["Homme", "Mortel", "Grec", "Philosophe"]
)
socrate = Constant("socrate")
platon = Constant("platon")
X = Variable("X")

hommeX = FolAtom(Homme, X)
mortelX = FolAtom(Mortel, X)
axiome = ForallQuantifiedFormula(Implication(hommeX, mortelX), X)

kb = FolBeliefSet()
for f in [axiome,
          FolAtom(Homme, socrate),
          FolAtom(Grec, socrate),
          FolAtom(Philosophe, platon)]:
    kb.add(JObject(f, FolFormula))

print("Axiome       :", axiome)
print("KB Tweety    :", kb)
print("Taille de KB :", kb.size(), "formules")

Axiome       : forall X: ((Homme(X)=>Mortel(X)))
KB Tweety    : { Grec(socrate), Homme(socrate), Philosophe(platon), forall X: ((Homme(X)=>Mortel(X))) }
Taille de KB : 4 formules

Lecture : la théorie est en place

La sortie montre l’axiome rendu par Tweety — la quantification universelle y apparaît avec sa variable liée — et la KB comptant ses 4 formules : l’universel, Homme(socrate), Grec(socrate) et Philosophe(platon).

Deux choix de construction, hérités du Tweety-02c :

API de constructeurs plutôt que FolParser : le parseur exige une signature complètement déclarée (chaque foncteur, chaque constante) avant de lire la moindre formule ; les constructeurs rendent la signature visible ligne à ligne — c’est ce que la section 4 mirrorera côté Lean avec les familles SocRel/SocFunc ;
FOL non typée (Predicate(nom, 1), constantes sans sort) : la FOL monosorte de ce labo est exactement celle que la sémantique FFL des structures définit — un seul domaine, des prédicats par arité.

# --- Les six requetes du labo : verdicts du reasoner Tweety ---
requetes = [
    ("Mortel(socrate)", FolAtom(Mortel, socrate), True),
    ("Homme(platon)", FolAtom(Homme, platon), False),
    ("exists X Grec(X)", ExistsQuantifiedFormula(FolAtom(Grec, X), X), True),
    ("exists X Philosophe(X)", ExistsQuantifiedFormula(FolAtom(Philosophe, X), X), True),
    ("exists X (Grec(X) && Philosophe(X))",
     ExistsQuantifiedFormula(Conjunction(FolAtom(Grec, X), FolAtom(Philosophe, X)), X), False),
    ("forall X Mortel(X)", ForallQuantifiedFormula(FolAtom(Mortel, X), X), False),
]

print("Requete                              Tweety   Attendu  Verdict")
print("-" * 66)
for label, q, attendu in requetes:
    res = bool(reasoner.query(kb, JObject(q, FolFormula)))
    ok = "OK" if res == attendu else f"ECART (attendu {attendu})"
    print(f"{label:<38s}{'TRUE' if res else 'FALSE':>7s}  {str(attendu):>8s}  {ok}")

assert all(bool(reasoner.query(kb, JObject(q, FolFormula))) == att for _, q, att in requetes)
print("\n6/6 verdicts conformes a la lecture semantique attendue.")

Requete                              Tweety   Attendu  Verdict
------------------------------------------------------------------
Mortel(socrate)                          TRUE      True  OK
Homme(platon)                           FALSE     False  OK
exists X Grec(X)                         TRUE      True  OK
exists X Philosophe(X)                   TRUE      True  OK
exists X (Grec(X) && Philosophe(X))     FALSE     False  OK
forall X Mortel(X)                      FALSE     False  OK

6/6 verdicts conformes a la lecture semantique attendue.

Lecture : ce que `FALSE` veut dire — et ce qu’il ne veut PAS dire

Les 6/6 verdicts collent au tableau de la section 2. Trois lectures, une par statut :

TRUE = conséquence. Mortel(socrate) vaut dans tout modèle de la KB — Tweety le trouve par énumération de Herbrand (instanciation de l’universel sur les constantes, modus ponens), et la section 4 en fera un théorème quantifié sur toutes les structures.

FALSE = non-conséquence — une preuve d’existence, pas une absence d’information. La réponse FALSE signifie exactement : il existe au moins un modèle de la KB qui falsifie la requête. C’est une affirmation mathématique forte, et la section 5 l’honore en exhibant ce contre-modèle.

L’erreur à ne jamais commettre (monde ouvert vs monde fermé). FALSE sur forall X Mortel(X) ne dit PAS que Tweety a prouvé ¬∀X Mortel(X), ni « il existe un immortel », ni « platon est immortel ». La KB ne contient aucune information sur d’éventuels autres individus : en FOL classique le domaine est ouvert — des éléments inconnus peuvent exister, et seuls les modèles décident. La négation KB ⊨ ¬φ est une conséquence elle aussi, qu’il faudrait prouver séparément ; la non-conséquence de φ ne l’entraîne pas. Un système qui confondrait les deux appliquerait une closed-world assumption que la FOL classique n’a pas.

La fusion, cœur du labo. ∃X Grec(X) est TRUE (témoin socrate), ∃X Philosophe(X) est TRUE (témoin platon) — mais ∃X (Grec(X) ∧ Philosophe(X)) est FALSE : les deux existentiels ont élu des témoins distincts, et aucun fait n’identifie un individu portant les deux propriétés. Le pas « deux existentiels vrais, donc leur conjonction unifiée est vraie » est invalide en FOL.

3. Le duel des témoins

Requête	Témoin élu	Atomes exigés
`∃X Grec(X)`	`socrate`	`Grec(socrate)`
`∃X Philosophe(X)`	`platon`	`Philosophe(platon)`
`∃X (Grec(X) ∧ Philosophe(X))`	aucun	un même `x` avec les deux

Un quantificateur existentiel vit dans son monde : chaque ∃ choisit son témoin, indépendamment des autres. La conjonction sous un seul ∃ exige un témoin unique portant les deux propriétés simultanément — une exigence strictement plus forte que la juxtaposition des deux existentiels. C’est l’exact analogue, en FOL, de l’erreur de raisonnement « il existe un grec et il existe un philosophe, donc il existe un philosophe grec ».

Le contrôle croisé qui suit rend cela visible : parmi les modèles de la KB, il en existe où personne ne porte les deux propriétés à la fois.

# --- Controle croise : enumeration exhaustive des interpretations du domaine {socrate, platon} ---
# 8 atomes fondes (4 predicats x 2 individus) -> 2^8 = 256 interpretations.
individus = ["socrate", "platon"]
atomes = [(p, i) for p in ["Homme", "Mortel", "Grec", "Philosophe"] for i in individus]

def kb_satisfaite(w):
    """Les 4 formules de la KB, relues atomiquement."""
    if not w[("Homme", "socrate")]:
        return False
    if not w[("Grec", "socrate")]:
        return False
    if not w[("Philosophe", "platon")]:
        return False
    for x in individus:  # axiome : forall X (Homme(X) => Mortel(X))
        if w[("Homme", x)] and not w[("Mortel", x)]:
            return False
    return True

def valeur(w, r):
    if r == "Mortel(socrate)":
        return w[("Mortel", "socrate")]
    if r == "Homme(platon)":
        return w[("Homme", "platon")]
    if r == "exists X Grec(X)":
        return any(w[("Grec", x)] for x in individus)
    if r == "exists X Philosophe(X)":
        return any(w[("Philosophe", x)] for x in individus)
    if r == "exists X (Grec(X) && Philosophe(X))":
        return any(w[("Grec", x)] and w[("Philosophe", x)] for x in individus)
    if r == "forall X Mortel(X)":
        return all(w[("Mortel", x)] for x in individus)
    raise ValueError(r)

modeles = []
for masque in range(256):
    bits = [bool((masque >> k) & 1) for k in range(8)]
    w = dict(zip(atomes, bits))
    if kb_satisfaite(w):
        modeles.append(w)

print(f"Interpretations du domaine {{socrate, platon}} : {2**8}")
print(f"Modeles de la KB                             : {len(modeles)}")

requetes_cc = ["Mortel(socrate)", "Homme(platon)", "exists X Grec(X)",
               "exists X Philosophe(X)", "exists X (Grec(X) && Philosophe(X))",
               "forall X Mortel(X)"]
print("\nRequete                              vraie dans   verdict (sur CE domaine)")
for r in requetes_cc:
    n = sum(1 for w in modeles if valeur(w, r))
    verdict = "unanime" if n == len(modeles) else "contestee"
    print(f"{r:<38s}{n:>2d}/{len(modeles)}{'':>8s}{verdict}")

# Le contre-modele minimal : exactement le monde temoin que Lean exhibera en section 4
monde_temoins = {("Homme", "socrate"): True, ("Mortel", "socrate"): True,
                 ("Grec", "socrate"): True, ("Philosophe", "socrate"): False,
                 ("Homme", "platon"): False, ("Mortel", "platon"): False,
                 ("Grec", "platon"): False, ("Philosophe", "platon"): True}
assert monde_temoins in modeles, "le monde temoin doit etre un modele de la KB"
falsifiees = [r for r in requetes_cc if not valeur(monde_temoins, r)]
print("\nMonde temoin {H,M,G sur socrate ; P sur platon} : modele de la KB, qui falsifie :")
for r in falsifiees:
    print("  -", r)

Interpretations du domaine {socrate, platon} : 256
Modeles de la KB                             : 12

Requete                              vraie dans   verdict (sur CE domaine)
Mortel(socrate)                       12/12        unanime
Homme(platon)                          4/12        contestee
exists X Grec(X)                      12/12        unanime
exists X Philosophe(X)                12/12        unanime
exists X (Grec(X) && Philosophe(X))    9/12        contestee
forall X Mortel(X)                     8/12        contestee

Monde temoin {H,M,G sur socrate ; P sur platon} : modele de la KB, qui falsifie :
  - Homme(platon)
  - exists X (Grec(X) && Philosophe(X))
  - forall X Mortel(X)

Lecture : l’énumération confirme — sur ce domaine, et ce qu’elle ne prouve pas

256 interprétations, dont 12 modèles de la KB : les faits fixent Homme/Mortel/Grec sur socrate et Philosophe sur platon, et restent libres les 4 atomes Philosophe(socrate), Homme(platon), Mortel(platon), Grec(platon) — 2⁴ = 16 combinaisons, moins les 4 où Homme(platon) est vrai sans Mortel(platon) (l’axiome contraint aussi platon) — d’où 12 ;
les requêtes Mortel(socrate), ∃X Grec(X), ∃X Philosophe(X) sont unanimes (12/12) : vraies dans chaque modèle du domaine — c’est la conséquence, sur ce domaine fixé ;
Homme(platon), la fusion et ∀X Mortel(X) sont contestées : des modèles les falsifient — c’est la non-conséquence, sur ce domaine fixé ;
le monde témoin imprimé en fin de cellule — Homme/Mortel/Grec sur socrate, Philosophe sur platon, rien d’autre — est un modèle de la KB qui falsifie d’un coup le contrôle Homme(platon), la fusion et l’universel : c’est exactement le contre-modèle Fin 2 que Lean exhibera (section 5).

La limite honnête du dénombrement. Cette énumération couvre le domaine {socrate, platon} uniquement. Pour les FALSE, un seul contre-modèle suffit — l’exhibition est une preuve complète. Mais pour les TRUE, l’unanimité sur 12 modèles d’un domaine fixé ne prouve pas la conséquence au sens FOL complet : des modèles à domaine 3, 10 ou infini existent hors de ce dénombrement. C’est précisément ce que le noyau Lean certifie dans les deux sections suivantes : les TRUE pour toutes les structures, les FALSE par exhibition formelle.

4. Le versant certifiant : le lake `formal_logic_lean` (FFL épinglé)

Le corpus Formalized Formal Logic formalise en Lean 4 les logiques elles-mêmes — syntaxe, sémantique, métathéorèmes. Le lake du dépôt le consomme en CONSUMER_PINNÉ (verdict du pilote #15520) : aucun module upstream n’est vendé ni adapté.

Le module FormalLogic.FolBridge (ce grain, #16877) définit la même micro-théorie côté Lean — le langage Lsoc (quatre SocRel unaires, deux SocFunc nulaires), la KB, les requêtes q* — puis :

Déclaration	Énoncé	Miroir Tweety
`mortel_socrate`	`KB ⊨ qMortelSocrate`	requête 1, TRUE
`existe_grec`, `existe_philosophe`	`KB ⊨ ∃X …`	requêtes 3-4, TRUE
`mondeTemoins` + `monde_modele_KB`	`Structure Lsoc (Fin 2)` qui modélise `KB`	le monde témoin de la section 3
`conjonction_non_consequence`	`¬(KB ⊨ ∃X (Grec ⋏ Philosophe))`	requête 5, FALSE
`tous_mortels_non_consequence`	`¬(KB ⊨ ∀X Mortel)`	requête 6, FALSE

Deux ancres métathéoriques sont citées (pas redémontrées) : Theory.Proof.sound (T ⊢ φ → T ⊨ φ) et Theory.Proof.complete_iff (T ⊨ φ ↔︎ T ⊢ φ) — le pont sémantique ↔︎ syntaxique que le versant propositionnel (Tweety-5e) ne pouvait qu’annoncer.

La cellule suivante mesure la provenance avant toute certification : pins git rev-parse réels contre le lake-manifest.json, puis lake build du module.

# --- Helpers WSL + provenance mesuree + build du module (patron Tweety-5e / Lean-3b) ---
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 4-5 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,
    )

# 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 ["Foundation", "mathlib", "ProvabilityLogic"]:
    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:<18s} {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.FolBridge", timeout=1800)
sortie = (r.stdout or "") + (r.stderr or "")
print("\n$ lake build FormalLogic.FolBridge")
print("\n".join(sortie.strip().splitlines()[-3:]))
assert r.returncode == 0, "lake build FormalLogic.FolBridge 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) :
  Foundation         81810b9f22c4  [pin confirme]
  mathlib            0df444a360ea  [pin confirme]
  ProvabilityLogic   01628c51f618  [pin confirme]

$ lake build FormalLogic.FolBridge
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 (1018 jobs).

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

Lecture : pins mesurés, build réel

les trois packages structurants sont mesurés par git rev-parse HEAD dans .lake/packages et confrontés au lake-manifest.json : Foundation 81810b9f22c4 (le pin CONSUMER_PINNÉ du pilote #15520), mathlib 0df444a360ea, ProvabilityLogic 01628c51f618 — chacun « pin confirmé ». Mesurer plutôt que déclarer : sans ce contrôle, le notebook compilerait contre une révision inconnue tout en affichant la bonne ;
lake build FormalLogic.FolBridge rend Build completed successfully : le module — le langage, la théorie, les six requêtes, les trois théorèmes de conséquence, le monde témoin et les deux réfutations — compile sans aucun sorry. Le comptage canonique du dépôt (scripts/lean/count_code_sorry.py, champ distinct_code_sorry) donne 0 pour ce lake ;
la moindre dérive (package manquant, pin décalé, build en échec) interrompt le notebook : le message dit quoi réparer, jamais comment contourner.

# --- Tour d'API : #check des objets FFL reels, 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)."""
    d = pathlib.Path(tempfile.mkdtemp(prefix="tweety02d_"))
    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)
    return (r.stdout or "") + (r.stderr or ""), r.returncode

api_tour = """import FormalLogic.FolBridge
open FFL.FirstOrder

#check @FFL.FirstOrder.Language
#check @FFL.FirstOrder.Structure
#check @FFL.FirstOrder.Semiformula.Eval
#check FFL.FirstOrder.Theory
#check FFL.FirstOrder.Consequence
#check @FFL.Semantics.consequence_iff
#check FFL.FirstOrder.Theory.Proof.sound
#check FFL.FirstOrder.Theory.Proof.complete_iff
#check @FormalLogic.FolBridge.Lsoc
#check @FormalLogic.FolBridge.KB
#check @FormalLogic.FolBridge.mortel_socrate
#check @FormalLogic.FolBridge.conjonction_non_consequence
#check @FormalLogic.FolBridge.tous_mortels_non_consequence
"""

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
Language : Type (u_1 + 1)
Structure : Language → Type u_2 → Type (max u_1 u_2)
@Semiformula.Eval : {ξ : Type u_3} →
  {L : Language} → {M : Type u_2} → {n : ℕ} → [s : Structure L M] → (Fin n → M) → (ξ → M) → Semiformula L ξ n →ˡᶜ Prop
FFL.FirstOrder.Theory.{u_1} (L : Language) : Type u_1
FFL.FirstOrder.Consequence.{u} {L : Language} (T : Theory L) (σ : Sentence L) : Prop
@FFL.Semantics.consequence_iff : ∀ {M : Type u_1} {F : Type u_2} [𝓢 : FFL.Semantics M F] {T : Set F} {φ : F},
  T ⊨[M] φ ↔ ∀ {𝓜 : M}, 𝓜 ⊧* T → 𝓜 ⊧ φ
FFL.FirstOrder.Theory.Proof.sound.{u, v} {L : Language} {T : Theory L} {φ : Sentence L} : T ⊢ φ → T ⊨[Struc L] φ
FFL.FirstOrder.Theory.Proof.complete_iff.{u} {L : Language} {T : Theory L} {φ : Sentence L} : T ⊨ φ ↔ T ⊢ φ
FormalLogic.FolBridge.Lsoc : Language
FormalLogic.FolBridge.KB : Theory FormalLogic.FolBridge.Lsoc
FormalLogic.FolBridge.mortel_socrate : FormalLogic.FolBridge.KB ⊨ FormalLogic.FolBridge.qMortelSocrate
FormalLogic.FolBridge.conjonction_non_consequence : ¬FormalLogic.FolBridge.KB ⊨
    FormalLogic.FolBridge.qExisteGrecEtPhilosophe
FormalLogic.FolBridge.tous_mortels_non_consequence : ¬FormalLogic.FolBridge.KB ⊨ FormalLogic.FolBridge.qTousMortels

[exit 0]

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

Le #check n’affiche pas une documentation — il demande au kernel le type exact de chaque déclaration, dans le dépôt épinglé :

Language : Type (u+1) — un langage FFL est une paire de familles Func/Rel indexées par l’arité ; côté pont, SocRel/SocFunc en sont les deux instances ;
Structure L M — une structure interprète le langage sur un domaine M quelconque : l’analogue d’un monde Tweety, mais pour n’importe quel ensemble — fini ou infini ;
Semiformula.Eval … →ˡᶜ Prop — la sémantique de Tarski comme fonction structurelle : la même Eval qui, côté notebook, calculera la vérité du monde témoin élément par élément ;
Consequence T σ : Prop — la relation notée T ⊨ σ, et consequence_iff qui la déplie : T ⊨ φ ↔︎ ∀ {𝓜}, 𝓜 ⊧* T → 𝓜 ⊧ φ — la caractérisation en tous modèles ;
Theory.Proof.sound : T ⊢ φ → T ⊨ φ et complete_iff : T ⊨ φ ↔︎ T ⊢ φ — les ancres métathéoriques (démontrées par FFL, citées par le pont) ;
les trois dernières lignes sont les déclarations du pont : mortel_socrate : KB ⊨ qMortelSocrate est un théorème ; les deux ¬(KB ⊨ …) sont des réfutations — chacune vérifiée pour son type exact.

# --- Certificat 1 : les trois TRUE de Tweety deviennent des theoremes ---
cert1 = """import FormalLogic.FolBridge

-- La derivation executee par Tweety (universel instancie a socrate + modus ponens),
-- certifiee pour TOUTE structure modelisant KB -- un sondage devient une preuve.
#print axioms FormalLogic.FolBridge.mortel_socrate

-- Les deux existentiels, chacun consequence (temoins socrate et platon).
#print axioms FormalLogic.FolBridge.existe_grec
#print axioms FormalLogic.FolBridge.existe_philosophe

-- Reutilisation : toute structure M modelisant KB satisfait Mortel(socrate).
example : ∀ (_M : Type) [Nonempty _M] [FFL.FirstOrder.Structure FormalLogic.FolBridge.Lsoc _M],
    _M↓[FormalLogic.FolBridge.Lsoc] ⊧* FormalLogic.FolBridge.KB →
    _M↓[FormalLogic.FolBridge.Lsoc] ⊧ FormalLogic.FolBridge.qMortelSocrate :=
  fun _M _ _ hM => FFL.Semantics.consequence_iff.mp FormalLogic.FolBridge.mortel_socrate hM
"""

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 : les trois verdicts TRUE sont des theoremes (toutes structures).")

$ lake env lean scratch.lean
'FormalLogic.FolBridge.mortel_socrate' depends on axioms: [propext, Classical.choice, Quot.sound]
'FormalLogic.FolBridge.existe_grec' depends on axioms: [propext, Classical.choice, Quot.sound]
'FormalLogic.FolBridge.existe_philosophe' depends on axioms: [propext, Classical.choice, Quot.sound]

[exit 0]
CERTIFICAT 1 : les trois verdicts TRUE sont des theoremes (toutes structures).

Lecture : trois théorèmes, trois axiomes standard, zéro sorry

#print axioms interroge le noyau sur les fondations exactes de chaque preuve : les trois théorèmes dépendent uniquement de [propext, Classical.choice, Quot.sound] — les trois axiomes standard de Lean 4 (extensionnalité propositionnelle, choix classique, quotients). Pas de sorryAx (preuve incomplète), pas de native_decide (réduction non certifiée) : ce sont des preuves complètes au sens du noyau.

La lecture croisée, requête par requête :

Tweety exécute	Lean certifie	Portée
`Mortel(socrate)` = TRUE (Herbrand)	`mortel_socrate : KB ⊨ qMortelSocrate`	toutes les structures, domaines arbitraires
`∃X Grec(X)` = TRUE	`existe_grec : KB ⊨ qExisteGrec`	idem — le témoin `socrate` vaut dans chaque modèle
`∃X Philosophe(X)` = TRUE	`existe_philosophe : KB ⊨ qExistePhilosophe`	idem — témoin `platon`

L’example de la cellule montre la réutilisation : via consequence_iff.mp, quiconque fournit une structure quelconque (avec un domaine arbitraire, même infini) qui modélise KB en dérive immédiatement Mortel(socrate) — le modus ponens a été déroulé une fois pour toutes les structures, là où l’énumération de Herbrand le rejouait sur le domaine fini.

# --- Certificat 2 : les FALSE deviennent des contre-modeles exhibes ---
cert2 = """import FormalLogic.FolBridge

-- Le monde temoin : domaine Fin 2 (0 = socrate, 1 = platon), construit et verifie par le noyau.
#check @FormalLogic.FolBridge.mondeTemoins
#print axioms FormalLogic.FolBridge.monde_modele_KB

-- La fusion a temoin unique n'est PAS consequence : le monde temoin la falsifie.
#print axioms FormalLogic.FolBridge.conjonction_non_consequence

-- Et forall X Mortel(X) non plus : platon (l'element 1) n'y est pas mortel.
#print axioms FormalLogic.FolBridge.tous_mortels_non_consequence
"""

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 deux FALSE sont des non-consequences prouvees par contre-modele.")

$ lake env lean scratch.lean
FormalLogic.FolBridge.mondeTemoins : FFL.FirstOrder.Structure FormalLogic.FolBridge.Lsoc (Fin 2)
'FormalLogic.FolBridge.monde_modele_KB' depends on axioms: [propext, Classical.choice, Quot.sound]
'FormalLogic.FolBridge.conjonction_non_consequence' depends on axioms: [propext, Classical.choice, Quot.sound]
'FormalLogic.FolBridge.tous_mortels_non_consequence' depends on axioms: [propext, Classical.choice, Quot.sound]

[exit 0]
CERTIFICAT 2 : les deux FALSE sont des non-consequences prouvees par contre-modele.

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

Le #check révèle le type du monde témoin : mondeTemoins : Structure Lsoc (Fin 2) — une structure véritable sur le domaine à deux éléments, où 0 joue socrate et 1 joue platon :

	Homme	Mortel	Grec	Philosophe
`0` (socrate)	oui	oui	oui	non
`1` (platon)	non	non	non	oui

— exactement le contre-modèle minimal imprimé par l’énumération Python (section 3). Les trois #print axioms attestent ensuite que :

monde_modele_KB : le noyau vérifie que ce monde satisfait les 4 formules de la KB — l’axiome universel n’y est impliqué que pour l’élément 0, seul Homme, et il est Mortel ;
conjonction_non_consequence : ¬(KB ⊨ ∃X (Grec ⋏ Philosophe)) : ce modèle falsifie la fusion (personne n’y porte les deux propriétés), donc la conséquence échoue — le FALSE de Tweety devient une réfutation certifiée ;
tous_mortels_non_consequence : ¬(KB ⊨ ∀X Mortel) : l’élément 1 n’y est pas mortel.

Et la négation ? Ces théorèmes ne disent rien de KB ⊨ ¬∃X (Grec ⋏ Philosophe) ni de KB ⊨ ∃X ¬Mortel(X) : la non-conséquence de φ n’implique pas la conséquence de ¬φ. Le monde reste ouvert — la KB ne parle d’aucun autre individu, et des modèles à domaine 3, 10 ou infini coexistent avec ce contre-modèle. La symétrie est complète : TRUE ↔︎ théorème, FALSE ↔︎ contre-modèle exhibé — la confusion closed-world (« FALSE donc la négation ») n’a jamais eu sa place, et ce labo l’a maintenant écrite noir sur blanc des deux côtés.

5. Bilan croisé : trois lectures, une seule vérité

Requête	Tweety (Herbrand)	Énumération (12 modèles)	Lean (kernel)
`Mortel(socrate)`	TRUE	unanime	`KB ⊨ ·` (théorème)
`Homme(platon)`	FALSE	contestée	— (exercice 3)
`∃X Grec(X)`	TRUE	unanime	`KB ⊨ ·` (théorème)
`∃X Philosophe(X)`	TRUE	unanime	`KB ⊨ ·` (théorème)
`∃X (Grec ⋏ Philosophe)`	FALSE	contestée	`¬(KB ⊨ ·)` + monde `Fin 2`
`∀X Mortel(X)`	FALSE	contestée	`¬(KB ⊨ ·)` + monde `Fin 2`

Ce que chaque colonne prouve, et ne prouve pas :

Tweety : la réponse d’un raisonneur FOL réel, par énumération de Herbrand sur les constantes — exécution industrielle, mais domaine de l’énumération borné aux éléments nommés ;
l’énumération Python : un contrôle croisé indépendant sur les 12 modèles du domaine à deux individus — vérifie la cohérence des verdicts, sans sortir de ce domaine ;
Lean : le statut définitif — les TRUE prouvés pour toutes les structures (domaines arbitraires, y compris infinis), les FALSE réfutés par exhibition d’un contre-modèle vérifié.

Et le cercle se referme par les ancres métathéoriques : Theory.Proof.complete_iff (T ⊨ φ ↔︎ T ⊢ φ) dit que la conséquence sémantique certifiée ici coïncide avec la dérivabilité syntaxique — ce que le modus ponens de Tweety calcule, FFL le théorise, et ce notebook relie les deux sur la même micro-théorie.

Exercice 1 : étendre la théorie — `Homme(platon)`

Contexte

Ajouter le fait Homme(platon) à la KB change plusieurs verdicts — mais pas tous, et pas dans le sens où l’intuition presse de conclure.

Objectifs

Construire kb2 (les 4 formules de KB + Homme(platon)) et requérir Mortel(platon) — prédire le verdict avant d’exécuter, puis vérifier
Requérir ∃X (Homme(X) ∧ Philosophe(X)) — quel témoin unique devient disponible ?
∀X Mortel(X) est-il devenu une conséquence de kb2 ? Justifier sans exécuter en construisant un contre-modèle (indice : il faut un troisième individu, ni homme ni mortel — le monde reste ouvert)

Indices : - réutilisez FolAtom(Homme, platon) et kb2.add(JObject(f, FolFormula)) ; - pour le contre-modèle : que la KB interdit-elle vraiment sur un individu dont aucun fait n’est posé ?

# --- Exercice 1 : KB + Homme(platon) ---
# TODO etudiant
# Etape 1 : kb2 = FolBeliefSet() + les 5 formules (axiome + 3 faits de KB + Homme(platon))
# Etape 2 : requeriez Mortel(platon) puis exists X (Homme(X) && Philosophe(X))
# Etape 3 : requeriez forall X Mortel(X) et expliquez le verdict via un contre-modele a 3 elements
print("Exercice a completer")

Exercice a completer

Exercice 2 : chirurgie de requête — réparer la fusion

Contexte

La fusion ∃X (Grec(X) ∧ Philosophe(X)) échoue parce qu’aucun fait ne donne les deux propriétés au même individu. Un seul fait bien choisi la rend vraie.

Objectifs

Sans exécuter : identifier le fait qui rend la fusion conséquence, et son témoin unique
Vérifier avec Tweety : kb3 = KB + ce fait, requérir la fusion — verdict attendu TRUE
Sur kb3, le verdict TRUE de la fusion entraîne-t-il Philosophe(socrate) ? Répondre sans exécuter, en termes de témoins (indice : témoin disponible ≠ égalité de témoins)

Indices : - les candidats sont Grec(platon) ou Philosophe(socrate) — un seul des deux suffit ; - pour la question 3, demandez-vous ce que le contre-modèle de la section 5 devient sur kb3.

# --- Exercice 2 : le fait qui retourne la fusion ---
# TODO etudiant
# Etape 1 : identifier le fait minimal (sur papier)
# Etape 2 : kb3 = KB + ce fait ; requeriez exists X (Grec(X) && Philosophe(X))
# Etape 3 : requeriez Philosophe(socrate) sur kb3 et expliquez l'ecart avec la question precedente
print("Exercice a completer")

Exercice a completer

Exercice 3 : votre premier certificat Lean

Contexte

Les sections 4-5 ont certifié 5 des 6 verdicts. Il manque le contrôle négatif : Homme(platon) n’est pas conséquence. Le pont ne déclare pas cette requête — c’est à vous de l’écrire.

Objectifs

Écrire un certificat qui définit qHommePlaton (pattern des q* de FolBridge.lean : Semiformula.rel SocRel.homme (fun _ => tPlaton)) puis prouve ¬(KB ⊨ qHommePlaton)
Preuve attendue : le monde témoin falsifie Homme(platon) — l’élément 1 n’y est pas homme — sur le pattern de monde_falsifie_tous_mortels (rw [models_iff_eval], have typé, absurd … (by decide))
Exécuter : sortie [exit 0] avec depends on axioms: [propext, Classical.choice, Quot.sound]

Indices : - squelette : import FormalLogic.FolBridge puis open FFL.FirstOrder et open FFL.FirstOrder.Semiterm (pour ∀¹ et #) ; - la définition d’une requête et la preuve de falsification sont dans Lean/formal_logic_lean/FormalLogic/FolBridge.lean — lisez monde_falsifie_tous_mortels ; - run_lean est déjà défini : out, rc = run_lean(mon_certificat) puis assert rc == 0.

# --- Exercice 3 : certificat Lean de la non-consquence de Homme(platon) ---
# TODO etudiant
# Etape 1 : mon_certificat = """import FormalLogic.FolBridge ... (definir qHommePlaton, puis
#           example/theorem : ¬(KB ⊨ qHommePlaton) via le monde temoin)"""
# Etape 2 : out, rc = run_lean(mon_certificat) ; print(out) ; print(rc)
# Etape 3 : assert rc == 0 and "sorry" not in out
print("Exercice a completer")

Exercice a completer

Conclusion

Ce labo a croisé trois moteurs de vérité sur une même micro-théorie FOL :

Tweety exécute : construction programmatique de la KB (prédicats, constantes, quantificateurs), six verdicts du SimpleFolReasoner — 6/6 conformes à la lecture sémantique ;
l’énumération contrôle : 256 interprétations, 12 modèles, unanimités et contestations mesurées, contre-modèle minimal identifié ;
Lean certifie : les trois TRUE deviennent des théorèmes KB ⊨ φ (toutes structures, aucun sorry, axiomes [propext, Classical.choice, Quot.sound] uniquement), les deux FALSE des réfutations ¬(KB ⊨ φ) par exhibition du monde Fin 2 — pins Foundation/mathlib/ProvabilityLogic mesurés avant certification.

Points clés à retenir :

FALSE ≠ négation prouvée : la non-conséquence est une preuve d’existence d’un contre-modèle ; la négation est une conséquence séparée à prouver. Le monde de la FOL classique est ouvert ;
la fusion à témoin unique ∃X (φ ⋏ ψ) est strictement plus forte que ∃X φ + ∃X ψ : deux existentiels indépendants élisent des témoins distincts ;
un verdict de raisonneur est un sondage (Herbrand, domaine nommé) ; un théorème certifié est une preuve pour toutes les structures — la complétude (complete_iff) relie les deux mondes ;
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 FOL et tutoriels ;
Formalized Formal Logic — corpus Foundation (pin 81810b9f) ;
EPIC #15066 — laboratoires croisés Tweety ↔︎ Lean (Tranche A : propositionnel #15520 ; Tranche B : ce grain, #16877) ;
Notebooks compagnons : Tweety-02 (FOL exécutée), Tweety-02c (port C#/IKVM), Tweety-5e (labo propositionnel certifié), Lean-3b (tour FFL complet).

Navigation : ← Tweety-02c (FOL C#) · Tweety-5e (labo propositionnel) · Index · 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 micro-théorie : deux individus, quatre prédicats

Lecture : la théorie est en place

Lecture : ce que FALSE veut dire — et ce qu’il ne veut PAS dire

3. Le duel des témoins

Lecture : l’énumération confirme — sur ce domaine, et ce qu’elle ne prouve pas

4. Le versant certifiant : le lake formal_logic_lean (FFL épinglé)

Lecture : pins mesurés, build réel

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

Lecture : trois théorèmes, trois axiomes standard, zéro sorry

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

5. Bilan croisé : trois lectures, une seule vérité

Exercice 1 : étendre la théorie — Homme(platon)

Contexte

Objectifs

Exercice 2 : chirurgie de requête — réparer la fusion

Contexte

Objectifs

Exercice 3 : votre premier certificat Lean

Contexte

Objectifs

Conclusion

Références

Lecture : ce que `FALSE` veut dire — et ce qu’il ne veut PAS dire

4. Le versant certifiant : le lake `formal_logic_lean` (FFL épinglé)

Exercice 1 : étendre la théorie — `Homme(platon)`