Zulip Chat Archive

Stream: new members

Topic: Arrow's theorem


view this post on Zulip Andrew Souther (Jan 06 2021 at 06:07):

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.

view this post on Zulip Yakov Pechersky (Jan 06 2021 at 06:13):

Could you express it about finsets instead?

view this post on Zulip Yakov Pechersky (Jan 06 2021 at 06:13):

Since you don't care about the order

view this post on Zulip Yakov Pechersky (Jan 06 2021 at 06:14):

I guess finsets of products of finsets

view this post on Zulip Yakov Pechersky (Jan 06 2021 at 06:15):

What's P?

view this post on Zulip Andrew Souther (Jan 06 2021 at 06:20):

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).

view this post on Zulip Andrew Souther (Jan 06 2021 at 06:33):

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.

view this post on Zulip Yakov Pechersky (Jan 06 2021 at 06:53):

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)

view this post on Zulip Yakov Pechersky (Jan 06 2021 at 06:53):

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.

view this post on Zulip Yakov Pechersky (Jan 06 2021 at 06:53):

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

view this post on Zulip Yakov Pechersky (Jan 06 2021 at 06:54):

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

view this post on Zulip Yakov Pechersky (Jan 06 2021 at 06:55):

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

view this post on Zulip Yakov Pechersky (Jan 06 2021 at 06:55):

You can add that inequality constraint to P I guess

view this post on Zulip Yakov Pechersky (Jan 06 2021 at 06:58):

Like this?

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

view this post on Zulip Andrew Souther (Jan 06 2021 at 18:15):

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.

view this post on Zulip Yakov Pechersky (Jan 06 2021 at 18:17):

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'.

view this post on Zulip Yakov Pechersky (Jan 06 2021 at 18:21):

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.

view this post on Zulip Aaron Anderson (Jan 06 2021 at 18:21):

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

view this post on Zulip Andrew Souther (Jan 06 2021 at 18:23):

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?

view this post on Zulip Andrew Souther (Jan 06 2021 at 18:24):

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


Last updated: May 08 2021 at 10:12 UTC