Using Theorema in the Formalization of Theoretical Economics

Manfred Kerber(( )^1)	Colin Rowat2	Wolfgang Windsteiger(( )^3)

1www.cs.bham.ac.uk/~mmk
2www.socscistaff.bham.ac.uk/rowat
1www.risc.jku.at/home/wwindste

Theorema Setup

Needs["Theorema`"]

SetOptions[Prove,transformBy->ProofSimplifier,TransformerOptions->{branches->Proved,steps->Useful}];

Power Function

Definition["agents", any[n], 
I[n]:={i (Underscript[|, i=1,…,n])}]

Definition["allocation", any[x,n],
(Subscript[allocation, n])[x] :⇔ (n∈ℕ∧is–tuple[x]∧ (\[LeftBracketingBar]x\[RightBracketingBar]=n)∧ (Underscript[∀, i∈I[n]])(Subscript[x, i])≥0 ∧((∑_(i∈I[n]))(Subscript[x, i]) = 1))]

Definition["allAllocations", any[n],
X[n] :={x(Underscript[\[VerticalSeparator], (Subscript[allocation, n])[x]])}]

Definition["WC", any[π,n],bound[(Subscript[allocation, n])[x]],
WC[π,n] :⇔(n∈ℕ∧(Underscript[(Underscript[∀, C1,C2]), C1 ⊂ C2 ∧ C2⊆I[n]])(Underscript[∀, x])π[C2,x]≥π[C1,x])]

Definition["WR", any[π,n],bound[(Subscript[allocation, n])[x], (Subscript[allocation, n])[y]],
WR[π,n] :⇔(n∈ℕ∧(Underscript[(Underscript[∀, C]), C⊆I[n]])(Underscript[∀, x,y])(((Underscript[∀, i∈C])(Subscript[y, i])≥ (Subscript[x, i]))\[Implies]π[C,y]≥π[C,x]))]

Definition["SR", any[π,n],bound[(Subscript[allocation, n])[x] , (Subscript[allocation, n])[y]],
SR[π,n] :⇔(n∈ℕ∧(Underscript[(Underscript[∀, C]), C⊆I[n]∧C≠∅])(Underscript[∀, x,y])(((Underscript[∀, i∈C])(Subscript[y, i])> (Subscript[x, i]))\[Implies]π[C,y]>π[C,x]))]

Definition["powerfunction", any[π,n],
powerfunction[π,n] :⇔ ∧{({{WC[π,n]}, {WR[π,n]}, {SR[π,n]}})} ]

Properties

Definition["AN",any[π,n],bound[(Subscript[allocation, n])[x],(Subscript[allocation, n])[y]],
AN[π,n] :⇔ (Underscript[(Underscript[∀, σ]), permutation[σ,I[n]]])(Underscript[(Underscript[∀, Cx,Cy,x,y]), Cx⊆I[n]∧Cy⊆I[n]])((Underscript[∀, i])(((i∈ Cx) ⇔ (σ[i]∈ Cy)) ∧ ((Subscript[x, i]) = (Subscript[y, σ[i]]))) \[Implies] (π[Cx,x] = π[Cy,y]))]

Domination

Definition["domination", any[π,n,x, y],
dominates[y,x,π,n] :⇔ π[W[n,x,y],x] > π[L[n,x,y],x]]

Definition["WinLose", any[n,x,y],
({{W[n,x,y] := {i(Underscript[\[VerticalSeparator], i∈I[n]])(Subscript[y, i])>(Subscript[x, i])}, "W"}, {L[n,x,y] := {i(Underscript[\[VerticalSeparator], i∈I[n]])(Subscript[x, i])>(Subscript[y, i])}, "L"}})]

Definition["dominion", any[π,n,Y],
D[Y,π,n]:={x(Underscript[\[VerticalSeparator], (Subscript[allocation, n])[x]])(Underscript[∃, y])(y∈Y∧dominates[y,x,π,n])}]

Definition["Un-dominion", any[π,n,Y],
U[Y,π,n] := X[n]∖D[Y,π,n]]

Core and stable set

Definition["core",any[π,n],
K[π,n] := U[X[n],π,n]]

Definition["IS",any[π,n,S],
IS[S,π,n] :⇔ (S ⋂ D[S,π,n]= ∅)]

Definition["ES",any[π,n,S],
ES[S,π,n] :⇔ (S ⋃ D[S,π,n]= X[n])]

Definition["stable", any[π,n,S],
stable[S,π,n] :⇔ (IS[S,π,n] ∧ ES[S,π,n])]

The stable set in n=3 with AN, CX, and RE

