Using Theorema in the Formalization of Theoretical Economics

Wolfgang Windsteiger(SuperStar[ ])

RISC Institute
Johannes Kepler University Linz (JKU Linz)
Austria

Wolfgang.Windsteiger@risc.jku.at

(SuperStar[ ]) joint work with M. Kerber and C. Rowat, University of Birmingham, UK.

Contents

Introduction to the mathematics

Formalization in Theorema

Some aspects of prove techniques applied

Proving and computing in the same language

Conclusion & Outlook

Introduction to the Mathematics

Game theory plays important role in theoretical economics

We study one particular form of cooperative games: pillage games

Interesting area for formalization: new area / non-trivial / not too complicated

and: the intuition-based style of deriving results has proved to be error-prone

Pillage Games

Pillage games describe how n agents form coalitions in order to rob members of other coalitions of their possessions

agents: I={1,…,n}

possessions = allocations        ((Subscript[x, 1]),…,(Subscript[x, n])) s.t. (∑_(i=1)^n)(Subscript[x, i])=1

pillage possible if

winning coalition more powerful than the losing coalition

every member of the winning coalition benefits

power of coalition described by power function, e.g.

π( (Underscript[{1,2,3}, (Underscript[⏟, coalition])]), (Underscript[((1/2),(1/4),(1/4)), (Underscript[⏟, allocation])]))   …

power the coalition consisting of agents 1, 2, 3, 
where agent 1 owns 1/2 and the others own 1/4 of the total possessions, resp.

power functions satisfy certain axioms:

taking a new member into the coalition cannot decrease the power (WC)

giving additional holdings to some members of the coalition cannot decrease the power (WR)

giving additional holdings to all members of the coalition must increase the power (SR)

Two sets of interest:

the core, i.e. the set of allocations in which no pillage can occur

the stable set, i.e. a set of allocations which cannot pillage each other (internal stability) but all other possible allocations (called external stability)

Content of the Formalization

(Elementary) properties of allocations / power functions

An important property of the core (in the case n=3)

A pseudo-algorithm for computing the stable set (for certain classes of power functions)

Formalization of Pillage Games

Needs["Theorema`"]

SetGlobals[Prover->SetTheoryPCSProver]

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

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["WC", any[π,n],bound[(Subscript[allocation, n])[x]],
WC[π,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]}})} ]

Lemma 1

The first lemma states that the power of a coalition depends only on the holdings of the members of the coalition, but not on the holdings of the other agents.

Lemma["powerfunction-independent", any[π,n,C,x,y],with[(Subscript[allocation, n])[x] ∧ (Subscript[allocation, n])[y]∧C⊆ I[n]∧ powerfunction[π,n]],
(Underscript[∀, i∈ C])((Subscript[x, i])= (Subscript[y, i])) \[Implies] (π[C,x] = π[C,y])]

Prove[Lemma["powerfunction-independent"],using->{Definition["powerfunction"],Definition["WR"],Proposition["ref/as"]},by->PredicateProver,SearchDepth->100]//Timing

Simplified proof

Auxiliary knowledge

Proposition["ref/as",any[a,b],
(a=b)⇔(a≥b∧b≥a)]

Axiom["po",any[x,y],
({{x≥x, "refl"}, {(x≥y∧y≥x)⇒(x=y), "anti-sym"}})]

Prove[Proposition["ref/as"],using->Axiom["po"],SearchDepth->50]

Lemma 2

The second Lemma states that when the opposing coalitions consist of one element each and the power function is anonymous then the one which wins is the one with bigger holdings.

Lemma["ANdominates",any[n,x,y],
with[n∈ℕ∧n≥2∧(Subscript[allocation, n])[x] ∧(Subscript[allocation, n])[y]∧(W[n,x,y]={1})∧(L[n,x,y]={2})],
(Underscript[(Underscript[∀, π]), anonymous[π,n]∧powerfunction[π,n]])(dominates[y,x, π,n] ⇔ (Subscript[x, 1])> (Subscript[x, 2]))]

Definition["anonymity",any[π,n],bound[(Subscript[allocation, n])[x],(Subscript[allocation, n])[y]],
anonymous[π,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]))]

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["domination", any[π,n,x, y],
dominates[y,x,π,n] :⇔ π[W[n,x,y],x] > π[L[n,x,y],x]]

Lemma["ANdominates \[Implies]",any[n,x,y],with[appAlloc[n,x]∧(Subscript[allocation, n])[y]∧(W[n,x,y]={1})∧(L[n,x,y]={2})],
(Underscript[(Underscript[∀, π]), anonymous[π,n]∧powerfunction[π,n]])(dominates[y,x, π,n] \[Implies] (Subscript[x, 1])> (Subscript[x, 2]))]

Proof =>

Prove[Lemma["ANdominates \[Implies]"],using->{Definition["domination"], Lemma["AN all"],Definition["WR contrapositive"],Lemma["2inI"],Definition["powerfunction"],Lemma["perm swap"],Definition["appAlloc"]},SearchDepth->80,ProverOptions->{AllowIntroduceQuantifiers->False,RWCombine->True,DisableProver->{STC},DisableInferenceRule->{¢KBSetEquality,¢KBInclusion}}]//Timing

ProofShow[]

Auxiliary knowledge

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

Lemma["AN all",any[n,π,x],with[appAlloc[n,x]∧anonymous[π,n]],
∧{({{π[{1},x]=π[{2},perm[x,(Subscript[σ, 1,2])]]}, {(Subscript[allocation, n])[perm[x,(Subscript[σ, 1,2])]]}})} ]

