Computer Aided Proof of Arrow’s Impossibility Theorem

Economic Theory
Author

Avinash Mani Tripathi

Published

April 24, 2026

This notebook reconstructs a small-scale, computer-aided search proof of Arrow’s impossibility theorem. The way this note was written is an interesting story. There is a theorem that says Arrow’s impossibility theorem holds for arbitrary number of (finite) individuals and alternatives if and only if it holds for a community of two individuals and three alternatives. This result essentially reduces Arrow’s impossibility theorem–and similar other impossibility theorems in social choice– to a finite search problem, something that can be checked by computer in finite time.

When I told this result to my senior colleague Arjun Jayadev, he asked me write a program to show Arrow’s Impossibilty Theorem. Even with 2 individuals and 3 alternatives, proving this result requires searching 6^36 possibilities. Consequently, brute force search does not work. In order to narrow down possibilities in each step, one has to use search with contstraint propogation. A python implementation of this approach–is given below.

The key reduction is standard: if Arrow’s theorem holds for a society with two individuals and three alternatives, then the general impossibility follows as well. That makes the problem finite and concrete enough to explore with code.

We work with:

A social welfare function (SWF) assigns one social ranking to each preference profile. The goal is to check whether any such function can satisfy:

The notebook shows that no non-dictatorial SWF survives these constraints.

from itertools import permutations, product

import pandas as pd

1. Enumerating rankings and preference profiles

With three alternatives, each voter has 3! = 6 strict rankings. A preference profile is an ordered pair of individual rankings, one for each voter, so there are 6 x 6 = 36 possible profiles.

ALTERNATIVES = ("a", "b", "c")

RANKINGS = ["".join(order) for order in permutations(ALTERNATIVES)]
PREFERENCE_PROFILES = [
    f"{ranking_a}&{ranking_b}"
    for ranking_a, ranking_b in product(RANKINGS, repeat=2)
]

# Initially, each preference profile may map to any of the six social rankings.
INITIAL_SWF_DOMAINS = {
    profile: RANKINGS.copy()
    for profile in PREFERENCE_PROFILES
}

print("Rankings:", RANKINGS)
print("Number of preference profiles:", len(PREFERENCE_PROFILES))
print("Number of unconstrained SWFs:", 6 ** 36)
Rankings: ['abc', 'acb', 'bac', 'bca', 'cab', 'cba']
Number of preference profiles: 36
Number of unconstrained SWFs: 10314424798490535546171949056

Even in this tiny setting, brute force is hopeless: there are 6^36 possible complete SWFs. Instead, we combine search with constraint propagation.

2. Basic preference comparison helpers

The next helper answers a simple question: given a ranking such as "abc", does it place one alternative above another?

def prefers(higher: str, lower: str, ranking: str) -> bool:
    """Return True when `ranking` places `higher` above `lower`."""
    positions = {alternative: index for index, alternative in enumerate(ranking)}
    return positions[higher] < positions[lower]


def split_profile(profile: str) -> tuple[str, str]:
    """Split a profile like 'abc&acb' into voter A and voter B rankings."""
    return tuple(profile.split("&"))


prefers("a", "b", "abc")
True

3. Unanimity as a local constraint

Unanimity says that whenever both voters rank one alternative above another, the social ranking must do the same.

This is a local condition: for a fixed preference profile and a candidate social ranking, we can test it independently of every other profile. That makes it a useful first pruning step.

def respects_unanimity(
    ranking_a: str,
    ranking_b: str,
    social_ranking: str,
) -> bool:
    """Check whether a candidate social ranking respects unanimity."""
    for left, right in permutations(ALTERNATIVES, 2):
        both_voters_prefer_left = (
            prefers(left, right, ranking_a)
            and prefers(left, right, ranking_b)
        )
        if both_voters_prefer_left and not prefers(left, right, social_ranking):
            return False
    return True


def filter_domains_by_unanimity(
    swf_domains: dict[str, list[str]],
) -> dict[str, list[str]]:
    """Remove social rankings that violate unanimity for each profile."""
    filtered_domains = {}

    for profile, candidate_rankings in swf_domains.items():
        ranking_a, ranking_b = split_profile(profile)
        filtered_domains[profile] = [
            social_ranking
            for social_ranking in candidate_rankings
            if respects_unanimity(ranking_a, ranking_b, social_ranking)
        ]

    return filtered_domains
unanimous_domains = filter_domains_by_unanimity(INITIAL_SWF_DOMAINS)

domain_sizes = pd.Series(len(rankings) for rankings in unanimous_domains.values())
domain_sizes.value_counts().sort_index()
1     6
2    12
3    12
6     6
Name: count, dtype: int64

After unanimity, the search space is already much smaller. Some profiles are fully determined, others still admit several social rankings.

