ファイル置き場 Sendai Logic Homepage

(1)

.

... .

. .

社会選択理論の逆数学

平田優志

東北大学大学院理学研究科数学専攻山崎武研究室

2012年10月26日

(2)

発表の流れ

. .¹. ^導入

逆数学について有限版Arrowの定理無限版^Arrowの定理

. .². ^{社会選択理論の逆数学} Social Welfare Function

ultrafilter_とSocial Welfare Function

3. _参考文献

(3)

逆数学について

逆数学とは「数学の諸定理の証明を行うために必要十分な公理とは何か」を調べる研究のことである.特に定理から公理を証明するというところから「逆」数学といわれている^.

逆数学は主に二階算術と言われる自然数と自然数の集合を扱える程度の弱い形式体系の中で行われてきた.その中で今回扱う予定の公理系は以下の3つである.

.

Definition

. .

... .

.

RCA₀,WKL₀,ACA₀はそれぞれ以下の公理からなる公理系である^. RCA0: BA(Basic Axioms) +Σ⁰₁-induction +∆⁰₁-comprehension WKL₀: RCA₀+ Weak K ¨onig’s Lemma

ACA0: RCA0+ arithmetical comprehension

(4)

有限版 Arrow の定理について

.

Theorem (Arrow の定理 )

. .

... .

.

選択肢が³つ以上あるとき^,社会選好を決定する際にみたしていると望ましいとされる条件⁽全会一致性^,無関係な選択対象からの独立性^,非独裁性⁾をすべて満たす SWF(_{社会厚生関数},Social Welfare Function)を見つけることはできない^.

これから「SWF(社会厚生関数)」や「社会選好を決定する際にみたしていると望ましいとされる条件」について,必要な記号などの準備をしながら説明をしていく.

(5)

用語・記号の準備

.

Definition ( 選択肢 , 投票者の集合 )

. .

... .

.

A = {a1,a2, · · · ,ak}:選択肢(alternative)の集合. N= {1,2, · · · ,n}:_投票者(individual)_の集合.

ここではA,Nは有限集合とし,♯A ≥3,N,ϕを仮定している.

.

Definition ( 選好と profile)

. .

... .

.

A上の選好(ballot)^def.⇔A上のlinear ordering.

例えばA = {a,b,c}のときには,例としてa<b<c,b<a<cなどが考えられる.

profile p= ⟨<^p_i:i∈N⟩^def.⇔各<^p_i が選好

ここで、<^p_i は「profile pにおけるi番目の投票者の選好」を意味する.

(6)

.

Definition

. .

... .

.

SOA

def.= 選好全体のなす集合

とする.このとき,profile全体のなす集合PAはPA= (SOA)ⁿである. .

Definition (Social Welfare Function)

. .

... .

.