Prove[Lemma["AN all"],using->{Lemma["ANswap"],Proposition["alloc perm"],Proposition["swapperm"],Definition["appAlloc"]},by->PredicateProver]//Timing

Lemma["ANswap",any[n,π,x],with[appL[n]∧anonymous[π,n]∧(Subscript[allocation, n])[x]],
π[{1},x]=π[{2},perm[x,(Subscript[σ, 1,2])]]]

Prove[Lemma["ANswap"],using->{Proposition["swapperm"],Proposition["swap idempotent"],Proposition["alloc perm"],Lemma["1inI"],Lemma["2inI"],Definition["anonymity"],Definition["perm"],Definition["swap"]},SearchDepth->80,ProverOptions->{AllowIntroduceQuantifiers->True,UseCyclicRules->False,EarlyRewriting->False,GRWTarget->{"goal","kb"}, DisableProver->{STC}}]//Timing

Lemma["perm swap",any[x],
(Subscript[perm[x,(Subscript[σ, 1,2])], 2])=(Subscript[x, 1])]

Prove[Lemma["perm swap"],using->{Definition["perm"],Definition["swap"]}]//Timing

Lemma["1inI",any[n],with[appL[n]],
{1}⊆I[n] ]

Prove[Lemma["1inI"],using->{Definition["agents"],Definition["appL"]},built–in->Built–in["Numbers"],ProverOptions->{SimplifyFormula->True}]//Timing

Lemma["2inI",any[n],with[appL[n]],
{2}⊆I[n] ]

Prove[Lemma["2inI"],using->{Definition["agents"],Definition["appL"]},built–in->Built–in["Numbers"],ProverOptions->{SimplifyFormula->True}]//Timing

Unproved: In the spirit of Theory Exploration, we would assume that the following facts have been proven earlier (e.g. when introducing the concept of "permutation").

Definition["perm",any[x,σ,k],
(Subscript[perm[x,σ], k]):=(Subscript[x, σ[k]])]

Definition["appAlloc",any[n,x],
appAlloc[n,x]:⇔(appL[n]∧(Subscript[allocation, n])[x])]

Definition["appL", any[n], 
appL[n]:⇔(n∈ℕ∧n≥2)]

Proposition["alloc perm",any[n,σ,x],with[appL[n]∧(Subscript[allocation, n])[x]∧permutation[σ,I[n]]],
(Subscript[allocation, n])[perm[x,σ]]]

Definition["permutation",any[σ,A],
permutation[σ,A]:⇔({{σ, ∷, A, (Overscript[→, bij.]), A  }})]

Definition["swap",any[i,j,k],
(Subscript[σ, i,j])[k]:={({{j, ⇐, k=i}, {i, ⇐, k=j}, {k, ⇐, otherwise}})} ]

Proposition["swapperm",any[n],with[appL[n]],
permutation[(Subscript[σ, 1,2]),I[n]]]

Proposition["swap idempotent",any[i],(Subscript[σ, 1,2])[(Subscript[σ, 1,2])[i]]=i]

Proof ⇐

Lemma["ANdominates ⇐",any[n,x,y],with[appAlloc[n,x]∧(Subscript[allocation, n])[y]∧(W[n,x,y]={1})∧(L[n,x,y]={2})],
(Underscript[(Underscript[∀, π]), anonymous[π,n]∧powerfunction[π,n]])((Subscript[x, 1])> (Subscript[x, 2])\[Implies]dominates[y,x, π,n])]

Prove[Lemma["ANdominates ⇐"],using->{Definition["domination"], Lemma["AN all"],Definition["SR"],Lemma["2inI"],Definition["powerfunction"],Lemma["perm swap"],Definition["appAlloc"]},built–in->{Built–in["Operators"]["¬","="]},SearchDepth->80,ProverOptions->{AllowIntroduceQuantifiers->False,RWCombine->True,DisableProver->{STP},DisableInferenceRule->{¢KBSetEquality,¢KBInclusion}}]//Timing

Lemma 3: Specialize n=3

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

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

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

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]])⟩]

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

Proof

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"]}]

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]]]

Executing a Pseudo-Algorithm

Algorithm["StableSet2",any[π],
stableSet[π]:={({{{({{"no stable", ⇐, 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["centre allocation",
(OverBar[p]) = ⟨(1/3),(1/3),(1/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["P",any[π],
P[π]:= {p[1,2,π],p[1,3,π],p[2,3,π]}]

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["r",any[π,i,j],
r[i,j,π]=(Underscript[∍, z∈M[i,π]])((Underscript[∀, x∈M[i,π]])(Subscript[z, j])≥ (Subscript[x, j]))]

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

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

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

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["emptyM,WIP",
¬empty[M[1,WIPπ]]]

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

Compute[dyadicSet[0,3]⋃(⋃_(i=1,…,3))S[i,WIPπ]]

Compute[S[1,WIPπ]]

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["WIPD"]}]

Compute[R[2,WIPπ]]

Compute[S[3,WIPπ]]

Compute[WIPπ[{1},⟨1,0,0⟩]]

Compute[WIPπ[{2,3},⟨1,0,0⟩]]

Compute[stableSet[WIPπ]]

Conclusion & Outlook

Appearance of formalization appealing to a "non-theorem-proving-mathematician"

Formalization influenced by features/weaknesses of particular provers used

Proving and computing in the same system/language very useful

Handling of current system too complicated