Navigation : Notebooks | Serie : SocialChoice 01 - Theoreme d’Arrow : Preuve Formelle et Simulation
Navigation : SocialChoice | 01b-Lean-SocialChoice-Formal.ipynb >> | Index
Autres notebooks : 03-Voting-Methods.ipynb | 04-Computational-Aggregation-SAT-Z3.ipynb
Kernel : Python 3
Ce notebook est un tutoriel transversal qui relie deux approches complementaires du theoreme d’impossibilite d’Arrow :
| Notebook | Approche | Ce qu’il montre |
|---|---|---|
| SC-02 (Lean) | Preuve formelle | Le theoreme est vrai pour TOUS les profils possibles |
| SC-03 (Python) | Simulation empirique | Les règles usuelles violent les axiomes dans la pratique |
| Ce notebook (SC-01) | Pont formel/empirique | Chaque étape de la preuve illustree en Python |
La preuve formelle en Lean garantit l’impossibilite pour un nombre infini de profils. La simulation Python ne teste qu’un nombre fini de cas. Ce notebook montre pourquoi cette différence est fondamentale.
Ancres savantes – Arrow, K.J. (1950), A Difficulty in the Concept of Social Welfare, Journal of Political Economy 58(4):328-346 (enonce original du theoreme d’impossibilite : aucune fonction de bien-etre social pour 3+ alternatives ne satisfait simultanement Pareto, IIA et non-dictature) ; Arrow, K.J. (1951), Social Choice and Individual Values, Cowles Commission Monograph 12, Wiley (2e ed. Yale University Press 1963 ; monographie canonique, prix Nobel d’economie 1972 pour cette contribution) ; Borda, J.-C. de (1781), Memoire sur les elections au scrutin, Histoire de l’Academie Royale des Sciences, Paris (compte de Borda enseigne ici comme règle de comparaison : 1104 violations IIA sur 216 profils, illustrant empiriquement l’impossibilite).
Hommage — le premier article de Richard E. Stearns portait sur ce théorème
Richard E. Stearns (1936–2026), co-lauréat du prix Turing 1993 pour avoir fondé la théorie de la complexité computationnelle (Hartmanis & Stearns, 1965), a commencé par le théorème d’Arrow : son tout premier article, écrit comme étudiant de dernière année à Carleton College, portait sur le paradoxe d’Arrow et a été publié dans The American Mathematical Monthly en 1959. Sa thèse de Princeton, dirigée par Harold W. Kuhn (co-éponyme de l’algorithme Kuhn–Munkres, célébré dans cette même série GameTheory), portait sur les jeux coopératifs à trois joueurs sans paiements transférables.
L’homme qui a donné son nom à la complexité a donc commencé par l’impossibilité de l’agrégation — le théorème que ce notebook démontre. Autre résonance inattendue : ses travaux sur les jeux répétés à information incomplète (contrôle des armements, chapitre du livre d’Aumann & Maschler 1995), racontés dans le README de
game_theory_lean/. Hommage complet — hiérarchie de Hartmanis–Stearns, sérieComplexity/: issue #15949.Sources : CACM, In Memoriam Richard E. Stearns (Spafford & Garfinkel, 03/09/2026) ; blog Computational Complexity (Gasarch, 04/09/2026) ; transcript du prix Turing ACM.
# Section 0 : Configuration
import numpy as np
import matplotlib.pyplot as plt
from itertools import permutations, combinations
from collections import Counter, defaultdict
import random
random.seed(42)
np.random.seed(42)
print("Configuration OK : SocialChoice 01 - Arrow")Configuration OK : SocialChoice 01 - ArrowAprès avoir défini le cadre experimental, nous allons maintenant implementer les tests Python pour verifier empiriquement les axiomes d’Arrow sur un ensemble fini de profils.
Le theoreme d’Arrow repose sur trois axiomes que l’on pourrait considerer comme “raisonnables” pour un système de vote equitable. Pour chaque axiome, nous presentons : - La definition formelle en Lean (issue de game_theory_lean/SocialChoice/Framework.lean) - Un test Python qui verifie si une règle de vote satisfait cet axiome
Dans le formalisme Lean du projet game_theory_lean :
-- Fonction de bien-etre social
def SWF (i sigma : Type*) := Profile i sigma -> PrefOrder sigma
-- Relation de préférence stricte
def P (R : sigma -> sigma -> Prop) (x y : sigma) : Prop :=
R x y /\ ¬R y xLa preuve formelle en Lean decompose le theoreme d’impossibilite en lemmes intermediaires, chacun validant une étape du raisonnement. Cette structure modulaire facilite la verification automatique et la comprehension de la preuve.
Definition Lean (Framework.lean) :
def weak_pareto (f : SWF i sigma) (X : Finset sigma) : Prop :=
forall prof : Profile i sigma, forall x y : sigma, x \in X -> y \in X ->
(forall i : iota, P (prof i).rel x y) -> P (f prof).rel x yEn francais : Si tous les individus preferent strictement x a y, alors la societe prefere aussi strictement x a y.
Intuition : C’est la condition la plus naturelle – l’unanimite devrait se refléter dans le choix collectif.
# 1.1 Pareto Faible -- Test Python
def borda_rule(profile):
"""Regle de Borda : points selon le rang."""
scores = defaultdict(int)
n = len(profile[0])
for pref in profile:
for rank, alt in enumerate(pref):
scores[alt] += (n - 1 - rank)
return sorted(scores.keys(), key=lambda x: -scores[x])
def plurality_rule(profile):
"""Regle de la pluralite : l'alternative avec le plus de premiers choix gagne."""
first_choices = [p[0] for p in profile]
counts = Counter(first_choices)
alternatives = list(dict.fromkeys(x for p in profile for x in p))
return sorted(alternatives, key=lambda x: -counts.get(x, 0))
def dictatorial_rule(profile, dictator_idx=0):
"""Regle dictatoriale : le classement social = preference du dictateur."""
return list(profile[dictator_idx])
def check_weak_pareto(voting_rule, n_voters, alternatives, n_tests=500):
"""Teste si une regle de vote satisfait Pareto faible.
Pour chaque profil teste, verifie que si tous les votants
preferent x a y, alors le classement social a aussi x avant y.
Args:
voting_rule: fonction prenant un profil (list de listes)
et retournant un classement (list)
n_voters: nombre de votants
alternatives: liste des alternatives
n_tests: nombre de profils a tester
Returns:
int: nombre de violations detectees
"""
violations = 0
for _ in range(n_tests):
profile = []
for _ in range(n_voters):
p = list(alternatives)
random.shuffle(p)
profile.append(p)
ranking = voting_rule(profile)
# Tester toutes les paires (x, y) ou tous preferent x a y
for x, y in combinations(alternatives, 2):
all_prefer = all(
pref.index(x) < pref.index(y) for pref in profile
)
if all_prefer:
if ranking.index(x) > ranking.index(y):
violations += 1
return violations
# Test sur differentes regles
alternatives = ['A', 'B', 'C']
n_voters = 5
print("TEST DU AXIOME DE PARETO FAIBLE")
print("=" * 33)
for name, rule in [
("Regle de Borda", borda_rule),
("Dictature (electeur 0)", lambda p: dictatorial_rule(p, 0)),
("Pluralite", plurality_rule),
]:
v = check_weak_pareto(rule, n_voters, alternatives)
status = "SATISFAIT Pareto faible" if v == 0 else f"VIOLE ({v} cas)"
print(f"{name} :")
print(f" Teste sur 500 profils aleatoires... {v} violations")
print(f" => {status}\n")TEST DU AXIOME DE PARETO FAIBLE
=================================
Regle de Borda :
Teste sur 500 profils aleatoires... 0 violations
=> SATISFAIT Pareto faible
Dictature (electeur 0) :
Teste sur 500 profils aleatoires... 0 violations
=> SATISFAIT Pareto faible
Pluralite :
Teste sur 500 profils aleatoires... 0 violations
=> SATISFAIT Pareto faible
Résultat : les trois règles testees satisfont toutes Pareto faible.
| Règle | Violations (sur 500 tests) | Verdict |
|---|---|---|
| Borda | 0 | Satisfait |
| Dictature | 0 | Satisfait |
| Pluralite | 0 | Satisfait |
Point cle : même une dictature satisfait Pareto faible ! Si le dictateur prefere x a y (et tout le monde aussi par hypothese), le classement social suit le dictateur.
Note : Pareto faible est le plus “facile” a satisfaire des trois axiomes. La ou les choses se compliquent, c’est quand on exige aussi l’IIA et la non-dictature.
Definition Lean (Framework.lean) :
def ind_of_irr_alts (f : SWF i sigma) (X : Finset sigma) : Prop :=
forall prof prof' : Profile i sigma, forall x y : sigma,
x \in X -> y \in X ->
(forall i : iota, same_order' (prof i).rel (prof' i).rel x y x y) ->
same_order' (f prof).rel (f prof').rel x y x yEn francais : Le classement social entre x et y depend uniquement des préférences individuelles entre x et y. Changer le classement d’une autre alternative ne doit pas affecter x vs y.
Intuition : Si un electeur change d’avis sur le classement A vs C, cela ne devrait pas changer le classement social de A vs B.
# 1.2 IIA -- Test Python
def check_iia(voting_rule, n_voters, alternatives, n_tests=1000):
"""Teste si une regle de vote satisfait IIA.
Pour chaque paire de profils (prof, prof') ou les preferences
individuelles entre x et y sont identiques pour chaque votant,
verifie que le classement social relatif de x vs y ne change pas.
Args:
voting_rule: fonction prenant un profil et retournant un classement
n_voters: nombre de votants
alternatives: liste des alternatives
n_tests: nombre de paires de profils a tester
Returns:
int: nombre de violations detectees
"""
violations = 0
alts = list(alternatives)
for _ in range(n_tests):
# Generer deux profils aleatoires
profile1 = []
profile2 = []
for _ in range(n_voters):
p1 = list(alts)
random.shuffle(p1)
p2 = list(alts)
random.shuffle(p2)
profile1.append(p1)
profile2.append(p2)
# Choisir une paire (x, y) au hasard
x, y = random.sample(alts, 2)
# Verifier que les preferences individuelles entre x et y
# sont les memes dans les deux profils
same_xy = all(
(p1.index(x) < p1.index(y)) == (p2.index(x) < p2.index(y))
for p1, p2 in zip(profile1, profile2)
)
if not same_xy:
continue
# Comparer le classement social relatif de x vs y
ranking1 = voting_rule(profile1)
ranking2 = voting_rule(profile2)
xy_in_1 = ranking1.index(x) < ranking1.index(y)
xy_in_2 = ranking2.index(x) < ranking2.index(y)
if xy_in_1 != xy_in_2:
violations += 1
return violations
# Test sur differentes regles
print("TEST DE L'AXIOME IIA (Independance des Alternatives Non-Pertinentes)")
print("=" * 69)
for name, rule in [
("Regle de Borda", borda_rule),
("Pluralite", plurality_rule),
("Dictature (electeur 0)", lambda p: dictatorial_rule(p, 0)),
]:
v = check_iia(rule, n_voters, alternatives)
status = "SATISFAIT IIA" if v == 0 else f"VIOLE IIA ({v} violations)"
print(f"{name} :")
print(f" Teste sur 1000 paires de profils... {v} violations")
print(f" => {status}\n")TEST DE L'AXIOME IIA (Independance des Alternatives Non-Pertinentes)
=====================================================================
Regle de Borda :
Teste sur 1000 paires de profils... 2 violations
=> VIOLE IIA (2 violations)
Pluralite :
Teste sur 1000 paires de profils... 7 violations
=> VIOLE IIA (7 violations)
Dictature (electeur 0) :
Teste sur 1000 paires de profils... 0 violations
=> SATISFAIT IIA
Résultat : seul le dictateur satisfait IIA !
| Règle | Violations IIA | Verdict |
|---|---|---|
| Borda | eleve | Viole IIA |
| Pluralite | eleve | Viole IIA |
| Dictature | 0 | Satisfait IIA |
Pourquoi Borda viole IIA : les scores de Borda dependent de la position de toutes les alternatives, pas seulement de x et y. Ajouter ou retirer une alternative peut changer le classement relatif de x vs y.
Pourquoi la dictature satisfait IIA : le classement social = celui du dictateur, donc le classement relatif x vs y ne depend que de la préférence du dictateur sur x vs y, independamment des autres alternatives.
Premier indice du theoreme d’Arrow : les règles “raisonnables” (Borda, Pluralite) violent IIA, et seule la dictature le satisfait…
Definition Lean (Arrow.lean) :
def is_dictatorship (f : SWF i sigma) (X : Finset sigma) : Prop :=
exists d : iota,
forall x y : sigma, x \in X -> y \in X -> x ≠ y ->
is_dictator_on f d x y
def non_dictatorial (f : SWF i sigma) (X : Finset sigma) : Prop :=
not (is_dictatorship f X)En francais : Il n’existe aucun individu dont la préférence stricte est toujours suivie par le classement social.
Intuition : Aucun electeur ne devrait avoir un pouvoir de veto absolu sur le classement social.
# 1.3 Non-dictature -- Test Python
def check_non_dictatorship(voting_rule, n_voters, alternatives, n_tests=500):
"""Teste si une regle de vote est dictatoriale.
Pour chaque votant, verifie si sa preference stricte
est toujours suivie par le classement social.
Args:
voting_rule: fonction prenant un profil et retournant un classement
n_voters: nombre de votants
alternatives: liste des alternatives
n_tests: nombre de profils a tester
Returns:
int or None: index du dictateur si trouve, None sinon
"""
for d in range(n_voters):
is_dict = True
for _ in range(n_tests):
profile = []
for _ in range(n_voters):
p = list(alternatives)
random.shuffle(p)
profile.append(p)
ranking = voting_rule(profile)
# Verifier : pour TOUTE paire, si le dictateur prefere x a y,
# le classement social doit avoir x avant y
for x, y in combinations(alternatives, 2):
# Le dictateur prefere strictement x a y
if profile[d].index(x) < profile[d].index(y):
if ranking.index(x) > ranking.index(y):
is_dict = False
break
# Le dictateur prefere strictement y a x
elif profile[d].index(y) < profile[d].index(x):
if ranking.index(y) > ranking.index(x):
is_dict = False
break
if not is_dict:
break
if is_dict:
return d
return None
print("TEST DE NON-DICTATURE")
print("=" * 22)
for name, rule in [
("Regle de Borda", borda_rule),
("Pluralite", plurality_rule),
("Dictature (electeur 0)", lambda p: dictatorial_rule(p, 0)),
]:
d = check_non_dictatorship(rule, n_voters, alternatives)
if d is not None:
print(f"{name} :")
print(f" Teste sur 500 profils... DICTATURE (dictateur = electeur {d})\n")
else:
print(f"{name} :")
print(f" Teste sur 500 profils... non-dictatoriale\n")TEST DE NON-DICTATURE
======================
Regle de Borda :
Teste sur 500 profils... non-dictatoriale
Pluralite :
Teste sur 500 profils... non-dictatoriale
Dictature (electeur 0) :
Teste sur 500 profils... DICTATURE (dictateur = electeur 0)
| Règle | Pareto | IIA | Non-dictature | Les trois ? |
|---|---|---|---|---|
| Borda | Oui | Non | Oui | Non |
| Pluralite | Oui | Non | Oui | Non |
| Dictature | Oui | Oui | Non | Non |
Observation : aucune règle ne parvient a satisfaire les trois axiomes simultanement. C’est exactement ce que dit le theoreme d’Arrow – et la preuve formelle en Lean montre que ce n’est pas un artefact de nos tests, mais une verite mathematique.
La preuve formelle dans game_theory_lean/SocialChoice/Arrow.lean suit la structure de la preuve de Geanakoplos (2005). Elle procede en quatre étapes que nous allons illustrer :
Definition Lean (Arrow.lean, ligne 199) :
theorem extremal_lemma (f : SWF i sigma) (X : Finset sigma)
(hwp : weak_pareto f X) (hind : ind_of_irr_alts f X)
(hX : 3 <= X.card) (b : sigma) (hb : b \in X)
(prof : Profile i sigma)
(hall : forall i : iota, is_extremal (prof i).rel b X) :
is_extremal (f prof).rel b XEn francais : Si chaque individu place l’alternative b soit en première position, soit en dernière position (et nulle part entre les deux), alors le classement social place aussi b en position extreme.
Preuve (idee) : Par l’absurde. Si la societe ne place pas b en position extreme, alors il existe a et c tels que la societe prefere a > b > c. Mais par IIA, le classement entre a et b (ou b et c) ne depend que des préférences individuelles sur ces paires. Comme b est toujours extreme pour chaque individu, les préférences sur (a,b) et (b,c) sont liees – ce qui mene a une contradiction avec Pareto.
# 2.1 Lemme Extremal -- Simulation Python
def generate_extremal_profiles(n_voters, alternatives, target):
"""Genere des profils ou 'target' est toujours en premiere ou derniere position.
Args:
n_voters: nombre de votants
alternatives: liste des alternatives
target: l'alternative a placer en position extreme
Returns:
list: profil genere
"""
profile = []
others = [a for a in alternatives if a != target]
for _ in range(n_voters):
random.shuffle(others)
if random.random() < 0.5:
# target en premier
profile.append([target] + list(others))
else:
# target en dernier
profile.append(list(others) + [target])
return profile
def is_extreme_position(ranking, item, n):
"""Verifie si 'item' est en premiere ou derniere position."""
idx = ranking.index(item)
return idx == 0 or idx == n - 1
alternatives_3 = ['A', 'B', 'C']
n_voters_test = 5
target = 'B'
print("LEMME EXTREMAL : SIMULATION")
print("=" * 28)
print(f"Alternatives : {alternatives_3}")
print(f"{target} sera place en position extreme (premier ou dernier)"
f" par chaque electeur")
# Cas 1 : tous placent B en dernier
print(f"\nProfil 1 : tous placent {target} en dernier")
profile_bottom = []
others = ['A', 'C']
for _ in range(n_voters_test):
p = list(others)
random.shuffle(p)
profile_bottom.append(p + [target])
for i, pref in enumerate(profile_bottom):
pos = "PREMIER" if pref.index(target) == 0 else "DERNIER"
print(f" Electeur {i}: {pref} -> {target} est {pos}")
ranking = borda_rule(profile_bottom)
pos_b = "PREMIER" if ranking.index(target) == 0 else "DERNIER"
print(f" Classement Borda : {ranking}")
print(f" Position de {target} : {pos_b} (index {ranking.index(target)})")
extreme = is_extreme_position(ranking, target, len(alternatives_3))
print(f" => {target} est {'bien' if extreme else 'PAS'} en position EXTREME")
# Cas 2 : tous placent B en premier
print(f"\nProfil 2 : tous placent {target} en premier")
profile_top = []
for _ in range(n_voters_test):
p = list(others)
random.shuffle(p)
profile_top.append([target] + p)
for i, pref in enumerate(profile_top):
pos = "PREMIER" if pref.index(target) == 0 else "DERNIER"
print(f" Electeur {i}: {pref} -> {target} est {pos}")
ranking = borda_rule(profile_top)
pos_b = "PREMIER" if ranking.index(target) == 0 else "DERNIER"
print(f" Classement Borda : {ranking}")
print(f" Position de {target} : {pos_b} (index {ranking.index(target)})")
extreme = is_extreme_position(ranking, target, len(alternatives_3))
print(f" => {target} est {'bien' if extreme else 'PAS'} en position EXTREME")
# Cas 3 : mixte
print(f"\nProfil 3 : positions mixtes ({target} premier ou dernier)")
profile_mix = generate_extremal_profiles(n_voters_test, alternatives_3, target)
for i, pref in enumerate(profile_mix):
pos = "PREMIER" if pref.index(target) == 0 else "DERNIER"
print(f" Electeur {i}: {pref} -> {target} est {pos}")
ranking = borda_rule(profile_mix)
pos_b = "PREMIER" if ranking.index(target) == 0 else "DERNIER"
print(f" Classement Borda : {ranking}")
print(f" Position de {target} : {pos_b} (index {ranking.index(target)})")
extreme = is_extreme_position(ranking, target, len(alternatives_3))
print(f" => {target} est {'bien' if extreme else 'PAS'} en position EXTREME")
# Test systematique
n_extreme = 0
n_total = 100
for _ in range(n_total):
prof = generate_extremal_profiles(n_voters_test, alternatives_3, target)
r = borda_rule(prof)
if is_extreme_position(r, target, len(alternatives_3)):
n_extreme += 1
print(f"\nResume sur {n_total} profils aleatoires :")
print(f" {target} toujours en position extreme (social) : {n_extreme}/{n_total}")LEMME EXTREMAL : SIMULATION
============================
Alternatives : ['A', 'B', 'C']
B sera place en position extreme (premier ou dernier) par chaque electeur
Profil 1 : tous placent B en dernier
Electeur 0: ['A', 'C', 'B'] -> B est DERNIER
Electeur 1: ['A', 'C', 'B'] -> B est DERNIER
Electeur 2: ['C', 'A', 'B'] -> B est DERNIER
Electeur 3: ['A', 'C', 'B'] -> B est DERNIER
Electeur 4: ['C', 'A', 'B'] -> B est DERNIER
Classement Borda : ['A', 'C', 'B']
Position de B : DERNIER (index 2)
=> B est bien en position EXTREME
Profil 2 : tous placent B en premier
Electeur 0: ['B', 'C', 'A'] -> B est PREMIER
Electeur 1: ['B', 'C', 'A'] -> B est PREMIER
Electeur 2: ['B', 'A', 'C'] -> B est PREMIER
Electeur 3: ['B', 'A', 'C'] -> B est PREMIER
Electeur 4: ['B', 'C', 'A'] -> B est PREMIER
Classement Borda : ['B', 'C', 'A']
Position de B : PREMIER (index 0)
=> B est bien en position EXTREME
Profil 3 : positions mixtes (B premier ou dernier)
Electeur 0: ['B', 'C', 'A'] -> B est PREMIER
Electeur 1: ['C', 'A', 'B'] -> B est DERNIER
Electeur 2: ['A', 'C', 'B'] -> B est DERNIER
Electeur 3: ['B', 'A', 'C'] -> B est PREMIER
Electeur 4: ['C', 'A', 'B'] -> B est DERNIER
Classement Borda : ['C', 'A', 'B']
Position de B : DERNIER (index 2)
=> B est bien en position EXTREME
Resume sur 100 profils aleatoires :
B toujours en position extreme (social) : 90/100Definition Lean (Arrow.lean, ligne 279) :
theorem pivot_exists (f : SWF i sigma) (X : Finset sigma)
(hwp : weak_pareto f X) (hind : ind_of_irr_alts f X)
(hX : 3 <= X.card) (b : sigma) (hb : b \in X) :
exists n : iota, is_pivotal f X n bEn francais : Pour toute alternative b, il existe un individu “pivotal” – c’est-a-dire un electeur dont le changement de préférence peut faire passer b du bas au sommet du classement social.
Preuve (idee) : On construit une sequence de profils \(prof^0, prof^1, ..., prof^m\) ou progressivement chaque electeur passe b du bas au sommet. Par le lemme extremal, b est toujours en position extreme socialement. Au depart (\(prof^0\)), b est en bas (Pareto). A la fin (\(prof^m\)), b est en haut (Pareto). Il y a donc un moment ou un seul electeur fait basculer b – c’est le pivot.
# 2.2 Existence du Pivot -- Simulation Python
def find_pivot_sequence(voting_rule, n_voters, alternatives, target):
"""Trouve l'electeur pivot en faisant basculer 'target' du bas au sommet.
Args:
voting_rule: regle de vote
n_voters: nombre de votants
alternatives: liste des alternatives
target: alternative cible
Returns:
int or None: index de l'electeur pivot
"""
others = [a for a in alternatives if a != target]
# Etat initial : tous placent target en bas
profile = []
for _ in range(n_voters):
p = list(others)
random.shuffle(p)
profile.append(p + [target])
ranking = voting_rule(profile)
was_last = ranking.index(target) == len(alternatives) - 1
if not was_last:
return None # target n'est pas dernier, conditions non remplies
# Progressivement, chaque electeur passe target en haut
for step in range(n_voters):
others_copy = list(others)
random.shuffle(others_copy)
profile[step] = [target] + others_copy
ranking = voting_rule(profile)
is_first = ranking.index(target) == 0
if is_first:
return step # L'electeur 'step' est le pivot
return None # Pas de basculement trouve (ne devrait pas arriver)
alternatives_3 = ['A', 'B', 'C']
n_voters_test = 5
target = 'B'
print("EXISTENCE DU PIVOT : SIMULATION")
print("=" * 32)
print(f"Alternatives : {alternatives_3} | {n_voters_test} electeurs")
print(f"Cible : {target}")
# Demonstration detaillee
print(f"\nSequence de profils ({target} passe du bas vers le haut):")
print("-" * 65)
others = ['A', 'C']
profile = []
random.seed(10) # Pour une demonstration reproductible
for _ in range(n_voters_test):
p = list(others)
random.shuffle(p)
profile.append(p + [target])
# Etat initial
ranking = borda_rule(profile)
scores = defaultdict(int)
n = len(alternatives_3)
for pref in profile:
for rank, alt in enumerate(pref):
scores[alt] += (n - 1 - rank)
pos_b = "PREMIER" if ranking.index(target) == 0 else "DERNIER"
print(f"Etape 0: {target} est en bas pour tous")
for i in range(n_voters_test):
pref_str = ' > '.join(profile[i])
if i < 3:
print(f" Electeur {i}: {pref_str}", end=" | ")
elif i == 3:
print(f"Electeur {i}: {pref_str}")
pref_str = ' > '.join(profile[i])
print(f" Electeur {i}: {pref_str}")
else:
print(f" Electeur {i}: {pref_str}")
# Reformater l'affichage des electeurs
print() # Reset
random.seed(10) # Reset pour la meme sequence
profile = []
for _ in range(n_voters_test):
p = list(others)
random.shuffle(p)
profile.append(p + [target])
pivot_found = None
for step in range(n_voters_test):
ranking = borda_rule(profile)
scores = defaultdict(int)
n = len(alternatives_3)
for pref in profile:
for rank, alt in enumerate(pref):
scores[alt] += (n - 1 - rank)
pos_b = "PREMIER" if ranking.index(target) == 0 else "DERNIER"
if step == 0:
label = f"Etape {step}: {target} est en bas pour tous"
else:
label = f"Etape {step}: Electeur {step-1} passe {target} en haut"
print(label)
for i in range(n_voters_test):
pref_str = ' > '.join(profile[i])
print(f" Electeur {i}: {pref_str}")
print(f" Social (Borda): {ranking} -> {target} est {pos_b}")
print(f" Score {target}: {scores[target]} | "
f"Score A: {scores['A']} | Score C: {scores['C']}")
if ranking.index(target) == 0 and pivot_found is None:
pivot_found = step - 1 if step > 0 else None
if pivot_found is not None:
print(f"\n** BASCULEMENT : {target} passe du bas au sommet "
f"quand l'electeur {pivot_found} change **")
print(f"L'electeur {pivot_found} est le PIVOT pour cette execution.")
break
print()
# Passer l'electeur suivant
if step < n_voters_test:
others_copy = list(others)
random.shuffle(others_copy)
profile[step] = [target] + others_copy
# Statistiques sur plusieurs repetitions
random.seed(42)
pivot_counts = Counter()
n_trials = 100
for _ in range(n_trials):
p = find_pivot_sequence(borda_rule, n_voters_test, alternatives_3, target)
if p is not None:
pivot_counts[p] += 1
print(f"\nResume sur {n_trials} repetitions :")
most_common = pivot_counts.most_common(1)
if most_common:
pivot_id, count = most_common[0]
print(f" Pivot le plus frequent : electeur {pivot_id} "
f"({count} occurrences)")
print(f" Distribution des pivots : {dict(pivot_counts)}")EXISTENCE DU PIVOT : SIMULATION
================================
Alternatives : ['A', 'B', 'C'] | 5 electeurs
Cible : B
Sequence de profils (B passe du bas vers le haut):
-----------------------------------------------------------------
Etape 0: B est en bas pour tous
Electeur 0: C > A > B | Electeur 1: A > C > B | Electeur 2: A > C > B | Electeur 3: C > A > B
Electeur 3: C > A > B
Electeur 4: C > A > B
Etape 0: B est en bas pour tous
Electeur 0: C > A > B
Electeur 1: A > C > B
Electeur 2: A > C > B
Electeur 3: C > A > B
Electeur 4: C > A > B
Social (Borda): ['C', 'A', 'B'] -> B est DERNIER
Score B: 0 | Score A: 7 | Score C: 8
Etape 1: Electeur 0 passe B en haut
Electeur 0: B > A > C
Electeur 1: A > C > B
Electeur 2: A > C > B
Electeur 3: C > A > B
Electeur 4: C > A > B
Social (Borda): ['A', 'C', 'B'] -> B est DERNIER
Score B: 2 | Score A: 7 | Score C: 6
Etape 2: Electeur 1 passe B en haut
Electeur 0: B > A > C
Electeur 1: B > A > C
Electeur 2: A > C > B
Electeur 3: C > A > B
Electeur 4: C > A > B
Social (Borda): ['A', 'C', 'B'] -> B est DERNIER
Score B: 4 | Score A: 6 | Score C: 5
Etape 3: Electeur 2 passe B en haut
Electeur 0: B > A > C
Electeur 1: B > A > C
Electeur 2: B > A > C
Electeur 3: C > A > B
Electeur 4: C > A > B
Social (Borda): ['B', 'A', 'C'] -> B est PREMIER
Score B: 6 | Score A: 5 | Score C: 4
** BASCULEMENT : B passe du bas au sommet quand l'electeur 2 change **
L'electeur 2 est le PIVOT pour cette execution.
Resume sur 100 repetitions :
Pivot le plus frequent : electeur 2 (90 occurrences)
Distribution des pivots : {3: 10, 2: 90}Definition Lean (Arrow.lean, ligne 408) :
theorem pivot_is_dictator_except_b (f : SWF i sigma) (X : Finset sigma)
(hind : ind_of_irr_alts f X)
(b : sigma) (hb : b \in X)
(n : iota) (hn : is_pivotal f X n b)
(a c : sigma) (ha : a \in X) (hc : c \in X)
(hab : a ≠ b) (hcb : c ≠ b) (hac : a ≠ c) :
is_dictator_on f n c aEn francais : L’electeur pivotal pour b est un dictateur partiel : pour toute paire (a, c) qui ne contient PAS b, le pivot dicte le classement social. Si le pivot prefere c a a, la societe prefere c a a.
Preuve (idee) : On construit des profils auxiliaires ou b est utilise comme “leurre”. Par IIA, le classement entre a et c ne depend que des préférences individuelles sur (a, c). En manipulant la position de b, on utilise le fait que le pivot peut contrôler le classement de b pour deduire qu’il contrôle aussi (a, c).
# 2.3 Pivot = Dictateur partiel -- Simulation Python
def check_partial_dictator(voting_rule, n_voters, alternatives,
pivot_idx, target, pair_without_target,
n_tests=500):
"""Teste si le pivot dicte le classement pour une paire ne contenant
pas l'alternative cible.
Args:
voting_rule: regle de vote
n_voters: nombre de votants
alternatives: liste des alternatives
pivot_idx: index du pivot suppose
target: alternative cible (b dans la preuve)
pair_without_target: tuple (a, c) ne contenant pas target
n_tests: nombre de tests
Returns:
int: nombre de fois ou le pivot ne dicte PAS le classement
"""
a, c = pair_without_target
non_concordances = 0
for _ in range(n_tests):
profile = []
for _ in range(n_voters):
p = list(alternatives)
random.shuffle(p)
profile.append(p)
ranking = voting_rule(profile)
# Le pivot prefere a a c ?
pivot_prefers_a = profile[pivot_idx].index(a) < profile[pivot_idx].index(c)
# Le social prefere a a c ?
social_prefers_a = ranking.index(a) < ranking.index(c)
if pivot_prefers_a != social_prefers_a:
non_concordances += 1
return non_concordances
alternatives_3 = ['A', 'B', 'C']
n_voters_test = 5
target = 'B'
pair = ('A', 'C') # Paire ne contenant pas B
pivot_idx = 1 # Du test precedent
print("PIVOT = DICTATEUR PARTIEL : SIMULATION")
print("=" * 39)
print("Configuration : 3 alternatives {}, pivot = electeur {}".format(
alternatives_3, pivot_idx))
print()
print("Test : le pivot dicte-t-il le classement "
"pour les paires sans {} ?".format(target))
print("Paire testee : {} -- ne contient pas {}".format(pair, target))
# Test avec Borda
nc = check_partial_dictator(
borda_rule, n_voters_test, alternatives_3,
pivot_idx, target, pair
)
print()
print("Test sur 500 profils aleatoires :")
print(" Non-concordances : {}/500".format(nc))
if nc == 0:
print(" => Le pivot EST un dictateur partiel")
else:
print(" => Le pivot n'est PAS un dictateur partiel")
if nc > 0:
print()
print("Resultat : le pivot pour {} n'est PAS un dictateur "
"partiel sous Borda".format(target))
print("C'est normal : Borda viole IIA, donc la preuve d'Arrow")
print("ne s'applique pas a cette regle.")
# Demonstration avec une dictature
nc_dict = check_partial_dictator(
lambda p: dictatorial_rule(p, 0), n_voters_test, alternatives_3,
0, target, pair
)
print()
print("Demonstration avec une DICTATURE (pivot = electeur 0) :")
print(" Non-concordances : {}/500".format(nc_dict))
if nc_dict == 0:
print(" => Le pivot EST dictateur partiel "
"(comme attendu pour une dictature)")PIVOT = DICTATEUR PARTIEL : SIMULATION
=======================================
Configuration : 3 alternatives ['A', 'B', 'C'], pivot = electeur 1
Test : le pivot dicte-t-il le classement pour les paires sans B ?
Paire testee : ('A', 'C') -- ne contient pas B
Test sur 500 profils aleatoires :
Non-concordances : 189/500
=> Le pivot n'est PAS un dictateur partiel
Resultat : le pivot pour B n'est PAS un dictateur partiel sous Borda
C'est normal : Borda viole IIA, donc la preuve d'Arrow
ne s'applique pas a cette regle.
Demonstration avec une DICTATURE (pivot = electeur 0) :
Non-concordances : 0/500
=> Le pivot EST dictateur partiel (comme attendu pour une dictature)Le résultat est instructif :
| Règle | Satisfait IIA ? | Pivot = dictateur partiel ? |
|---|---|---|
| Borda | Non | Non (coherent) |
| Dictature | Oui | Oui (verification) |
Lien avec la preuve Lean : le theoreme
pivot_is_dictator_except_butilise explicitement l’hypothese IIA (hind : ind_of_irr_alts f X) dans sa preuve. Sans IIA, la conclusion ne tient pas.
Theoreme principal (Arrow.lean, ligne 679) :
theorem arrow (f : SWF i sigma) (X : Finset sigma)
(hwp : weak_pareto f X) (hind : ind_of_irr_alts f X)
(hX : 3 <= X.card) :
is_dictatorship f XCorollaire (forme negative, Arrow.lean, ligne 697) :
theorem no_perfect_swf (f : SWF i sigma) (X : Finset sigma)
(hwp : weak_pareto f X) (hind : ind_of_irr_alts f X)
(hX : 3 <= X.card) :
not (non_dictatorial f X)Structure de la preuve dans Arrow.lean :
theorem arrow ... := by
obtain ⟨b, hb⟩ := hne -- Choisir une alternative b
obtain ⟨n, hn⟩ := pivot_exists ... -- Trouver le pivot pour b
have h3 := pivot_is_dictator_except_b ... -- Pivot = dictateur sauf b
have h4 := partial_dictator_is_full_dictator ... -- Dictateur partiel = complet
exact ⟨n, h4⟩ -- Conclusion : il existe un dictateurEn francais : Toute fonction de bien-etre social (avec au moins 3 alternatives) qui satisfait Pareto faible et IIA est necessairement une dictature. Il n’existe aucune règle de vote parfaite.
La preuve complete se trouve dans game_theory_lean/SocialChoice/Arrow.lean.
Nous avons vu que nos tests Python confirment empiriquement les predictions du theoreme d’Arrow. Mais une question naturelle se pose : pourquoi avons-nous besoin d’une preuve formelle ?
| Aspect | Simulation Python | Preuve formelle Lean |
|---|---|---|
| Domaine | Un nombre fini de profils tests | Tous les profils possibles (infini) |
| Garantie | Statistique (probabiliste) | Mathematique (absolue) |
| Contre-exemple | Peut trouver une violation | Prouve qu’il n’y en a pas |
| Theoreme universel | Ne peut PAS le prouver | Le prouve rigoureusement |
Le theoreme d’Arrow dit : “Pour TOUTE SWF, Pour TOUT profil de préférences, si Pareto + IIA sont satisfaits, alors c’est une dictature.”
C’est un enonce universel (\(\forall\)). Aucun nombre fini de tests ne peut le prouver – il faudrait tester une infinite de SWF et une infinite de profils.
En revanche, un seul contre-exemple pourrait le refuter. Essayons !
# 3. Tentative de refutation d'Arrow par force brute
def exhaustive_check(rule_name, rule_func, alternatives, n_voters):
"""Verification exhaustive sur TOUS les profils possibles."""
all_perms = list(permutations(alternatives))
# Generer tous les profils possibles (produit cartesien)
from itertools import product
all_profiles = list(product(all_perms, repeat=n_voters))
all_profiles = [list(p) for p in all_profiles]
# 1. Verifier Pareto
pareto_violations = 0
for prof in all_profiles:
ranking = rule_func(list(prof))
for x, y in combinations(alternatives, 2):
all_prefer = all(
list(p).index(x) < list(p).index(y) for p in prof
)
if all_prefer and ranking.index(x) > ranking.index(y):
pareto_violations += 1
# 2. Verifier IIA
iia_violations = 0
for prof1 in all_profiles:
for prof2 in all_profiles:
for x, y in combinations(alternatives, 2):
same_xy = all(
(list(p1).index(x) < list(p1).index(y))
== (list(p2).index(x) < list(p2).index(y))
for p1, p2 in zip(prof1, prof2)
)
if same_xy:
r1 = rule_func(list(prof1))
r2 = rule_func(list(prof2))
if (r1.index(x) < r1.index(y)) != (r2.index(x) < r2.index(y)):
iia_violations += 1
# 3. Verifier non-dictature
dictator = check_non_dictatorship(
rule_func, n_voters, alternatives, n_tests=200
)
is_dict = dictator is not None
n_profiles = len(all_profiles)
print(f"{rule_name} :")
p_status = "OK" if pareto_violations == 0 else f"VIOLE ({pareto_violations})"
print(f" Pareto : {p_status} ({pareto_violations} violations sur {n_profiles} profils)")
n_pairs = n_profiles * n_profiles
iia_status = "OK" if iia_violations == 0 else f"VIOLE ({iia_violations})"
print(f" IIA : {iia_status} ({iia_violations} violations sur les paires de profils)")
dict_status = "VIOLE (c'est une dictature)" if is_dict else "OK"
print(f" Non-dictature : {dict_status}")
satisfies_all = (pareto_violations == 0
and iia_violations == 0
and not is_dict)
print(f" => {'Satisfait' if satisfies_all else 'Ne satisfait PAS'}"
f" les trois axiomes")
return satisfies_all
alternatives_3 = ['A', 'B', 'C']
n_voters_brute = 3 # 3 votants pour rester calculable
n_perms = len(list(permutations(alternatives_3)))
n_profiles = n_perms ** n_voters_brute
print("TENTATIVE DE REFUTATION D'ARROW (force brute)")
print("=" * 47)
print(f"Configuration : {n_voters_brute} votants, "
f"3 alternatives {alternatives_3}")
print(f"Nombre de preferences possibles : {n_perms} (3! permutations)")
print(f"Nombre de profils possibles : {n_profiles} ({n_perms}^{n_voters_brute})")
print(f"Nombre de SWF possibles : {n_perms}^{n_profiles}")
print(f" (impossible d'enumerer toutes les SWF)")
print("\nStrategie : tester les regles de vote usuelles")
print("et les comparer aux axiomes d'Arrow.")
print(f"\nVerification exhaustive sur TOUS les {n_profiles} profils :")
found_counterexample = False
for name, rule in [
("Borda", borda_rule),
("Pluralite", plurality_rule),
("Dictature (electeur 0)", lambda p: dictatorial_rule(p, 0)),
]:
satisfies = exhaustive_check(name, rule, alternatives_3, n_voters_brute)
if satisfies:
found_counterexample = True
print()
if not found_counterexample:
print("CONCLUSION : aucune regle usuelle ne satisfait les 3 axiomes")
print("Ce resultat est coherent avec le theoreme d'Arrow, mais ce test")
print(f"ne prouve le theoreme QUE pour ({n_voters_brute} votants, "
"3 alternatives).")
print("La preuve formelle en Lean couvre TOUS les cas "
"(inclus ceux non testes).")TENTATIVE DE REFUTATION D'ARROW (force brute)
===============================================
Configuration : 3 votants, 3 alternatives ['A', 'B', 'C']
Nombre de preferences possibles : 6 (3! permutations)
Nombre de profils possibles : 216 (6^3)
Nombre de SWF possibles : 6^216
(impossible d'enumerer toutes les SWF)
Strategie : tester les regles de vote usuelles
et les comparer aux axiomes d'Arrow.
Verification exhaustive sur TOUS les 216 profils :
Borda :
Pareto : OK (0 violations sur 216 profils)
IIA : VIOLE (1104) (1104 violations sur les paires de profils)
Non-dictature : OK
=> Ne satisfait PAS les trois axiomes
Pluralite :
Pareto : OK (0 violations sur 216 profils)
IIA : VIOLE (3312) (3312 violations sur les paires de profils)
Non-dictature : OK
=> Ne satisfait PAS les trois axiomes
Dictature (electeur 0) :
Pareto : OK (0 violations sur 216 profils)
IIA : OK (0 violations sur les paires de profils)
Non-dictature : VIOLE (c'est une dictature)
=> Ne satisfait PAS les trois axiomes
CONCLUSION : aucune regle usuelle ne satisfait les 3 axiomes
Ce resultat est coherent avec le theoreme d'Arrow, mais ce test
ne prouve le theoreme QUE pour (3 votants, 3 alternatives).
La preuve formelle en Lean couvre TOUS les cas (inclus ceux non testes).Nous allons maintenant comparer les résultats empiriques obtenus par simulation avec la garantie formelle de la preuve Lean, en analysant les limites de chaque approche.
Notre test exhaustif a couvert 216 profils (3 votants, 3 alternatives). Le theoreme d’Arrow s’applique a :
Pour \(n = 10\) votants et 4 alternatives, le nombre de profils possibles est déjà \(24^{10} \approx 6.3 \times 10^{13}\) – bien au-dela de ce qu’un ordinateur peut enumerer.
| Paramètres | Profils possibles | Faisable ? |
|---|---|---|
| 3 votants, 3 alts | 216 | Oui (quelques secondes) |
| 5 votants, 3 alts | 7 776 | Oui (quelques minutes) |
| 10 votants, 4 alts | \(6.3 \times 10^{13}\) | Non |
| \(n\) votants, \(m\) alts | \((m!)^n\) | Seulement pour petit \(n, m\) |
Conclusion : la simulation est utile pour intuiter le theoreme, mais seule la preuve formelle peut garantir qu’il n’existe aucune exception dans l’infinite des cas possibles.
La section précédente aboutit à un mur : il y a \(6^{216}\) SWF possibles, on ne peut pas les énumérer, et la force brute n’a testé que trois règles particulières. Un solveur SAT franchit exactement ce mur. Au lieu d’énumérer les fonctions, on encode la question d’existence — « existe-t-il une SWF quelconque (parmi les \(6^{216}\)) qui satisfait simultanément Pareto, IIA et non-dictature sur les 216 profils ? » — en clauses logiques, et on laisse un solveur CDCL industriel répondre. Un verdict UNSAT est une preuve de non-existence : aucune SWF ne réunit les trois axiomes.
Encodage — un littéral par décision sociale : \(v_{P,(x,y)}\) = « le résultat social du profil \(P\) classe \(x\) avant \(y\) » :
| Axiome | Clause (schéma) | Lecture |
|---|---|---|
| Totalité + asymétrie | \(v_{P,(x,y)} \lor v_{P,(y,x)}\), puis \(\neg v_{P,(x,y)} \lor \neg v_{P,(y,x)}\) | ordre strict total sur chaque profil |
| Transitivité | \(\neg v_{P,(x,y)} \lor \neg v_{P,(y,z)} \lor v_{P,(x,z)}\) | préférence sociale cohérente |
| Pareto | \(v_{P,(x,y)}\) si tous préfèrent \(x\) à \(y\) dans \(P\) | l’unanimité s’impose |
| IIA | \(v_{P_1,(x,y)} \leftrightarrow v_{P_2,(x,y)}\) si \(P_1, P_2\) accordés sur \((x,y)\) | indifférent aux alternatives non pertinentes |
| Non-dictature | négation de « le social suit toujours le votant \(i\) » (une clause par votant) | personne n’impose systématiquement son avis |
Même instance que la force brute (3 alternatives, 3 votants), mais la question n’est plus « cette règle vérifie-t-elle les axiomes ? » — c’est « une règle vérifiant les axiomes existe-t-elle ? ».
# Annexe SAT : encodage d'Arrow en CNF et resolution par pysat (axe lib-vs-lib)
from itertools import permutations, combinations, product
from time import perf_counter
from pysat.solvers import Glucose3, Minisat22, Cadical103
def arrow_cnf(alternatives, n_voters):
"""Encode 'existe-t-il une SWF quelconque Pareto + IIA + non-dictature ?' en CNF.
Litteral v[(P, (x, y))] = 'le resultat social classe x avant y sur le profil P'.
"""
orders = list(permutations(alternatives))
profiles = list(product(orders, repeat=n_voters))
pairs = [(x, y) for x in alternatives for y in alternatives if x != y]
lits = {}
for pi in range(len(profiles)):
for xy in pairs:
lits[(pi, xy)] = len(lits) + 1
cnf = []
familles = {"totalite + asymetrie": 0, "transitivite": 0,
"pareto": 0, "iia": 0, "non-dictature": 0}
for pi, prof in enumerate(profiles):
for x, y in combinations(alternatives, 2): # ordre total strict
cnf.append([lits[(pi, (x, y))], lits[(pi, (y, x))]])
cnf.append([-lits[(pi, (x, y))], -lits[(pi, (y, x))]])
familles["totalite + asymetrie"] += 2
for x, y, z in permutations(alternatives, 3): # transitivite
cnf.append([-lits[(pi, (x, y))], -lits[(pi, (y, z))],
lits[(pi, (x, z))]])
familles["transitivite"] += 1
for x, y in pairs: # pareto (tous preferent x a y)
if all(list(p).index(x) < list(p).index(y) for p in prof):
cnf.append([lits[(pi, (x, y))]])
familles["pareto"] += 1
for p1 in range(len(profiles)): # IIA
for p2 in range(p1 + 1, len(profiles)):
for x, y in pairs:
accord = all(
(list(a).index(x) < list(a).index(y))
== (list(b).index(x) < list(b).index(y))
for a, b in zip(profiles[p1], profiles[p2])
)
if accord:
cnf.append([-lits[(p1, (x, y))], lits[(p2, (x, y))]])
cnf.append([lits[(p1, (x, y))], -lits[(p2, (x, y))]])
familles["iia"] += 2
for i in range(n_voters): # non-dictature
cnf.append([-lits[(pi, (x, y))] for pi, prof in enumerate(profiles)
for x, y in pairs
if list(prof[i]).index(x) < list(prof[i]).index(y)])
familles["non-dictature"] += 1
return cnf, lits, profiles, familles
print("ANNEXE SAT : Arrow par solveur -- existence d'une SWF quelconque")
print("=" * 62)
cnf_arrow, lits_arrow, profiles_arrow, familles = arrow_cnf(
alternatives_3, n_voters_brute)
print(f"Instance : {len(profiles_arrow)} profils, {len(lits_arrow)} litteraux, "
f"{len(cnf_arrow)} clauses")
for nom, n in familles.items():
print(f" {nom:<20}: {n}")
print()
for nom, solveur in [("Glucose3", Glucose3), ("MiniSat22", Minisat22),
("CaDiCaL103", Cadical103)]:
t0 = perf_counter()
with solveur(bootstrap_with=cnf_arrow) as s:
est_sat = s.solve()
dt_ms = (perf_counter() - t0) * 1000.0
verdict = "SAT (contredit Arrow !)" if est_sat else "UNSAT (Arrow verifie)"
print(f" {nom:<11}: {verdict} [{dt_ms:7.1f} ms]")
# Frontiere : avec 2 alternatives, le meme encodage devient SAT (theoreme de May)
cnf_2alt, lits_2alt, profiles_2alt, _ = arrow_cnf(['A', 'B'], n_voters_brute)
with Glucose3(bootstrap_with=cnf_2alt) as s:
est_sat_2alt = s.solve()
modele = set(s.get_model())
print()
print(f"Frontiere |A| = 2 : {'SAT' if est_sat_2alt else 'UNSAT'} "
f"-- l'impossibilite ne nait qu'avec la 3e alternative")
if est_sat_2alt:
print("(avis des 3 votants) -> social (modele Glucose3)")
for pi, prof in enumerate(profiles_2alt):
avis = ["A>B" if list(p).index('A') < list(p).index('B') else "B>A"
for p in prof]
social = "A>B" if lits_2alt[(pi, ('A', 'B'))] in modele else "B>A"
print(f" {' '.join(avis):<11} -> {social}")
# La regle de majorite est-elle ELLE-MEME un modele de la CNF ?
def clause_satisfaite(cl, vrais):
return any((l > 0 and l in vrais) or (l < 0 and -l not in vrais)
for l in cl)
modele_maj = set()
for pi, prof in enumerate(profiles_2alt):
n_ab = sum(1 for p in prof if list(p).index('A') < list(p).index('B'))
xy = ('A', 'B') if n_ab >= 2 else ('B', 'A')
modele_maj.add(lits_2alt[(pi, xy)])
maj_valide = all(clause_satisfaite(cl, modele_maj) for cl in cnf_2alt)
print()
print(f"Verification directe : la majorite satisfait-elle toute la CNF ? "
f"{'OUI' if maj_valide else 'NON'}")
print()
print(">>> UNSAT pour |A| = 3 : aucune SWF ne satisfait les trois axiomes.")
print(">>> SAT pour |A| = 2 : des SWF valides existent -- la majorite en est une")
print(" (theoreme de May, 1952) ; le modele rendu par Glucose3 en est une autre")
print(" (biaisee vers A) : existence n'est pas unicite.")ANNEXE SAT : Arrow par solveur -- existence d'une SWF quelconque
==============================================================
Instance : 216 profils, 1296 litteraux, 36453 clauses
totalite + asymetrie: 1296
transitivite : 1296
pareto : 162
iia : 33696
non-dictature : 3
Glucose3 : UNSAT (Arrow verifie) [ 52.1 ms]
MiniSat22 : UNSAT (Arrow verifie) [ 17.5 ms]
CaDiCaL103 : UNSAT (Arrow verifie) [ 21.9 ms]
Frontiere |A| = 2 : SAT -- l'impossibilite ne nait qu'avec la 3e alternative
(avis des 3 votants) -> social (modele Glucose3)
A>B A>B A>B -> A>B
A>B A>B B>A -> A>B
A>B B>A A>B -> A>B
A>B B>A B>A -> A>B
B>A A>B A>B -> A>B
B>A A>B B>A -> A>B
B>A B>A A>B -> A>B
B>A B>A B>A -> B>A
Verification directe : la majorite satisfait-elle toute la CNF ? OUI
>>> UNSAT pour |A| = 3 : aucune SWF ne satisfait les trois axiomes.
>>> SAT pour |A| = 2 : des SWF valides existent -- la majorite en est une
(theoreme de May, 1952) ; le modele rendu par Glucose3 en est une autre
(biaisee vers A) : existence n'est pas unicite.Synthese visuelle des tests d’axiomes sur les différentes règles de vote.
# 4. Visualisation : Synthese des axiomes
fig, axes = plt.subplots(1, 3, figsize=(15, 5))
rules = ['Borda', 'Pluralite', 'Dictature']
axioms = ['Pareto', 'IIA', 'Non-dictature']
# Resultats tires des tests precedents
# 1 = satisfait (vert), 0 = viole (rouge)
results = {
'Borda': [1, 0, 1], # Pareto OK, IIA viole, Non-dict OK
'Pluralite': [1, 0, 1], # Pareto OK, IIA viole, Non-dict OK
'Dictature': [1, 1, 0], # Pareto OK, IIA OK, Non-dict viole
}
colors_map = {1: '#2ecc71', 0: '#e74c3c'}
for idx, (rule_name, ax) in enumerate(zip(rules, axes)):
values = results[rule_name]
bars = ax.bar(axioms, [1, 1, 1], color=[colors_map[v] for v in values],
edgecolor='black', linewidth=0.5)
for i, v in enumerate(values):
label = "SATISFAIT" if v == 1 else "VIOLE"
ax.text(i, 0.5, label, ha='center', va='center',
fontweight='bold', fontsize=9, color='white')
ax.set_ylim(0, 1.3)
ax.set_title(rule_name, fontsize=13, fontweight='bold')
ax.set_yticks([])
ax.tick_params(axis='x', labelsize=9)
# Titre global
fig.suptitle("Theoreme d'Arrow : aucun systeme ne satisfait les 3 axiomes",
fontsize=14, fontweight='bold', y=1.02)
plt.tight_layout()
plt.show()
print("Synthese visuelle generee.")
Synthese visuelle generee.| Étape de la preuve Lean | Theoreme Lean | Demonstration Python |
|---|---|---|
| Axiome Pareto | weak_pareto (Framework.lean:31) |
check_weak_pareto() sur 500 profils |
| Axiome IIA | ind_of_irr_alts (Framework.lean:36) |
check_iia() sur 1000 paires de profils |
| Non-dictature | non_dictatorial (Arrow.lean:693) |
check_non_dictatorship() sur 500 profils |
| Lemme Extremal | extremal_lemma (Arrow.lean:199) |
Profils avec B en position extreme |
| Existence du Pivot | pivot_exists (Arrow.lean:279) |
Sequence de basculement du bas vers le haut |
| Pivot = Dictateur partiel | pivot_is_dictator_except_b (Arrow.lean:408) |
Concordance pivot/social sur paires sans B |
| Theoreme final | arrow (Arrow.lean:679) |
Force brute exhaustive (216 profils) |
| Corollaire negatif | no_perfect_swf (Arrow.lean:697) |
Aucune règle ne satisfait les 3 axiomes |
game_theory_lean)Navigation : << SC-02 Lean SocialChoice | SC-03 Méthodes de vote >> | Index
Ce notebook a illustre la complementarite entre preuve formelle et simulation empirique. La preuve Lean garantit l’impossibilite pour tous les profils possibles, tandis que la simulation Python permet d’intuiter le résultat et de visualiser des contre-exemples concrets.
Objectif : Verifier que le lemme extremal s’applique aussi avec plus de 3 alternatives.
Ce que vous devez implementer : - Modifier la fonction generate_extremal_profiles pour 4 alternatives - Tester que l’alternative cible reste en position extreme dans le classement social - Comparer les résultats avec 3 et 4 alternatives
# Exercice 1 : Lemme Extremal avec 4 alternatives
# ================================================
# Exercice: adaptez generate_extremal_profiles pour 4 alternatives
# Indice : avec ['A', 'B', 'C', 'D'], la cible 'B' peut etre en premiere
# ou derniere position. Les 3 autres alternatives sont melangees entre elles.
alternatives_4 = ['A', 'B', 'C', 'D']
# Exercice: generez 100 profils ou B est toujours en position extreme
# et comptez combien de fois B reste en position extreme dans le classement Borda.
# Indice : utilisez une boucle similaire au test systematique de la section 2.1
# mais avec alternatives_4 au lieu de alternatives_3.
# Exercice: comparez les resultats avec 3 et 4 alternatives.
# Le lemme extremal s'applique-t-il aussi bien avec 4 alternatives ?
print("Exercice 1 : Lemme Extremal avec 4 alternatives")Exercice 1 : Lemme Extremal avec 4 alternativesObjectif : Trouver explicitement (pas par tirage aleatoire) deux profils qui montrent une violation de IIA par la méthode de Borda.
Ce que vous devez implementer : - Deux profils ou les préférences entre A et B sont identiques pour chaque electeur - Mais le classement social de A vs B change - Expliquer pourquoi cela viole IIA
# Exercice 2 : Contre-exemple IIA explicite pour Borda
# =====================================================
# Exercice: construisez deux profils avec 3 electeurs et 3 alternatives
# ou les preferences relatives entre A et C sont identiques pour chaque electeur,
# mais le classement social de A vs C change.
# Indice : la cle d IIA est que seuls les classements relatifs entre A et C
# devraient compter ; toute autre alternative (ici B) ne devrait pas influencer.
# Changez uniquement la position de B (l alternative "non pertinente") dans
# les preferences d un electeur pour faire basculer le verdict Borda.
# profil_1 = [
# # TODO etudiant : 3 listes [pref1, pref2, pref3] pour 3 electeurs
# ]
# profil_2 = [
# # TODO etudiant : meme contraintes mais position de B differente
# ]
# Exercice: verifiez que dans chaque profil, chaque electeur a la
# meme preference relative entre A et C.
# Exercice: appliquez borda_rule() aux deux profils et comparez
# la position relative de A et C.
# Exercice: expliquez pourquoi cela constitue une violation de IIA.
print("Exercice 2 : Contre-exemple IIA pour Borda")Exercice 2 : Contre-exemple IIA pour BordaObjectif : Calculer le nombre de profils possibles pour différentes configurations et comprendre pourquoi la force brute ne suffit pas.
Ce que vous devez implementer : - Une fonction qui calcule le nombre de profils possibles - Un tableau comparatif pour différentes tailles - Estimer le temps necessaire pour une enumeration exhaustive
# Exercice 3 : Complexite de la force brute
# ==========================================
def count_profiles(n_voters, n_alternatives):
"""Calcule le nombre de profils possibles.
Args:
n_voters: nombre de votants
n_alternatives: nombre d'alternatives
Returns:
int: nombre de profils possibles
"""
# TODO etudiant : implementez la formule.
# Indice : pour chaque votant, il y a (n_alternatives!) classements possibles.
# Pour n_voters independants, on multiplie les possibilites.
# Importez factorial depuis math.
return None # remplacez par le calcul correct
print("Exercice 3 : Complexite de la force brute")
# Configurations a tester
configs = [
(3, 3),
(5, 3),
(10, 4),
]
# Exercice: ajoutez d'autres configurations
# (par exemple, 20 votants, 5 alternatives)
# TODO etudiant : une fois count_profiles implemente, decommentez le bloc ci-dessous
# pour visualiser le temps estime de force brute :
#
# for n_v, n_a in configs:
# n_prof = count_profiles(n_v, n_a)
# print(f"Nombre de profils possibles pour ({n_v} votants, {n_a} alternatives) : {n_prof}")
# seconds = n_prof / 1_000_000
# if seconds > 3600:
# print(f"A 1 million de profils/seconde : {seconds / (3600 * 24 * 365):.1f} annees")
# elif seconds > 60:
# print(f"A 1 million de profils/seconde : {seconds / 60:.1f} minutes")
# else:
# print(f"A 1 million de profils/seconde : {seconds:.1f} secondes")
# Exercice: calculez le nombre de SWF possibles
# (chaque SWF est une fonction de l'ensemble des profils vers l'ensemble
# des classements). Combien y a-t-il de SWF pour (3, 3) ?
# Indice : c'est (n_alternatives!) ^ (nombre de profils)Exercice 3 : Complexite de la force bruteConstruire un profil de préférences qui viole le critere de Condorcet avec la règle de Borda.
Indice : 3 votants, 3 alternatives, verifiez le gagnant de Condorcet vs Borda.
# Exercice 4 : Profil de preferences paradoxaux
# TODO etudiant : Construire un profil de preferences qui viole le critere de Condorcet avec la regle de Borda
# Indice : 3 votants, 3 alternatives, verifiez le gagnant de Condorcet vs Borda
result = None # TODO etudiant : remplacer par votre implementation
print("Exercice a completer : Profil de preferences paradoxaux")Exercice a completer : Profil de preferences paradoxauxCe notebook a illustre le theoreme d’impossibilite d’Arrow par la simulation empirique, en parallele de la preuve formelle en Lean.
| Règle | Pareto faible | IIA | Non-dictature | Les 3 satisfaits ? |
|---|---|---|---|---|
| Borda | 0 violations | 1104 violations | OK | NON (IIA) |
| Pluralite | 0 violations | 3312 violations | OK | NON (IIA) |
| Dictature | 0 violations | 0 violations | Electeur 0 = dictateur | NON (non-dictature) |
Aucune règle de vote ne peut simultanement satisfaire les trois axiomes d’Arrow : Pareto faible, Indépendance des Alternatives Irrelevantes (IIA), et Non-dictature. La preuve formelle Lean garantit ce résultat pour un nombre quelconque de votants et d’alternatives.
L’IIA est l’axiome le plus difficile a satisfaire : Borda et Pluralite accumulent respectivement 1104 et 3312 violations sur seulement 216 profils. La force brute confirme l’impossibilite sur les petites instances, mais explose en complexite (10 votants, 4 alternatives = 6.3x10^13 profils).
Retour au sommaire : Social Choice | GameTheory