Arrow's theorem (1951) says that with three or more candidates, no way of turning a set of individual rankings into one group ranking can satisfy four conditions at once. I wrote a scroll-through explainer in seven chapters with a sandbox at the end where you set three voters' rankings over three candidates, pick a method, and watch the checker find a counterexample.
The four conditions
A social welfare function takes a profile, one ranking per voter, and returns a single ranking. Arrow asks for unrestricted domain (it accepts every profile), Pareto (if everyone ranks \(A\) above \(B\), so does the group), independence of irrelevant alternatives (the group's \(A\) versus \(B\) depends only on how each voter ranks \(A\) versus \(B\)), and non-dictatorship (no voter's ranking is always the group's). The theorem says no function on three or more candidates has all four.
The methods
Plurality counts first-place votes. It fails IIA in the familiar way: add a candidate similar to the leader and the leader's first places split.
Borda gives a candidate in position \(i\) (from 0) of a ballot \(m - 1 - i\) points and sums. Moving a third candidate around on some ballots changes the gap between the other two, so it fails IIA.
Instant runoff drops the candidate with the fewest first-place votes and moves those ballots to their next choice until someone has a majority. It fails IIA too, and it also fails monotonicity: ranking a candidate higher can make them lose, by changing who gets eliminated first. My checker also flags IRV for Pareto, which is a tie-break bug in my code. IRV itself satisfies Pareto.
The method I labeled Condorcet is Copeland. It builds the pairwise matrix, counts how many head-to-head matchups each candidate wins, and sorts by that count with an alphabetical tie-break. A Condorcet winner, someone who wins every matchup, comes out on top when one exists. When there's a cycle (\(A\) beats \(B\), \(B\) beats \(C\), \(C\) beats \(A\)), everyone has one win and the tie-break decides. So it always returns a total order, satisfies Pareto and unrestricted domain, and fails IIA. In Arrow's framing a cycle is a failure of transitivity in the group ranking, and Copeland never produces one, at the cost of an arbitrary answer.
The library also has an approval method that approves the top \(\lceil m/2 \rceil\) of each ranking, and the last chapter says approval and score voting fall outside Arrow's scope. That's true of approval as people use it, where each voter hands in a set rather than a ranking. My version maps a ranking to its top half, which makes it a positional rule and puts it squarely inside the theorem. It's in the methods table and not in the sandbox.
Checking by enumeration
With three candidates each voter has \(3! = 6\) rankings, and three voters give \(6^3 = 216\) profiles. That's small enough to check every one, and for three candidates the checkers do. The IIA checker takes every pair of profiles in which all three voters agree on \(A\) versus \(B\), runs the method on both, and reports the first pair where the group disagrees. The unrestricted domain checker just confirms every profile produces a complete ranking, and the dictatorship checker looks for a voter whose ranking matches the output on every profile.
For four candidates the space is \(4!^3 = 13{,}824\) profiles and for five it's \(5!^3 = 1{,}728{,}000\), so the checkers sample instead, 200 random profiles for most criteria and 300 for IIA. A pass at four or more candidates only means no counterexample turned up in the sample, and the sample changes each run.
The proof chapter
The proof walkthrough follows the pivotal-voter argument from Geanakoplos (Economic Theory 26(1): 211-215, 2005) in four steps. Suppose a method has all four properties. Put candidate \(B\) last on every ballot, so by Pareto the group puts \(B\) last too. Move \(B\) from last to first on one ballot at a time. At some ballot \(B\) jumps from the bottom of the group ranking to the top. That voter is pivotal. Using IIA and Pareto, that voter's ranking of any two other candidates decides the group ranking of those two, so the pivotal voter is a dictator. The diagrams use five voters, with voter 3 as the pivot, because the jump is easier to see with more than one voter on each side.
The sandbox presets are unanimous, the classic cycle, its reverse, a split top, a middle squeeze where \(B\) is everyone's second choice and nobody's first, and a polarized one. Drag the rankings from there. When IIA fails the checker prints both profiles and both group rankings.