Arrow's theorem

Stream: new members

[Andrew Souther]

I have been tinkering with Arrow's Impossibility Theorem from social choice theory, which apparently has been formalized before in other systems. If you aren't familiar with Arrow's theorem, I am working on the first proof from this paper. I have a design question, but I am pretty far down a rabbit hole, so I think I'll have to provide some context.....

I am treating "individuals" as type ι and "social states" as type σ. A society is a finset of individuals. A preference, σ → σ → Prop, is a relation between two social states. An individual preference is a mapping from each individual to a preference, and I treat it as type ι → σ → σ → Prop. A social welfare function is a mapping from every possible set of individual preferences to a single "social" preference. I treat social welfare functions as type (ι → σ → σ → Prop) → (σ → σ → Prop).

Arrow's theorem is a fact about the properties that social welfare functions can have. However, I've realized that the theorem quietly relies on a certain fact about individual preferences. I'll try to articulate it like this: for every possible arrangement of social states by every individual in society, an individual preference exists such that everyone in society arranges them in those ways. In Lean, I've tried expressing this using vectors. It got pretty convoluted....

def unrestricted_domain (f : (ι → σ → σ → Prop) → (σ → σ → Prop)) : Prop :=
    (∀ (m : ℕ) (n : fin (m+1) ) (V : vector (finset ι) n) (T : vector (vector σ m) n),
    ∃Rᵢ  : ι → (σ → σ → Prop), ∀ (i : ι) (j : fin n) (k k': fin m), i ∈ nth V j → k > k' →
        P (Rᵢ i) (nth (nth T j) k) (nth (nth T j) k') )

(I realize that the definition doesn't even use f... Most textbooks state this assumption as a fact about the domain of social social welfare functions, so I originally tried defining it that way. I couldn't really make that interpretation work though ).

I recently finished the first step (out of 4) in that proof of Arrow's theorem using this definition. But I'm sure there has to be a better way to do this... Does anyone have advice for expressing this assumption more succintly? The second step is more complicated, and I'm getting frustrated with all these vectors and fins floating around :anguished:

If it would help to see how I use this definition in context, my proof of that first step is at the bottom of this file.

[Yakov Pechersky]

Could you express it about finsets instead?

[Yakov Pechersky]

Since you don't care about the order

[Yakov Pechersky]

I guess finsets of products of finsets

[Yakov Pechersky]

What's P?

[Andrew Souther]

P is how I define the 'strict' version of a given preference relation. That is, P R x y iff (R x y) ∧ ¬ (R y x).

[Andrew Souther]

I don't understand what you mean about using finsets, but it could be possible. I started working with vectors because at least the order of social states does matter.

For example, in that proof, I have three social states A, B , and C. For a given society, I'm trying to show there exists an individual preference such that some subset of people strictly prefer B over A and C, while other people strictly prefer A and C over B.

In this sense, I think of order as important for the whole definition, but curious to hear how you see finsets fitting in.

[Yakov Pechersky]

How about something like:

import data.sym2

variables {ι σ : Type*} [decidable_eq ι] [decidable_eq σ] [fintype ι] [fintype σ]

def P (R : σ → σ → Prop) (x y : σ) : Prop := R x y ∧ ¬ R y x

def unrestricted_domain (f : (ι → σ → σ → Prop) → (σ → σ → Prop)) : Prop :=
  ∀ (society : finset ι),
  ∀ (arrangement : ι → finset (sym2 σ)),
  ∃ Rᵢ : ι → (σ → σ → Prop),
  ∀ individual ∈ society,
  ∀ pair ∈ arrangement individual,
  ∀ (state₁ : σ) (hs : state₁ ∈ pair),
  P (Rᵢ individual) state₁ (sym2.mem.other' hs)

[Yakov Pechersky]

My brief familiarity with Arrow's theorem is that I know graph theory people are into it. And sym2 was constructed to represent edges in undirected graphs.

[Yakov Pechersky]

There's probably some formulation of your statement that talks about graphs instead

[Yakov Pechersky]

sym2.mem.other' is the way to get the second state2

[Yakov Pechersky]

Ah, I guess I didn't include here the constraint that the two things being compared are different.

[Yakov Pechersky]

You can add that inequality constraint to P I guess

[Yakov Pechersky]

Like this?

def P (R : σ → σ → Prop) (x y : σ) : Prop := x ≠ y ∧ anti_symmetric R

[Andrew Souther]

Graph theory could be a cool route to take this, thanks Yakov. Are you sure about using undirected graphs though?

For example, consider a pair of social states A and B. If I understand the last two lines of your definition, each element in each pair is strictly preferred to the "other" element. But that would mean A is strictly preferred to B while B is also strictly preferred to A. That should lead to a contradiction.

[Yakov Pechersky]

You're right, I misunderstood the problem statement. Then, you can use σ × σ instead of sym2 σ. I was just trying to understand your antidiagonal constraint of k < k'.

[Yakov Pechersky]

def unrestricted_domain (f : (ι → σ → σ → Prop) → (σ → σ → Prop)) : Prop :=
  ∀ (society : finset ι),
  ∀ (arrangement : ι → finset (σ × σ)),
  ∃ Rᵢ : ι → (σ → σ → Prop),
  ∀ individual ∈ society,
  ∀ pair ∈ arrangement individual,
  P (Rᵢ individual) (prod.fst pair) pair.snd

but I'm still not sure if that's exactly right.

[Aaron Anderson]

Andrew Souther said:

I have been tinkering with Arrow's Impossibility Theorem from social choice theory, which apparently has been formalized before in other systems. If you aren't familiar with Arrow's theorem, I am working on the first proof from this paper. I have a design question, but I am pretty far down a rabbit hole, so I think I'll have to provide some context.....

I am treating "individuals" as type ι and "social states" as type σ. A society is a finset of individuals. A preference, σ → σ → Prop, is a relation between two social states. An individual preference is a mapping from each individual to a preference, and I treat it as type ι → σ → σ → Prop. A social welfare function is a mapping from every possible set of individual preferences to a single "social" preference. I treat social welfare functions as type (ι → σ → σ → Prop) → (σ → σ → Prop).

Arrow's theorem is a fact about the properties that social welfare functions can have. However, I've realized that the theorem quietly relies on a certain fact about individual preferences. I'll try to articulate it like this: for every possible arrangement of social states by every individual in society, an individual preference exists such that everyone in society arranges them in those ways. In Lean, I've tried expressing this using vectors. It got pretty convoluted....

def unrestricted_domain (f : (ι → σ → σ → Prop) → (σ → σ → Prop)) : Prop :=
    (∀ (m : ℕ) (n : fin (m+1) ) (V : vector (finset ι) n) (T : vector (vector σ m) n),
    ∃Rᵢ  : ι → (σ → σ → Prop), ∀ (i : ι) (j : fin n) (k k': fin m), i ∈ nth V j → k > k' →
        P (Rᵢ i) (nth (nth T j) k) (nth (nth T j) k') )

(I realize that the definition doesn't even use f... Most textbooks state this assumption as a fact about the domain of social social welfare functions, so I originally tried defining it that way. I couldn't really make that interpretation work though ).

I recently finished the first step (out of 4) in that proof of Arrow's theorem using this definition. But I'm sure there has to be a better way to do this... Does anyone have advice for expressing this assumption more succintly? The second step is more complicated, and I'm getting frustrated with all these vectors and fins floating around :anguished:

If it would help to see how I use this definition in context, my proof of that first step is at the bottom of this file.

I've usually seen Arrow's Theorem connected to ultrafilters, which we do have in mathlib: docs#ultrafilter

[Andrew Souther]

I think I've also realized there's a problem in the original definition I proposed...
Somehow, I'd like to make sure each individual's preference ordering respects transitivity. No individual can strictly prefer A to B, B to C, and C to A. I'm not 100% sure this assumption is necessary, but I think it is important.

Is there a way to include this requirement in the definition too?

[Andrew Souther]

And thanks @Aaron Anderson , I've never heard of ultrafilters, but I'll look into that.