Algorithm["S",any[π],
stableSet[π]:={({{{({{"no stable set exists", ⇐, empty[M[1,π]]}, {where[𝒮=dyadicSet[0,3]⋃(⋃_(i=1,…,3))S[i,π],
{({{𝒮⋃P[π], ⇐, ¬fullSet[𝒮⋃D[𝒮,π,3]]}, {𝒮, ⇐, fullSet[𝒮⋃D[𝒮,π,3]]}, {"unknown X", ⇐, otherwise}})} ], ⇐, ¬empty[M[1,π]]}, {"unknown M", ⇐, otherwise}})} , ⇐, π[{1},t[1,3]]≥π[{2,3},t[1,3]]}, {dyadicSet[1,3]∖dyadicSet[0,3], ⇐, otherwise}})} ]

Definition["empty",any[ℳ],
empty[ℳ]:=ℳ=∅]

Lemma["D03",
dyadicSet[0,3]={t[1,3],t[2,3],t[3,3]}]

Lemma["D13",
dyadicSet[1,3]={t[1,3],t[2,3],t[3,3],s[1,2,3],s[1,3,3],s[2,3,3]}]

Definition["maxBalanced",any[π,i],
M[i,π]={x∈B[i,π]\[VerticalSeparator]((Subscript[x, i])= (max_(y∈B[i,π]))(Subscript[y, i]))}]

Definition["powerBalance",any[π,i],
B[i,π]:={x∈X[3]\[VerticalSeparator](π[{i},x]= π[I[3]∖{i},x])}]

Definition["tyrannical",any[i,n],
t[i,n]:=⟨{({{1, ⇐, j=i}, {0, ⇐, otherwise}})} (Underscript[|, j∈I[n]])⟩]

Definition["split allocation",any[k,j,n],
s[j,k,n]:=⟨{({{(1/2), ⇐, ((i=j )∨( i=k))}, {0, ⇐, otherwise}})} (Underscript[|, i∈I[n]])⟩]

Definition["Si",any[i,π],
S[i,π]:=R[i,π]⋃(Sq[i,π]⋂M[i,π])]

Definition["RMaxBalanced",any[π,i],
R[i,π]:={r∈M[i,π]\[VerticalSeparator] (Underscript[∃, j∈I[3]∖{i}])(Underscript[∀, s∈M[i,π]])(Subscript[r, j])≥(Subscript[s, j])}]

Definition["P",any[π],
P[π]:= {p[1,2,π],p[1,3,π],p[2,3,π]}]

Definition["pij",any[π,j,k],
p[j,k,π]:={({{(1/2)⊙(r[3,1,π]⊕r[3,2,π]), ⇐, (j=1)∧(k=2)}, {(1/2)⊙(r[2,1,π]⊕r[2,3,π]), ⇐, (j=1)∧(k=3)}, {(1/2)⊙(r[1,2,π]⊕r[1,3,π]), ⇐, (j=2)∧(k=3)}})} ]

Definition["tup+*",any[x,y],
({{x⊕y:=⟨(Subscript[x, i])+(Subscript[y, i])(Underscript[|, i=1,…,\[LeftBracketingBar]y\[RightBracketingBar]])⟩}, {x⊙y:=⟨x*(Subscript[y, i])(Underscript[|, i=1,…,\[LeftBracketingBar]y\[RightBracketingBar]])⟩}})]

Definition["r",any[π,i,j],
r[i,j,π]=(Underscript[∍, z∈M[i,π]])((Underscript[∀, x∈M[i,π]])(Subscript[z, j])≥ (Subscript[x, j]))]

Definition["centre allocation",
(OverBar[p]) = ⟨(1/3),(1/3),(1/3)⟩]

Use[{Built–in["Connectives"],Built–in["Quantifiers"],Built–in["Tuples"],Built–in["Sets"],Built–in["Numbers"]}]

UseAlso[{Algorithm["S"],Lemma["D13"],Lemma["D03"],Definition["tyrannical"],Definition["split allocation"],Definition["agents"],Definition["Si"],Definition["RMaxBalanced"],Definition["centre allocation"],Definition["r"],Definition["P"],Definition["pij"],Definition["tup+*"],Definition["empty"]}]

Wealth is Power

Definition["WIP",any[C,x],
WIPπ[C,x]= (∑_(i∈C))(Subscript[x, i])]

UseAlso[Definition["WIP"]]

Compute[stableSet[WIPπ]]

Lemma["emptyM,WIP",
¬empty[M[1,WIPπ]]]

Lemma["WIPR",
({{R[1,WIPπ]={⟨1/2,0,1/2⟩,⟨1/2,1/2,0⟩}}, {R[2,WIPπ]={⟨0,1/2,1/2⟩,⟨1/2,1/2,0⟩}}, {R[3,WIPπ]={⟨1/2,0,1/2⟩,⟨0,1/2,1/2⟩}}})]

Lemma["midpoint of B,WIP",
({{Sq[1,WIPπ]⋂M[1,WIPπ]={⟨1/2,1/4,1/4⟩}}, {Sq[2,WIPπ]⋂M[2,WIPπ]={⟨1/4,1/2,1/4⟩}}, {Sq[3,WIPπ]⋂M[3,WIPπ]={⟨1/4,1/4,1/2⟩}}})]