V :P_A→SO_A_をSWF(Social Welfare Function_）という. このとき^,投票結果V(p)が表す選好を^<^psと書く^.

(7)

.

Definition (Arrow の定理における「民主的である」ことの定義 )

. .

... .

.

SWF V:PA ^→SOAが以下の性質をみたすとき,民主的であるという.

.

^.¹. ^Pareto[^{パレート条件}^,^{全会一致制}^]

任意のprofile pと任意のx,y∈A に対して,

∀i(x<^p_i y) ⇒x<^p_s y

.

^.². IIA(Independence of Irrelevant Alternative)[無関係な選択対象からの独立性] 任意の^{profile p,}p^′と任意の^x,y∈Aに対して,

∀i(x <^p_i y⇔x<^p_i^′y) ⇒ (x<^p_s y ⇔x <^p_s^′y)

.

^.³. Nondictatorship[_非独裁制]

次の条件をみたすような^dictator(独裁者⁾ⁱ0は存在しない^. 任意の^{profile p}に対して^,

∀x,y ∈A(x<^p_i

0^y ^⇒^x ^< p s y)

(8)

有限版 Arrow の定理

.

Theorem ( 有限版 Arrow の定理 )

. .

... .

.

民主的であるような^{SWF V}:P_A →SO_A_{は存在しない}.

つまり、^{SWF V} :P_A→SO_A_がPareto,IIAをみたすときには、以下をみたすような^dictator(独裁者⁾ⁱ0が存在するということである^.

任意のprofile pに対して

∀x,y ∈A(x<^p_i

0^y ^⇒^x ^< p s y)

(9)

無限版 Arrow の定理

ここから投票者の集合^Nを無限集合として考える^{.(i.e. N}= N) .

Theorem ( 無限版 Arrow の定理 )

. .

... .

. .民主的であるようなSWFが存在する.

「この定理が^RCA0上で^ACA0と同値になる」というのが^,本発表における主結果である.

無限版Arrowの定理を考えるとき,有限版と同じように選好やprofileは2階算術で

定めることができる.

しかし,profile全体のなす集合PAは2階算術では扱えない.

よって,N= NのときはSWFを今までとは別の形で定める必要がある. ここでは参考文献の6章に基づいた定式化を行うことにする.

(10)

Social Welfare Function

.

Definition (RCA

₀

)

. .

... .

.

次の条件をみたすとき、^B= ⟨{Xn:n∈ N}, ∨, ∧, ¬⟩は集合によるブール代数である^.

.

^.¹. ^X⁰^{= ϕ,}^X¹^{= N}

.

^.². ^∨^{: N}²^{→ N}^{s.t. X}^∨(ⁿ^,^m⁾⁼^Xⁿ^∪^X^m

.

^.³. ^∧^{: N}²^{→ N}^{s.t. X}^∧(ⁿ^,^m⁾⁼^Xⁿ^∩^X^m

.

^.⁴. ^¬^{: N → N}^{s.t. X}^¬(ⁿ⁾⁼^Xⁿ 以下では^|B|= {Xn:n∈ N}_と書く.

なお^,nと^Xnの同一視により^,|B|= Nである^.

ただし^,n^,^mで^Xn=X_m_{の場合もある}._{このときも}n,m_は(_{コードとして})_別物として扱うこととする^.

.

(11)

.

Definition (RCA

0

)

. .

... .

.

^.¹. ^F^{= ⟨F}^ab ^{: (a,}^{b) ∈ [A}^]²^⟩^が^(IIA^をみたす)B-Social Welfare Relation(B-SWR) である.

def.⇔ ∀a,b∈A,Fab ⊆ |B|

.

^.². ^任意の^{profile p}^と^(a,^{b) ∈ [A}^]²^{に対して、}

a<^p_s b by F^def.⇔ {i∈ N:a<^p_i b} ∈F_ab

.

^.³. ^F^{= ⟨F}^ab ^{: (a,}^{b) ∈ [A}^]²^⟩^が^B-SWF^である^.

def.⇔_任意のprofile p_に対して,<^p_s_がA_上のlinear order_を与える.

.

^.⁴. ^{B-SWF F}^{= ⟨F}^ab ^{: (a,}^{b) ∈ [A}^]²^⟩^が^Pareto^{条件をみたす}^.

def.⇔ ∀(a,b) ∈ [A]²に対して、^N∈Fab

FがIIAの条件をみたすことは上のFの定式化から明らかなので,この先の議論では^Fが^IIAをみたすことは表記しないことにする^.

(12)

.

Proposition1(RCA

0

)

. .

... .

.

F= ⟨Fab : (a,b) ∈ [A]²⟩_がPareto_をみたすSWF_である.

⇒任意の(a,b), (c,d) ∈ [A]²に対してFab =Fcd が成り立つ. よって,ParetoをみたすSWFはF ⊆ |B|とみなしてよい. .

Proposition2(RCA

0

)

. .

... .

.

F⊆ |B|とする.このとき,

FがParetoをみたすSWFである⇔Fはultrafilterである .

Proposition3(RCA

₀

)

.

. ^.

F⊆ |B|_とする.このとき, FがParetoをみたすSWFであるならば、

(13)

ultrafilter と Social Welfare Function

.

Definition (RCA

0

)

. .

... .

.

B˜= ⟨| ˜B|, ∨, ∧, ¬,0_B˜,1_B˜⟩は可算ブール代数である.

def.⇔ | ˜B| ⊆ Nで、∨, ∧, ¬,0_B˜,1_B˜はブール代数の公理をみたす.

.

Theorem (RCA

₀

)

. .

... .

.

RCA₀_{上で次は同値である}.

.

^.¹. ^WKL⁰^.

.

^.². ^{可算ブール代数}^B^˜^{= ⟨| ˜}B|, ∨, ∧, ¬,0_B˜,1_B˜⟩と,Σ⁰₁-definable filter F ⊂ | ˜B|に対して、Fを含むultrafilterが存在する.

(14)

[proof]最初に(1)⇒(2)を示す.

いま,⟨an:n∈ N⟩を| ˜B|のenumerationとする.ただし,a0=0_B˜,a1=1_B˜とする. さらにF= ∪s^Fs(ここで⟨Fs:s∈ N⟩は有限集合の増加列である)をΣ⁰₁-definable filterとする.

ここで,次の条件をみたすtree T⊆2^<Nを考える.

σ ∈T ⇔











lh(σ) ≥1→σ(0) =0 lh(σ) ≥2→σ(1) =1

∀n,m,l<lh(σ), an∈Flh(σ)^→σ(n) =1

(an^∧^am=a_l) ∧ (σ(n) = σ(m) =1) → σ(l) =1 (an≤am) ∧ (an=1) → σ(m) =1

a_n= ¬am^→σ(n) =1−σ(m)

すると,このTはinfinite treeとなる.(これはΣ⁰₁-inductionで示せる)

よってよりがとれる

(15)

[proof]次に(2)⇒(1)を示す.

⟨ai :i∈ N⟩: enumeration of countable symbols.

P : aiらを命題変数とする論理式全体の集合.

とする.ここで,各^{σ ∈}2^<Nについて^,¬(∧i<lh(σ)^a^σ( i)

i ⁾^を^Φ^σ^{と書くことにする}^.

ただし,a_i⁰= ¬ai,a_i¹=aiとする. α ∼ β ⇔⊢ α ↔ β_とし,B^˜=P/ ∼_とおく. いま^,T⊆²^<Nをinfinite tree_とする.

このとき^,F= {α/ ∼ ∈ | ˜B|:⊢ ∧_i_<_lΦσi ^→^α^{for some}^σ0, · · · , σ_l₋₁<T}

とすると^,Tはinfinite tree_なので0<F_であり,F_はΣ⁰₁-definable filter_となる. よって⁽²⁾より^F^⊂^Mとなるultrafilter M_{が存在する},

このとき^, f(i) =











1 ai/ ∼ ∈M 0 o.w.

とおけばfはTのpathである.

(16)

.

Theorem (ACA

0

)

. .

... .

.

Bを集合によるブール代数とする.

このとき,Paretoをみたし,dictatorをもたないB-SWF Fが存在する. [proof]| ˜B|= {n: ∀l<n(Xl ^,^Xn)}となるブール代数^B^˜が存在する^.

また^,F0= {n∈ | ˜B|:X_n_はco-finite}_はfilter_なので,_{このような}F₀_を含むultrafilter U_{が存在する}.

よって,F= {m: ∃n∈U(Xn=Xm)}とすれば,Fはnon-principalなBのultrafilter である.

したがって,Proposition3よりFはdictatorをもたないSWFである.

(17)

.

Proposition4(RCA

₀

)

. .

... .

. .∃Φ :Seq→PRA s.t. Φ(σ) = {n: σ(n) =1}(_のコード)

.

Theorem (RCA

₀

)

. .

... .

.

RCA0上で次は同値である.

.

^.¹. ^ACA⁰^.

.

^.². ^Pareto^をみたし^,dictator^{をもたない}^B-SWF^である^F^{が存在する}^.

(18)

[proof](1)⇒(2)はすでに示した.なのでここでは(2)⇒(1)を示す. 単射な関数f: N → Nを任意にとってくる.

このとき,PRAをfで相対化した集合(のコード)全体であるPRA^fが存在する. (2)とProposition3より,non-principal ultrafilterU⊆PRA^fが存在する.

ここで,Yn= {m: ∃l≤m f(l) =n}とする.

このとき,Proposition4よりΦ : N →PRA^f s.t.Φ(n) =Ynが存在する. これより,

Φ(n) ∈U⇔Ynはco-finite⇔n∈rng f

よって^{rng f}が存在することが示せた^.

(19)

参考文献

.

^.¹. Alan D. Taylor ”Social Choice and the Mathematics of Manipulation” (2005)