Tranche E de l’Epic #15066 (Formalized Formal Logic) — l’arc Lean autonome annoncé par la conclusion de Lean-3b : calculabilité, diagonalisation et limites. Prérequis direct des niveaux L2/L3 de #15062 (FairBot, coopération one-shot), mais valable indépendamment.
Le contrat : quatre énoncés souvent amalgamés
#
Énoncé
Ce qu’il dit
Ce qu’il ne dit PAS
1
Indécidabilité de la logique du premier ordre (Church)
aucun algorithme ne décide la validité FOL
rien sur l’arithmétique ni sur l’arrêt
2
Problème de l’arrêt
aucun programme ne décide si un programme termine
c’est un énoncé de calculabilité, pas une théorie
3
Incomplétude arithmétique (Gödel I/II, Rosser)
toute théorie arithmétique récursive suffisante a une phrase vraie indémontrable, et ne prouve pas sa propre cohérence
pas « les mathématiques sont fausses », pas Tarski
4
Indéfinissabilité de la vérité (Tarski)
aucune formule arithmétique ne définit la vérité des phrases de ℕ
pas une question de démontrabilité mais de définissabilité
Le fil du notebook : exécuter (des témoins Python bornés rendent la diagonalisation palpable), puis certifier — chaque énoncé devient un #check contre le noyau Lean, chaque preuve un #print axioms audité. L’arithmétisation n’est pas redémontrée ici : elle vit dans Formalized Formal Logic, consommée en CONSUMER_PINNÉ.
Outils
Python (kernel du notebook) : les témoins exécutables — diagonale de l’arrêt, point fixe diagonal sur chaînes ;
le lake formal_logic_lean (toolchain Lean v4.33.1) : le noyau qui certifie — Foundation piné au commit 81810b9f et ProvabilityLogic au commit 01628c51 (pilotes #15520 / #15923), aucun module upstream vendu ni adapté.
1. Calculer, énumérer, décider — et la diagonale de l’arrêt
Le problème de l’arrêt demande un décideurH(prog, entrée) → oui/non correct pour tous les programmes. L’argument diagonal montre qu’un tel H ne peut pas exister : à tout candidat H on associe le programme diagonal
D_H(p) := si H(p, p) alors boucler infiniment sinon s'arrêter
et l’exécution de D_H(D_H) contredit H(D_H, D_H)dans les deux cas. Le témoin ci-dessous exécute cette contradiction sur deux candidats concrets (bornés, donc explicitement pas des décideurs — chacun est réfuté sur sa propre diagonale).
# --- Setup : localiser le lake (patron Lean-3b) ---import osimport 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).stdout.strip() +"/formal_logic_lean"r = subprocess.run( ["wsl", "-e", "bash", "-lc",f"cd {LAKE_DIR} && cat lean-toolchain && lake --version | head -1"], capture_output=True, text=True, timeout=120)print(r.stdout.strip() or r.stderr.strip())
leanprover/lean4:v4.33.1
Lake version 5.0.0-src+819816b (Lean version 4.33.1)
Lecture du setup : deux machines qui dialoguent
La sortie confirme le contrat d’exécution : le lake formal_logic_lean tourne sous WSL avec la toolchain leanprover/lean4:v4.33.1 et Lake 5.0.0-src. Ce notebook est un Python orchestrateur : chaque cellule « audit » écrit un fichier .lean temporaire, le soumet au vrai noyau via lake env lean, puis détruit le fichier — les réponses affichées ne sont jamais fabriquées, elles viennent du kernel. Notez aussi le soin porté au chemin : wslpath -a dérive l’emplacement du lake depuis le répertoire courant, jamais en dur — le notebook reste exécutable depuis n’importe quel checkout (clone post-merge comme worktree d’agent). Et la version 4.33.1 affichée ici est celle que le manifeste du lake épingle : tout écart de toolchain entre machines serait visible en tête de notebook, avant toute preuve.
Le choix de WSL n’est pas cosmétique : le toolchain Lean 4 officiel est compilé pour Linux ; sous Windows, c’est la voie canonique — on répare l’environnement, on ne le contourne pas.
# --- Temoin executable : la diagonale de l'arret ---# Chaque candidat H est une heuristique BORNEE (stand-in d'un oracle hypothetique) ;# on construit D_H et on observe la contradiction sur sa propre diagonale.class BudgetEpuise(Exception):"""Levee quand la simulation bornee epuise ses pas (= 'boucle')."""BUDGET =200_000# pas de simulationdef run_borne(f, x):"""Simule f(x) avec un budget de pas ; rend ("arret", v) ou ("boucle", None).""" compteur = [0]def trace(frame, event, arg): compteur[0] +=1if compteur[0] > BUDGET:raise BudgetEpuisereturn traceimport sys sys.settrace(trace)try:return ("arret", f(x))except BudgetEpuise:return ("boucle", None)finally: sys.settrace(None)def boucle_infinie():whileTrue:pass# interrompu par le budget# Candidat A : pretend que tout programme s'arrete.def candidat_toujours_arret(prog, x):returnTrue# Candidat B : pretend que tout programme boucle.def candidat_toujours_boucle(prog, x):returnFalsedef fabrique_diagonale(candidat):"""D_H(p) := si candidat(p, p) alors boucler sinon s'arreter."""def D_H(x):if candidat(D_H, x): boucle_infinie()return0return D_Hfor nom, candidat in [("A (dit 'tout s'arrete')", candidat_toujours_arret), ("B (dit 'tout boucle')", candidat_toujours_boucle)]: D_H = fabrique_diagonale(candidat) verdict = candidat(D_H, D_H) # ce que le candidat PRETEND realite, _ = run_borne(D_H, D_H) # ce qui se PRODUIT (simulation bornee) contradiction = ("arrete"if verdict else"boucle") != realiteprint(f"Candidat {nom}")print(f" H(D_H, D_H) pretend : {'arret'if verdict else'boucle'}")print(f" execution bornee : {realite}")print(f" contradiction : {contradiction}")print()print("La construction D_H contredit TOUT candidat : c'est le theoreme.")print("La version certifiee vit dans Halting.lean -- auditee en cellule suivante.")
Candidat A (dit 'tout s'arrete')
H(D_H, D_H) pretend : arret
execution bornee : boucle
contradiction : True
Candidat B (dit 'tout boucle')
H(D_H, D_H) pretend : boucle
execution bornee : arret
contradiction : True
La construction D_H contredit TOUT candidat : c'est le theoreme.
La version certifiee vit dans Halting.lean -- auditee en cellule suivante.
Lecture du témoin
Le témoin exécute la diagonale : pour chaque candidat borné, la prédiction H(D_H, D_H) et le comportement réel de D_H(D_H) divergent — dans les deux sens possibles. C’est l’incarnation calculable de l’argument ; la preuve, elle, est un énoncé Lean dans Foundation.FirstOrder.Incompleteness.Halting : incomplete_of_halting_problem, qui transforme l’indécidabilité de l’arrêt en incomplétude de toute théorie arithmétique récursive — l’énoncé 2 produit l’énoncé 3. On construit d’abord (build), puis on interroge le noyau (#check, #print axioms).
# --- Certification : build des modules cibles (patron Tweety-5d) ---# Les 8 modules consommes par ce notebook : build explicite (idempotent,# instantane si le cache d'oleans est chaud).import subprocesscibles = ["Foundation.FirstOrder.Incompleteness.Church","Foundation.FirstOrder.Incompleteness.Halting","Foundation.FirstOrder.Incompleteness.First","Foundation.FirstOrder.Incompleteness.Second","Foundation.FirstOrder.Incompleteness.Löb","Foundation.FirstOrder.Incompleteness.Tarski","Foundation.FirstOrder.Incompleteness.RosserProvability","Foundation.FirstOrder.Bootstrapping.FixedPoint",]r = subprocess.run( ["wsl", "-e", "bash", "-lc",f"cd {LAKE_DIR} && lake build {' '.join(cibles)} 2>&1 | tail -10; ""echo \"lake build rc=${PIPESTATUS[0]}\""], capture_output=True, text=True, timeout=1800)print(r.stdout.strip() or r.stderr.strip())
Lecture du build : 1226 jobs, et des info: qui ne sont pas des erreurs
Trois choses à lire dans cette sortie. lake build rc=0 : les huit modules d’incomplétude (Church, Halting, First, Second, Löb, Tarski, RosserProvability, FixedPoint) compilent — et le cache d’oléanes rend le build idempotent, quasi instantané au deuxième passage. Build completed successfully (1226 jobs) : le compte de tâches mesure la profondeur réelle de la chaîne de compilation en aval — la bibliothèque Foundation entraîne une grande partie de sa propre arborescence. Enfin, les lignes info: qui précèdent ne sont pas des diagnostics de nos modules : elles viennent de BinderNotation.lean, qui s’auto-documente en pretty-printant des Semiformula d’exemple — des égalités entre termes de l’arithmétique du premier ordre en notation interne du noyau (op(=).operator ![...], variables de de Bruijn &0, #3). Savoir trier info / warning / error dans une sortie de build est un réflexe Lean : ici, tout est au vert.
Une dernière précision utile : le build est ciblé. Nous ne compilons pas tout le lake, seulement les huit modules que le notebook consomme — lake build Foundation.FirstOrder.Incompleteness.Halting (et ses frères) résout les dépendances au juste nécessaire. C’est la différence entre un notebook reproductible en minutes et une reconstruction entière à chaque exécution.
# --- Audit : le noyau repond -- arret et incompletude ---import tempfileimport pathlibdef audit_lean(src, timeout=900, tail=14):"""Ecrit src dans un .lean temporaire, le soumet au noyau via lake env lean."""with tempfile.NamedTemporaryFile("w", suffix=".lean", delete=False, encoding="utf-8", newline="\n") as f: f.write(src) chemin = f.name wsl_path = subprocess.run( ["wsl", "-e", "wslpath", "-a", chemin.replace(chr(92), "/")], capture_output=True, text=True).stdout.strip() r = subprocess.run( ["wsl", "-e", "bash", "-lc",f"cd {LAKE_DIR} && lake env lean {wsl_path} 2>&1 | tail -{tail}"], capture_output=True, text=True, timeout=timeout) pathlib.Path(chemin).unlink(missing_ok=True)print(r.stdout.strip() or r.stderr.strip())audit_lean("import Foundation.FirstOrder.Incompleteness.Halting\n""#check @FFL.FirstOrder.Arithmetic.incomplete_of_halting_problem\n""#check @FFL.FirstOrder.Arithmetic.incomplete_of_REPred_not_ComputablePred\n""#print axioms FFL.FirstOrder.Arithmetic.incomplete_of_halting_problem\n""#print axioms FFL.FirstOrder.Arithmetic.incomplete_of_REPred_not_ComputablePred\n")
FFL.FirstOrder.Arithmetic.incomplete_of_halting_problem : ∀ (T : FFL.FirstOrder.ArithmeticTheory)
[FFL.FirstOrder.Theory.Δ₁ T] [𝗜𝚺₁ ⪯ T] [T.SoundOnHierarchy 𝚺 1], FFL.Entailment.Incomplete T
FFL.FirstOrder.Arithmetic.incomplete_of_REPred_not_ComputablePred : ∀ (T : FFL.FirstOrder.ArithmeticTheory)
[FFL.FirstOrder.Theory.Δ₁ T] [𝗜𝚺₁ ⪯ T] [T.SoundOnHierarchy 𝚺 1] {α : Type u_1} [inst : Primcodable α] {P : α → Prop},
REPred P → ¬ComputablePred P → FFL.Entailment.Incomplete T
'FFL.FirstOrder.Arithmetic.incomplete_of_halting_problem' depends on axioms: [propext, Classical.choice, Quot.sound]
'FFL.FirstOrder.Arithmetic.incomplete_of_REPred_not_ComputablePred' depends on axioms: [propext,
Classical.choice,
Quot.sound]
Lecture : le théorème tel que le noyau le connaît
incomplete_of_halting_problem : Entailment.Incomplete T — sous ses hypothèses de section (théorie arithmétique récursive contenant 𝗥₀), la théorie T est incomplète : il existe une phrase qu’elle ne prouve ni ne réfute. L’audit #print axioms liste les axiomes engagés par la preuve FFL — en général Classical.choice, propext, Quot.sound (les trois standard de Mathlib) : la métathéorie de la certification est honnête, rien de plus fort n’est smugglé. Le pont exécutif du haut de section (incomplete_of_REPred_not_ComputablePred) est la forme générale : tout prédicat récursivement énumérable mais non calculable produit de l’incomplétude — l’énoncé 2 est devenu l’énoncé 3.
2. Le point fixe diagonal — l’ingrédient central
Le lemme diagonal (Carnap–Gödel–Tarski) : pour toute formule arithmétique à une variable libre θ, il existe une phrase σ telle que T ⊢ σ ↔︎ θ(⌜σ⌝) — chaque phrase peut « parler de son propre numéro ». C’est l’ingrédient unique derrière Gödel I, Tarski et Löb. Témoin exécutable minimal : l’opérateur de substitution Q ↦ texte(Q) sur les chaînes produit un programme qui se cite lui-même.
# --- Temoin executable : le point fixe diagonal (quine) ---def diagonal(theta):"""Remplace dans theta la marque @ par le texte de theta lui-meme."""return theta.replace(chr(64), repr(theta))theta ="s = @\nprint(s.replace(chr(64), repr(s)))"fixpoint = diagonal(theta)print("--- programme fixpoint produit par diagonal(theta) ---")print(fixpoint)print("--- execution : il imprime exactement son propre texte ---")exec(fixpoint)print("---------------- fin du temoin ----------------")print("diagonal(theta) joue le role de \u03c3 ; l'auto-citation est le temoin.")
--- programme fixpoint produit par diagonal(theta) ---
s = 's = @\nprint(s.replace(chr(64), repr(s)))'
print(s.replace(chr(64), repr(s)))
--- execution : il imprime exactement son propre texte ---
s = 's = @\nprint(s.replace(chr(64), repr(s)))'
print(s.replace(chr(64), repr(s)))
---------------- fin du temoin ----------------
diagonal(theta) joue le role de σ ; l'auto-citation est le temoin.
Lecture du quine : la propriété de point fixe, lisible sur la sortie
Comparez les deux blocs imprimés : le texte du programme fixpoint produit par diagonal(theta), puis ce qu’imprime son exec — ils sont identiques, caractère pour caractère. C’est la propriété de point fixe rendue visible : l’opérateur diagonal (substituer à la marque @ le repr du programme lui-même) joue le rôle de l’opération de substitution de Gödel, le programme fixpoint joue σ, et son texte joue ⌜σ⌝ — le programme se cite lui-même au sens propre. C’est le même ingrédient diagonal que dans le témoin de l’arrêt (D_H reçoit sa propre définition en argument) et celui-là même que Tarski interdit à la vérité (aucune formule ne peut s’auto-appliquer). La version certifiée — T ⊢ fixedpoint θ 🡘 θ/[⌜fixedpoint θ⌝] — est auditée à la cellule suivante.
Un détail d’implémentation mérite l’œil : diagonal opère sur des chaînes (theta.replace(chr(64), repr(theta))), pas sur des arbres de syntaxe. C’est la version « texte brut » de l’opération de Gödel, historiquement la première — la version arithmétique (coder les chaînes par des entiers, substituer par des fonctions représentables) est celle que le noyau certifie à la cellule suivante.
# --- Audit : le lemme diagonal tel que FFL le prouve ---audit_lean("import Foundation.FirstOrder.Bootstrapping.FixedPoint\n""#check @FFL.FirstOrder.Arithmetic.diagonal\n""#print axioms FFL.FirstOrder.Arithmetic.diagonal\n")
Lecture de la signature : fixedpoint θ 🡘 θ/[⌜fixedpoint θ⌝]
Le noyau énonce le lemme diagonal sous sa forme la plus économique : pour toute semi-phrase arithmétique θ à une variable libre, il existe une phrase — fixedpoint θ — que T prouve équivalente (c’est le 🡘) à θ substituée par le numéro de cette phrase elle-même (la notation θ/[⌜·⌝]). L’hypothèse de section 𝗜𝚺₁ ⪯ T est minimale : il suffit que la théorie contienne l’arithmétique 𝗜𝚺₁. Et l’audit #print axioms ne liste que les trois axiomes standard (propext, Classical.choice, Quot.sound) — l’auto-référence arithmétique n’engage aucune métathéorie exotique. C’est ce unique lemme, appliqué à trois θ différentes, qui produit Gödel I (θ = « je ne suis pas prouvable »), Tarski (θ = « je suis faux ») et Löb.
Remarquez aussi l’échange silencieux de l’énoncé : fixedpoint θ est une phrase (aucune variable libre), alors que θ en a une — la substitution θ/[⌜fixedpoint θ⌝] referme exactement cette variable sur le numéro de la phrase produite. Le noyau type cette fermeture pour nous : toute erreur d’arité ou de liaison serait rejetée à la compilation, pas à la relecture.
3. Les quatre énoncés au noyau
Chaque ligne de la table d’ouverture devient un #check — le noyau vérifie que le nom existe et que la signature est bien celle annoncée. Deux audits : Gödel I/II + Church, puis Tarski + Löb + Rosser.
Lecture croisée — pourquoi ces énoncés sont distincts
Church ≠ halting : undecidability_first_order_logic porte sur la validité dans toutes les structures du langage FOL ; l’arrêt porte sur le comportement des programmes. Les deux sont indécidables, les preuves ne se substituent pas — FFL les sépare dans deux modules.
Gödel II ≠ Tarski : consistent_unprovable dit que la théorie ne prouve pas sa cohérence (faillibilité de la démontrabilité) ; undefinability_of_truth dit qu’aucune formule ne définit le prédicat de vérité (limite de la définissabilité). Le second est strictement plus fort sur le plan sémantique — et c’est un théorème de ℕ, pas de T.
Rosser retire l’hypothèse de ω-cohérence : rosser_internalize montre que la prouvabilité interne se reflète en prouvabilité de Rosser — la version « économique » de Gödel I.
Löb renforce le deuxième : si T prouve Prov(⌜σ⌝) → σ, alors T prouve σ. C’est la porte d’entrée de la logique de prouvabilité GL — le pont explicite vers la Tranche F et #15062 (FairBot prouve sa propre coopération dans GL).
Les quatre #print axioms audités confirment que rien au-delà des axiomes standard du noyau n’est engagé : ces limites sont des théorèmes, pas des actes de foi métathéoriques.
4. Exercices
# Exercice a completer : diagonale de Cantor sur les suites binaires.# Aucune suite (s_n) de suites binaires n'egale la suite diagonale# d := n |-> 1 - s_n(n). Construire d pour les 3 premieres suites donnees,# puis verifier sur les indices 0..2 que d differe de chacune.suites = [ [0, 1, 1, 0, 1], [1, 1, 0, 0, 0], [0, 0, 1, 1, 1],]# TODO etudiant : construire d (liste des 5 premiers termes) puis comparer.d =None# TODO etudiantprint("Exercice 1 a completer : diagonale de Cantor.")
Exercice 1 a completer : diagonale de Cantor.
# Exercice a completer : audit Loeb formalise.# Soumettre au noyau (fonction audit_lean de ce notebook) le #check de# FFL.FirstOrder.Arithmetic.formalized_loeb_theorem, puis formuler en une# phrase ce que la formalisation INTERNE ajoute au loeb_theorem externe.# Indice : la preuve de lob est elle-meme un enonce demontre dans ISigma_1.print("Exercice 2 a completer : lecture du Lob formalise.")
Exercice 2 a completer : lecture du Lob formalise.
# Exercice a completer : independance de la cohérence.# Second.lean fournit aussi inconsistent_independent : pour T sigma_1-sonde,# la phrase de cohérence est INDEPENDANTE (ni prouvable, ni refutable).# Contraster avec consistent_unprovable (qui n'exclut pas la refutabilite# pour une theorie incoherente). Ecrire la table des 3 cas.print("Exercice 3 a completer : cohérence -- non prouvable vs indépendante.")
Exercice 3 a completer : cohérence -- non prouvable vs indépendante.
Ce que les trois exercices réutilisent
Chaque exercice replie un ingrédient audité plus haut. L’exercice 1 (diagonale de Cantor) réutilise le mécanisme du témoin d’arrêt : construire un objet qui contredit toute proposition faite sur lui — la même diagonalisation que D_H, sur les ensembles plutôt que les programmes. L’exercice 2 (lecture du Löb formalisé) demande de relire löb_theorem tel que le noyau l’a affiché : T ⊢ Prov(⌜σ⌝) 🡒 σ → T ⊢ σ — comprendre pourquoi l’hypothèse elle-même est une prouvabilité, et ce que ça change de Gödel II. L’exercice 3 (cohérence : non prouvable vs indépendante) s’appuie sur les deux signatures consistent_unprovable / inconsistent_unprovable : la cohérence n’est pas prouvable (Gödel II), mais sa négation non plus (sous 𝚺₁-sondité) — « indépendante » est le mot juste, « fausse » serait une erreur.
Conseil de méthode : pour chaque exercice, commencez par relire la sortie du noyau correspondante avant d’écrire — la réponse à « que formalise Löb ? » est littéralement dans la signature löb_theorem affichée plus haut ; l’exercice consiste à la traduire, pas à la redécouvrir.
Conclusion — ce que l’arc établit, et la suite
Exécuter : la diagonale de l’arrêt et le point fixe sur chaînes, comme témoins bornés. Certifier : Church, arrêt→incomplétude, Gödel I/II, Rosser, Tarski et Löb comme énoncés #check-és du noyau, axiomes audités. Séparer : quatre énoncés distincts qui se répondent sans se confondre. L’arithmétisation n’a pas été refaite — elle vit dans Foundation, consommée en CONSUMER_PINNÉ, et c’est précisément le contrat de l’Epic.