Lemma["WIPD",any[S],
fullSet[{⟨0,0,1⟩,⟨0,(1/2),(1/2)⟩,⟨0,1,0⟩,⟨(1/4),(1/4),(1/2)⟩,⟨(1/4),(1/2),(1/4)⟩,⟨(1/2),0,(1/2)⟩,⟨(1/2),(1/4),(1/4)⟩,⟨(1/2),(1/2),0⟩,⟨1,0,0⟩}⋃D[{⟨0,0,1⟩,⟨0,(1/2),(1/2)⟩,⟨0,1,0⟩,⟨(1/4),(1/4),(1/2)⟩,⟨(1/4),(1/2),(1/4)⟩,⟨(1/2),0,(1/2)⟩,⟨(1/2),(1/4),(1/4)⟩,⟨(1/2),(1/2),0⟩,⟨1,0,0⟩},WIPπ,3]]]

UseAlso[{Lemma["midpoint of B,WIP"],Lemma["WIPR"],Lemma["emptyM,WIP"],Lemma["WIPD"]}]

Compute[stableSet[WIPπ]]

Strength in Numbers

Definition["SIN",any[C,x,ν],
(Subscript[SINπ, ν])[C,x]= (∑_(i∈C))((Subscript[x, i])+ν)]

UseAlso[{Definition["SIN"]}]

Compute[stableSet[(Subscript[SINπ, 2])]]

Compute[stableSet[(Subscript[SINπ, 0.5])]]

Lemma["emptyM,SIN",
empty[M[1,(Subscript[SINπ, 0.5])]]]

UseAlso[{Lemma["emptyM,SIN"]}]

Compute[stableSet[(Subscript[SINπ, 0.5])]]

Use[]

Proof of a Lemma

If the core is empty then the tyrannical elements (one agent possesses everything) are dominated by the half splits (e.g., ⟨1/2,1/2,0) dominates ⟨0,0,1⟩), i.e.

Lemma["Core n=3,a", any[π],
(K[π,3]=∅) \[Implies] (Underscript[∀, i,j,k∈I[3]]) (distinct[i,j,k]\[Implies]t[i,3]∈ D[{s[j,k,3]},π,3])]

Prove[Lemma["Core n=3,a"],using->{Theorem["Jordan[2006a],2.6a,contra"],Lemma["s dominates t"],Lemma["tyrannical allocation"],Definition["dominion"],Definition["domination"]},
by->SetTheoryPCSProver,ProverOptions->{DisableProver->{STKBR}},built–in->{Built–in["Number Domains"],Built–in["Connectives"]},SearchDepth->110]//Timing

Simplified Proof

Lemmas needed …

Interesting Lemma (computation!)

Lemma["s dominates t",any[i,j,k∈I[3]],with[distinct[i,j,k]],
({{W[3,t[i,3],s[j,k,3]]=I[3]∖{i}}, {L[3,t[i,3],s[j,k,3]]={i}}})]

Compute[W[3,t[1,3],s[2,3,3]],using->{Definition["agents"],Definition["WinLose"],Definition["tyrannical"],Definition["split allocation"]},built–in->{Built–in["Connectives"],Built–in["Quantifiers"],Built–in["Tuples"],Built–in["Sets"],Built–in["Numbers"]}]

Compute[W[3,t[2,3],s[1,3,3]],using->{Definition["agents"],Definition["WinLose"],Definition["tyrannical"],Definition["split allocation"]},built–in->{Built–in["Connectives"],Built–in["Quantifiers"],Built–in["Tuples"],Built–in["Sets"],Built–in["Numbers"]}]

Compute[L[3,t[2,3],s[1,3,3]],using->{Definition["agents"],Definition["WinLose"],Definition["tyrannical"],Definition["split allocation"]},built–in->{Built–in["Connectives"],Built–in["Quantifiers"],Built–in["Tuples"],Built–in["Sets"],Built–in["Numbers"]}]

Definition["distinct",any[i,j,k],
distinct[i,j,k]:⇔(i≠j∧i≠k∧j≠k)]

Prove[Lemma["s dominates t"],built–in->{Definition["distinct"],Definition["agents"],Definition["WinLose"],Definition["tyrannical"],Definition["split allocation"],Built–in["Connectives"],Built–in["Quantifiers"],Built–in["Tuples"],Built–in["Sets"],Built–in["Numbers"]},ProverOptions->{DisableProver->{STKBR,STP,QR,PND,CDP},TransformRanges->False}]

Without proof:

Theorem["Jordan[2006a],2.6a,contra",any[π,n],
(Underscript[∀, i∈I[n]])((t[i,n] ∉ K[π,n]) \[Implies] π[I[n]∖ {i},t[i,n]]> π[{i},t[i,n]])]

Lemma["tyrannical allocation",any[i,n],with[n∈ℕ∧i∈I[n]],
(Subscript[allocation, n])[t[i,n]]]