The remaining number of candidate SWFs is:

remaining_candidate_swfs = 1

for domain in unanimous_domains.values():
    remaining_candidate_swfs *= len(domain)

remaining_candidate_swfs
101559956668416

4. IIA as a global consistency condition

Independence of irrelevant alternatives is global rather than local. It links the social comparison of any pair of alternatives across different preference profiles.

If two profiles agree on how each voter compares x and y, then the social ranking must also compare x and y in the same way in both profiles.

This allows each assignment to propagate constraints to many other profiles.

def respects_iia_between_profiles(
    ranking_a_1: str,
    ranking_b_1: str,
    social_ranking_1: str,
    ranking_a_2: str,
    ranking_b_2: str,
    social_ranking_2: str,
) -> bool:
    """Check whether two profile assignments are jointly consistent with IIA."""
    for left, right in permutations(ALTERNATIVES, 2):
        voter_a_changes = prefers(left, right, ranking_a_1) != prefers(left, right, ranking_a_2)
        voter_b_changes = prefers(left, right, ranking_b_1) != prefers(left, right, ranking_b_2)

        # If neither voter changes their comparison of (left, right),
        # the social comparison must stay fixed as well.
        if not voter_a_changes and not voter_b_changes:
            if prefers(left, right, social_ranking_1) != prefers(left, right, social_ranking_2):
                return False

    return True


def assign_and_propagate(
    profile: str,
    chosen_social_ranking: str,
    swf_domains: dict[str, list[str]],
) -> dict[str, list[str]] | bool:
    """Assign one social ranking to a profile and propagate IIA constraints.

    Returns False if propagation empties any domain.
    """
    updated_domains = {
        other_profile: candidate_rankings.copy()
        for other_profile, candidate_rankings in swf_domains.items()
    }
    updated_domains[profile] = [chosen_social_ranking]

    assigned_ranking_a, assigned_ranking_b = split_profile(profile)

    for other_profile, candidate_rankings in updated_domains.items():
        other_ranking_a, other_ranking_b = split_profile(other_profile)
        updated_domains[other_profile] = [
            social_ranking
            for social_ranking in candidate_rankings
            if respects_iia_between_profiles(
                assigned_ranking_a,
                assigned_ranking_b,
                chosen_social_ranking,
                other_ranking_a,
                other_ranking_b,
                social_ranking,
            )
        ]

        if not updated_domains[other_profile]:
            return False

    return updated_domains

5. Searching for a non-dictatorial SWF

The search uses a standard constraint-satisfaction strategy:

  • always branch on the most constrained profile first
  • assign one candidate social ranking
  • immediately propagate IIA
  • backtrack as soon as a contradiction appears

To make the result more informative, the search prints dictatorial solutions when it encounters them and keeps going. The theorem is established when no non-dictatorial solution remains.

def is_dictatorship(complete_swf: dict[str, str]) -> bool:
    """Return True when voter A or voter B always determines the social ranking."""
    voter_a_is_dictator = all(
        split_profile(profile)[0] == social_ranking
        for profile, social_ranking in complete_swf.items()
    )
    voter_b_is_dictator = all(
        split_profile(profile)[1] == social_ranking
        for profile, social_ranking in complete_swf.items()
    )
    return voter_a_is_dictator or voter_b_is_dictator


def search_for_non_dictatorial_swf(
    swf_domains: dict[str, list[str]],
) -> dict[str, str] | bool:
    """Search for a complete SWF satisfying unanimity and IIA, but not dictatorship."""
    if swf_domains is False:
        return False

    if all(len(candidate_rankings) == 1 for candidate_rankings in swf_domains.values()):
        complete_swf = {
            profile: candidate_rankings[0]
            for profile, candidate_rankings in swf_domains.items()
        }
        if is_dictatorship(complete_swf):
            print("=" * 20)
            print("Dictatorial solution found:")
            print(complete_swf)
            return False
        return complete_swf

    _, next_profile = min(
        (len(candidate_rankings), profile)
        for profile, candidate_rankings in swf_domains.items()
        if len(candidate_rankings) > 1
    )

    for candidate_social_ranking in swf_domains[next_profile]:
        propagated_domains = assign_and_propagate(
            next_profile,
            candidate_social_ranking,
            swf_domains,
        )
        result = search_for_non_dictatorial_swf(propagated_domains)
        if result:
            return result

    return False

Conclusion

The computation is deliberately small, but it captures the logic of Arrow’s theorem.

Once we require unanimity and IIA, the only surviving complete social welfare functions are dictatorial. Therefore, no social welfare function on this domain can satisfy unanimity, IIA, and non-dictatorship simultaneously.

That is precisely the impossibility result.