Keyword: social-choice

Theorem Arrow's Impossibility Theorem staged

Theorem Arrow's Theorem via Decisive Coalitions staged

Definition Borda Score and Borda Rule formalized

Theorem Coalition Contraction — Splitting a Decisive Coalition staged

Theorem Condorcet Paradox staged

Definition Condorcet Winner formalized

Definition Decisive Coalition and Dictator formalized

Definition Decisive Coalition for an Ordered Pair formalized

Definition Dictatorial Social Choice Function formalized

Definition Dictatorial Social Welfare Function formalized

Theorem Field Expansion — Decisive on One Pair Implies Decisive Everywhere staged

Theorem Gibbard–Satterthwaite Theorem staged

Theorem Grand Coalition Is Decisive under Unanimity staged

Lemma IIA on Strict Preference staged

Definition Independence of Irrelevant Alternatives formalized

Theorem Minimal Decisive Coalition Has Size One staged

Definition Monotonic Social Choice Function formalized

Theorem Muller–Satterthwaite Theorem staged

Definition Pairwise Majority Comparison formalized

Definition Plurality Score and Plurality Rule formalized

Definition Preference Profile formalized

Definition Preference Relation formalized

Definition Social Choice Function formalized

Definition Social Choice Instance formalized

Definition Social Welfare Function formalized

Definition Solution Concept, Rule, and Correspondence formalized

Definition Strategy-Proof Social Choice Function formalized

Theorem Strategy-Proof ⇒ Monotonic staged

Definition Strict Preference formalized

Definition Unanimity (Pareto Axiom) formalized

Definition Weakly Decisive Coalition formalized