Tweety-5b — Théorie de l’argumentation de Dung (companion formel natif)

Ce notebook est le companion formel du lake argumentation_lean, dont la lib Argumentation prouve les résultats fondateurs de la théorie de l’argumentation abstraite de Dung (1995) — existence de l’extension grounded comme point fixe de la fonction caractéristique (Knaster–Tarski) — avec zéro sorry.

La théorie de Dung modélise un débat comme un graphe d’arguments reliés par une relation d’attaque, et définit des sémantiques (ensembles d’arguments cohérents et « défendus ») : admissible, complète, grounded, preferred, stable.

Convention de vérification — `#check` natif dans le kernel Lean

Ce notebook est un notebook Lean natif (kernel lean4-wsl) : il importe les modules du lake directement et le compilateur Lean rend les signatures dans le notebook. C’est rendu possible par l’UNLOCK (patch lean4_jupyter + jonction Mathlib #2611).

⚠️ À l’exécution, la première cellule (import) peut prendre ~3 min : le kernel charge les oleans Mathlib via la jonction NTFS. Les suivantes sont instantanées.

1. Import des modules du lake `argumentation_lean`

Le lake est structuré en un module racine + 5 sous-modules (Basic, Characteristic, Extensions, Fundamental, Grounded) sous les namespaces Argumentation / Argumentation.AF. La racine porte ArgLattice — le treillis complet (Set α, ⊆) sur lequel opère la fonction caractéristique (section 4) ; les cinq sous-modules portent les définitions et théorèmes. Le lakefile builde les deux (globs .one + .submodules) ; on importe le tout.

import Argumentation
import Argumentation.Basic
import Argumentation.Characteristic
import Argumentation.Extensions
import Argumentation.Fundamental
import Argumentation.Grounded
open Argumentation

import Argumentation

import Argumentation.Basic

import Argumentation.Characteristic

import Argumentation.Extensions

import Argumentation.Fundamental

import Argumentation.Grounded

open Argumentation

--% env 0

Raw input

{"cmd": "import Argumentation\nimport Argumentation.Basic\nimport Argumentation.Characteristic\nimport Argumentation.Extensions\nimport Argumentation.Fundamental\nimport Argumentation.Grounded\nopen Argumentation"}

Raw output

{"env": 0}

2. Preuve sans `sorry` — `#print axioms`

Le théorème phare grounded_fixed (point fixe de l’extension grounded) ne dépend que des 3 axiomes standards de Lean (propext, Classical.choice, Quot.sound) — pas de sorryAx — ce qui prouve que la preuve est complète (0 sorry).

#print axioms AF.grounded_fixed

#print axioms AF.grounded_fixed 'Argumentation.AF.grounded_fixed' depends on axioms: [propext, Classical.choice, Quot.sound]

--% env 1

Raw input

{"cmd": "#print axioms AF.grounded_fixed", "env": 0}

Raw output

{"messages":
 [{"severity": "info",
   "pos": {"line": 1, "column": 0},
   "endPos": {"line": 1, "column": 6},
   "data":
   "'Argumentation.AF.grounded_fixed' depends on axioms: [propext, Classical.choice, Quot.sound]"}],
 "env": 1}

3. Cadre d’argumentation (Dung) — sans-conflit, défense

Le module Argumentation/Basic.lean pose le cadre abstrait de Dung :

AF α — un type d’arguments α muni d’une relation d’attaque attacks : α → α → Prop.
conflictFree S — un ensemble est sans conflit si aucun de ses membres n’en attaque un autre (Définition 1).
defends S a — a est défendu par S si tout attaquant de a est contre-attaqué par un membre de S (Définition 3).

La monotonie de la défense (defends_mono) est le fait combinatoire clé : si S ⊆ T et S défend a, alors T défend aussi a. C’est la croissance de la fonction caractéristique, cœur du point fixe de Dung.

#check AF
#check AF.conflictFree
#check AF.defends
#check AF.conflictFree_empty
#check AF.defends_mono

#check AF Argumentation.AF.{u_2} (α : Type u_2) : Type u_2

#check AF.conflictFree Argumentation.AF.conflictFree.{u_1} {α : Type u_1} (af : AF α) (S : Set α) : Prop

#check AF.defends Argumentation.AF.defends.{u_1} {α : Type u_1} (af : AF α) (S : Set α) (a : α) : Prop

#check AF.conflictFree_empty Argumentation.AF.conflictFree_empty.{u_1} {α : Type u_1} (af : AF α) : af.conflictFree ∅

#check AF.defends_mono Argumentation.AF.defends_mono.{u_1} {α : Type u_1} (af : AF α) {S T : Set α} (hST : S ⊆ T) {a : α}
  (hS : af.defends S a) : af.defends T a

--% env 2

Raw input

{"cmd": "#check AF\n#check AF.conflictFree\n#check AF.defends\n#check AF.conflictFree_empty\n#check AF.defends_mono", "env": 1}

Raw output

{"messages":
 [{"severity": "info",
   "pos": {"line": 1, "column": 0},
   "endPos": {"line": 1, "column": 6},
   "data": "Argumentation.AF.{u_2} (α : Type u_2) : Type u_2"},
  {"severity": "info",
   "pos": {"line": 2, "column": 0},
   "endPos": {"line": 2, "column": 6},
   "data":
   "Argumentation.AF.conflictFree.{u_1} {α : Type u_1} (af : AF α) (S : Set α) : Prop"},
  {"severity": "info",
   "pos": {"line": 3, "column": 0},
   "endPos": {"line": 3, "column": 6},
   "data":
   "Argumentation.AF.defends.{u_1} {α : Type u_1} (af : AF α) (S : Set α) (a : α) : Prop"},
  {"severity": "info",
   "pos": {"line": 4, "column": 0},
   "endPos": {"line": 4, "column": 6},
   "data":
   "Argumentation.AF.conflictFree_empty.{u_1} {α : Type u_1} (af : AF α) : af.conflictFree ∅"},
  {"severity": "info",
   "pos": {"line": 5, "column": 0},
   "endPos": {"line": 5, "column": 6},
   "data":
   "Argumentation.AF.defends_mono.{u_1} {α : Type u_1} (af : AF α) {S T : Set α} (hST : S ⊆ T) {a : α}\n  (hS : af.defends S a) : af.defends T a"}],
 "env": 2}

Lecture : modélisation d’un débat

Symbole Lean	Lecture
`AF α`	cadre d’argumentation : type `α` + relation d’attaque
`conflictFree S`	aucun membre de `S` n’en attaque un autre
`defends S a`	tout attaquant de `a` est contre-attaqué par `S`
`conflictFree_empty`	l’ensemble vide est trivialement sans conflit
`defends_mono`	la défense est monotone en l’ensemble défenseur

4. Le treillis complet des ensembles d’arguments — `ArgLattice`

Le module racine Argumentation.lean nomme le socle sur lequel toute la théorie opère : ArgLattice α, l’abbrev du treillis complet (Set α, ⊆).

Knaster–Tarski exige exactement cette structure — un ordre où toute famille admet un sup et un inf — pour garantir qu’un morphisme monotone comme la fonction caractéristique F possède un plus petit point fixe. C’est ce treillis qui donne son sens à l’écriture grounded = F.lfp :

les joins sont les unions arbitraires ⋃₀, les meets les intersections ⋂₀ ;
l’instance CompleteLattice de Mathlib pour Set α traverse l’abbrev sans redéfinition ;
ArgLattice est le nom sous lequel le lake rend cette hypothèse explicite.

-- Module racine Argumentation.lean : ArgLattice, le treillis ou vit F
#check ArgLattice
#check @Argumentation.ArgLattice

-- ArgLattice n'est qu'un abbrev de Set alpha : la definition se deplie par rfl
example : ArgLattice Nat = Set Nat := rfl

-- L'instance CompleteLattice de Mathlib traverse l'abbrev sans redefinition :
-- le sup d'une famille est son union (sSup = iUnion id)
#check (inferInstance : CompleteLattice (ArgLattice Nat))
example (S : Set (ArgLattice Nat)) : sSup S = ⋃₀ S := rfl

-- Module racine Argumentation.lean : ArgLattice, le treillis ou vit F

#check ArgLattice Argumentation.ArgLattice.{u_1} (α : Type u_1) : Type u_1

#check @Argumentation.ArgLattice ArgLattice : Type u_1 → Type u_1

-- ArgLattice n'est qu'un abbrev de Set alpha : la definition se deplie par rfl

example : ArgLattice Nat = Set Nat := rfl

-- L'instance CompleteLattice de Mathlib traverse l'abbrev sans redefinition :

-- le sup d'une famille est son union (sSup = iUnion id)

#check (inferInstance : CompleteLattice (ArgLattice Nat)) inferInstance : CompleteLattice (ArgLattice ℕ)

example (S : Set (ArgLattice Nat)) : sSup S = ⋃₀ S := rfl

--% env 3

Raw input

{"cmd": "-- Module racine Argumentation.lean : ArgLattice, le treillis ou vit F\n#check ArgLattice\n#check @Argumentation.ArgLattice\n\n-- ArgLattice n'est qu'un abbrev de Set alpha : la definition se deplie par rfl\nexample : ArgLattice Nat = Set Nat := rfl\n\n-- L'instance CompleteLattice de Mathlib traverse l'abbrev sans redefinition :\n-- le sup d'une famille est son union (sSup = iUnion id)\n#check (inferInstance : CompleteLattice (ArgLattice Nat))\nexample (S : Set (ArgLattice Nat)) : sSup S = \u22c3\u2080 S := rfl", "env": 2}

Raw output

{"messages":
 [{"severity": "info",
   "pos": {"line": 2, "column": 0},
   "endPos": {"line": 2, "column": 6},
   "data": "Argumentation.ArgLattice.{u_1} (α : Type u_1) : Type u_1"},
  {"severity": "info",
   "pos": {"line": 3, "column": 0},
   "endPos": {"line": 3, "column": 6},
   "data": "ArgLattice : Type u_1 → Type u_1"},
  {"severity": "info",
   "pos": {"line": 10, "column": 0},
   "endPos": {"line": 10, "column": 6},
   "data": "inferInstance : CompleteLattice (ArgLattice ℕ)"}],
 "env": 3}

Lecture : le treillis complet, l’hypothèse exacte de Knaster–Tarski

Symbole Lean	Lecture
`ArgLattice α`	le treillis complet `(Set α, ⊆)`, nommé par le module racine
`CompleteLattice (ArgLattice α)`	instance héritée de `Set α` à travers l’`abbrev`
`sSup S = ⋃₀ S`	le sup d’une famille d’ensembles est son union
`F.lfp`	le plus petit point fixe — existe parce que le treillis est complet

La complétude — un sup et un inf pour toute famille, pas seulement les paires — est l’hypothèse du théorème de Knaster–Tarski : c’est elle qui garantit l’existence de F.lfp, donc de l’extension grounded. Le module racine la rend explicite en nommant le treillis sur lequel F opère.

5. La fonction caractéristique comme morphisme monotone

Le module Argumentation/Characteristic.lean définit la fonction caractéristique de Dung F(S) = { a | S défend a }, bundlée comme un morphisme d’ordre monotone OrderHom sur le treillis complet Set α. L’extension grounded en est le plus petit point fixe F.lfp — c’est le théorème phare grounded_fixed.

L’identité a ∈ F(S) ⇔ S défend a (mem_characteristic_iff) rend la réécriture directe.

#check AF.characteristic
#check AF.mem_characteristic_iff
#check AF.characteristic_eq_defendedBy

#check AF.characteristic Argumentation.AF.characteristic.{u_1} {α : Type u_1} (af : AF α) : Set α →o Set α

#check AF.mem_characteristic_iff Argumentation.AF.mem_characteristic_iff.{u_1} {α : Type u_1} (af : AF α) (S : Set α) (a : α) :
  a ∈ af.characteristic S ↔ af.defends S a

#check AF.characteristic_eq_defendedBy Argumentation.AF.characteristic_eq_defendedBy.{u_1} {α : Type u_1} (af : AF α) (S : Set α) :
  af.characteristic S = af.defendedBy S

--% env 4

Raw input

{"cmd": "#check AF.characteristic\n#check AF.mem_characteristic_iff\n#check AF.characteristic_eq_defendedBy", "env": 3}

Raw output

{"messages":
 [{"severity": "info",
   "pos": {"line": 1, "column": 0},
   "endPos": {"line": 1, "column": 6},
   "data":
   "Argumentation.AF.characteristic.{u_1} {α : Type u_1} (af : AF α) : Set α →o Set α"},
  {"severity": "info",
   "pos": {"line": 2, "column": 0},
   "endPos": {"line": 2, "column": 6},
   "data":
   "Argumentation.AF.mem_characteristic_iff.{u_1} {α : Type u_1} (af : AF α) (S : Set α) (a : α) :\n  a ∈ af.characteristic S ↔ af.defends S a"},
  {"severity": "info",
   "pos": {"line": 3, "column": 0},
   "endPos": {"line": 3, "column": 6},
   "data":
   "Argumentation.AF.characteristic_eq_defendedBy.{u_1} {α : Type u_1} (af : AF α) (S : Set α) :\n  af.characteristic S = af.defendedBy S"}],
 "env": 4}

Lecture : `F` est un morphisme d’ordre

Symbole Lean	Lecture
`AF.characteristic`	`Set α →o Set α` (OrderHom monotone)
`mem_characteristic_iff`	`a ∈ F(S) ⇔ defends S a`
`characteristic_eq_defendedBy`	`F(S) = defendedBy S` (identité)

6. Les cinq extensions et leur hiérarchie

Le module Argumentation/Extensions.lean définit les cinq sémantiques de Dung, de la plus faible à la plus forte :

Admissible S — sans conflit + défend chacun de ses membres (Définition 5).
Complete S — admissible + contient tout argument qu’elle défend (Définition 7).
grounded — le plus petit point fixe de F (Knaster–Tarski), l’extension minimale.
Preferred S — extension complète maximale pour l’inclusion (Définition 10).
Stable S — sans conflit + attaque tout argument hors de S (Définition 12).

#check AF.Admissible
#check AF.Complete
#check AF.grounded
#check AF.Preferred
#check AF.Stable

#check AF.Admissible Argumentation.AF.Admissible.{u_1} {α : Type u_1} (af : AF α) (S : Set α) : Prop

#check AF.Complete Argumentation.AF.Complete.{u_1} {α : Type u_1} (af : AF α) (S : Set α) : Prop

#check AF.grounded Argumentation.AF.grounded.{u_1} {α : Type u_1} (af : AF α) : Set α

#check AF.Preferred Argumentation.AF.Preferred.{u_1} {α : Type u_1} (af : AF α) (S : Set α) : Prop

#check AF.Stable Argumentation.AF.Stable.{u_1} {α : Type u_1} (af : AF α) (S : Set α) : Prop

--% env 5

Raw input

{"cmd": "#check AF.Admissible\n#check AF.Complete\n#check AF.grounded\n#check AF.Preferred\n#check AF.Stable", "env": 4}

Raw output

{"messages":
 [{"severity": "info",
   "pos": {"line": 1, "column": 0},
   "endPos": {"line": 1, "column": 6},
   "data":
   "Argumentation.AF.Admissible.{u_1} {α : Type u_1} (af : AF α) (S : Set α) : Prop"},
  {"severity": "info",
   "pos": {"line": 2, "column": 0},
   "endPos": {"line": 2, "column": 6},
   "data":
   "Argumentation.AF.Complete.{u_1} {α : Type u_1} (af : AF α) (S : Set α) : Prop"},
  {"severity": "info",
   "pos": {"line": 3, "column": 0},
   "endPos": {"line": 3, "column": 6},
   "data":
   "Argumentation.AF.grounded.{u_1} {α : Type u_1} (af : AF α) : Set α"},
  {"severity": "info",
   "pos": {"line": 4, "column": 0},
   "endPos": {"line": 4, "column": 6},
   "data":
   "Argumentation.AF.Preferred.{u_1} {α : Type u_1} (af : AF α) (S : Set α) : Prop"},
  {"severity": "info",
   "pos": {"line": 5, "column": 0},
   "endPos": {"line": 5, "column": 6},
   "data":
   "Argumentation.AF.Stable.{u_1} {α : Type u_1} (af : AF α) (S : Set α) : Prop"}],
 "env": 5}

7. La Fundamental Lemma de Dung

Le module Argumentation/Fundamental.lean prouve la Fundamental Lemma (Dung 1995, Lemme 1) : si S est admissible et défend a, alors S ∪ {a} est admissible. C’est la clé de l’existence des extensions preferred — elle garantit qu’on peut toujours étendre une extension admissible défendable, d’où l’existence de maximaux.

#check AF.fundamental_lemma
#check AF.fundamental_lemma_defends
#check AF.fundamental_lemma_defends_self

#check AF.fundamental_lemma Argumentation.AF.fundamental_lemma.{u_1} {α : Type u_1} (af : AF α) {S : Set α} {a : α} (hS : af.Admissible S)
  (ha : af.defends S a) : af.Admissible (insert a S)

#check AF.fundamental_lemma_defends Argumentation.AF.fundamental_lemma_defends.{u_1} {α : Type u_1} (af : AF α) {S : Set α} {a b : α} (hS : af.Admissible S)
  (ha : af.defends S a) (hb : af.defends S b) : af.defends (insert a S) b

#check AF.fundamental_lemma_defends_self Argumentation.AF.fundamental_lemma_defends_self.{u_1} {α : Type u_1} (af : AF α) {S : Set α} {a : α}
  (hS : af.Admissible S) (ha : af.defends S a) : af.defends (insert a S) a

--% env 6

Raw input

{"cmd": "#check AF.fundamental_lemma\n#check AF.fundamental_lemma_defends\n#check AF.fundamental_lemma_defends_self", "env": 5}

Raw output

{"messages":
 [{"severity": "info",
   "pos": {"line": 1, "column": 0},
   "endPos": {"line": 1, "column": 6},
   "data":
   "Argumentation.AF.fundamental_lemma.{u_1} {α : Type u_1} (af : AF α) {S : Set α} {a : α} (hS : af.Admissible S)\n  (ha : af.defends S a) : af.Admissible (insert a S)"},
  {"severity": "info",
   "pos": {"line": 2, "column": 0},
   "endPos": {"line": 2, "column": 6},
   "data":
   "Argumentation.AF.fundamental_lemma_defends.{u_1} {α : Type u_1} (af : AF α) {S : Set α} {a b : α} (hS : af.Admissible S)\n  (ha : af.defends S a) (hb : af.defends S b) : af.defends (insert a S) b"},
  {"severity": "info",
   "pos": {"line": 3, "column": 0},
   "endPos": {"line": 3, "column": 6},
   "data":
   "Argumentation.AF.fundamental_lemma_defends_self.{u_1} {α : Type u_1} (af : AF α) {S : Set α} {a : α}\n  (hS : af.Admissible S) (ha : af.defends S a) : af.defends (insert a S) a"}],
 "env": 6}

8. Théorème phare : le point fixe de l’extension grounded

Le module Argumentation/Grounded.lean prouve le résultat central :

grounded_fixed : F(grounded) = grounded — l’extension grounded est un point fixe de la fonction caractéristique (identité de Knaster–Tarski via OrderHom.map_lfp).
grounded_defends_iff_mem : a ∈ grounded ⇔ grounded défend a.
grounded_least_complete : grounded est la plus petite extension complète.

#check AF.grounded_fixed
#check AF.grounded_defends_iff_mem
#check AF.grounded_least_complete

#check AF.grounded_fixed Argumentation.AF.grounded_fixed.{u_1} {α : Type u_1} (af : AF α) : af.characteristic af.grounded = af.grounded

#check AF.grounded_defends_iff_mem Argumentation.AF.grounded_defends_iff_mem.{u_1} {α : Type u_1} (af : AF α) (a : α) :
  af.defends af.grounded a ↔ a ∈ af.grounded

#check AF.grounded_least_complete Argumentation.AF.grounded_least_complete.{u_1} {α : Type u_1} (af : AF α) (T : Set α) (h : af.Complete T) :
  af.grounded ⊆ T

--% env 7

Raw input

{"cmd": "#check AF.grounded_fixed\n#check AF.grounded_defends_iff_mem\n#check AF.grounded_least_complete", "env": 6}

Raw output

{"messages":
 [{"severity": "info",
   "pos": {"line": 1, "column": 0},
   "endPos": {"line": 1, "column": 6},
   "data":
   "Argumentation.AF.grounded_fixed.{u_1} {α : Type u_1} (af : AF α) : af.characteristic af.grounded = af.grounded"},
  {"severity": "info",
   "pos": {"line": 2, "column": 0},
   "endPos": {"line": 2, "column": 6},
   "data":
   "Argumentation.AF.grounded_defends_iff_mem.{u_1} {α : Type u_1} (af : AF α) (a : α) :\n  af.defends af.grounded a ↔ a ∈ af.grounded"},
  {"severity": "info",
   "pos": {"line": 3, "column": 0},
   "endPos": {"line": 3, "column": 6},
   "data":
   "Argumentation.AF.grounded_least_complete.{u_1} {α : Type u_1} (af : AF α) (T : Set α) (h : af.Complete T) :\n  af.grounded ⊆ T"}],
 "env": 7}

Lecture : grounded = plus petit point fixe (Knaster–Tarski)

Théorème	Conclusion
`grounded_fixed`	`F(grounded) = grounded` (point fixe)
`grounded_defends_iff_mem`	`a ∈ grounded ⇔ grounded défend a`
`grounded_least_complete`	`grounded ⊆ T` pour toute extension complète `T`

L’extension grounded est donc la plus prudente : exactement ce que tout argument défendu itérativement à partir de l’ensemble vide.

9. La chaîne causale complète

Les six modules composent une chaîne unique, du treillis au point fixe :

Racine — ArgLattice, le treillis complet (Set α, ⊆) (le socle de Knaster–Tarski).
Basic — cadre AF, sans-conflit, défense, monotonie (defends_mono).
Characteristic — F : Set α →o Set α morphisme monotone (la croissance).
Extensions — les 5 sémantiques (Admissible → Complete → grounded → Preferred → Stable).
Fundamental — la Fundamental Lemma (étendre un admissible défendable ⟹ admissible).
Grounded — F(grounded) = grounded (point fixe ⟹ grounded est la plus petite complète).

10. Exercices

Exercice 1 — Sans-conflit et défense sur un mini-cadre (Python)

Ancrez l’intuition sur un exemple concret : un cadre à 3 arguments {a, b, c} où a attaque b et b attaque c. Quels ensembles sont sans conflit ? Lequel défend c ?

attacks = {('a','b'), ('b','c')}
args = ['a', 'b', 'c']
def conflict_free(S, attacks):
    # TODO etudiant : un ensemble S est sans-conflit si aucune attaque n'a
    #                ses deux extremites dans S.
    return None  # TODO

Exercice 2 — L’ensemble vide est sans conflit

Prouvez en Lean que l’ensemble vide est sans conflit (c’est un cas particulier de conflictFree_empty, mais essayez de le refaire à la main).

-- TODO etudiant : formaliser conflictFree_empty a la main
-- example (af : AF α) : af.conflictFree (∅ : Set α) := by sorry

Exercice 3 — Un cadre sans extension stable (contre-exemple)

Un cycle de 3 arguments (a attaque b, b attaque c, c attaque a) n’admet pas d’extension stable : tout ensemble sans-conflit laisse au moins un argument non attaqué. Justifiez sur papier, puis proposez la formalisation Lean du contre-exemple.

-- TODO etudiant : formaliser un cycle a 3 arguments et montrer l'absence d'extension stable
-- def threeCycle : AF (Fin 3) := ⟨fun i j => ...⟩
-- example : ¬ ∃ S, (threeCycle).Stable S := by sorry

Conclusion

Ce companion natif exhibe la preuve formelle 0-sorry de la théorie de l’argumentation de Dung dans le kernel Lean lui-même : #check et #print axioms rendent les signatures et les axiomes réels produits par le compilateur, sans intermédiaire Python.

Le résultat phare grounded_fixed — l’extension grounded est le point fixe de la fonction caractéristique — formalise l’un des piliers de l’argumentation computationnelle (Dung 1995), via Knaster–Tarski (OrderHom.map_lfp).

Jalon ouvert : l’existence des extensions preferred (via la Fundamental Lemma + Zorn) n’est qu’esquissée dans le lake ; la lib reste sorry-free.

Retour au sommet

Convention de vérification — #check natif dans le kernel Lean

1. Import des modules du lake argumentation_lean

2. Preuve sans sorry — #print axioms

3. Cadre d’argumentation (Dung) — sans-conflit, défense

Lecture : modélisation d’un débat

4. Le treillis complet des ensembles d’arguments — ArgLattice

Lecture : le treillis complet, l’hypothèse exacte de Knaster–Tarski

5. La fonction caractéristique comme morphisme monotone

Lecture : F est un morphisme d’ordre

6. Les cinq extensions et leur hiérarchie

7. La Fundamental Lemma de Dung

8. Théorème phare : le point fixe de l’extension grounded

Lecture : grounded = plus petit point fixe (Knaster–Tarski)

9. La chaîne causale complète

10. Exercices

Exercice 1 — Sans-conflit et défense sur un mini-cadre (Python)

Exercice 2 — L’ensemble vide est sans conflit

Exercice 3 — Un cadre sans extension stable (contre-exemple)

Conclusion

Convention de vérification — `#check` natif dans le kernel Lean

1. Import des modules du lake `argumentation_lean`

2. Preuve sans `sorry` — `#print axioms`

4. Le treillis complet des ensembles d’arguments — `ArgLattice`

Lecture : `F` est un morphisme d’ordre