We consider a recent game theory paper, on democratic forking: suppose you want to go to the opera with a group of 10 friends, with a choice of two operas. Everyone has a preference for one of the operas, but everyone also prefers a large community over a small one. Is there an assignment of each friend to one opera that is stable? The paper answers the question afirmatively giving an algorithm. We have formalised the main result of that paper in the proof assistant Isabelle. This provides proofs of the results that are much more reliable, since computer-checked, than paper-and-pencil proofs. The exercise has also been useful for improving the paper-and-pencil proof. We also contribute some results concerning the uniqueness of assignments.
About three years ago, a formalism in the field of social choice (a subfield of game theory), was
presented: democratic forking [
An assignment is a function assigning each agent to an alternative. It is stable if no agent has an incentive to switch. The main question is: can a stable assignment be found? The authors give an afirmative answer via an algorithm with several variants, and also address issues such as strategy-proofness.
This seemingly simple formalism quickly leads to non-trivial considerations. E.g., while it is relatively easy to see that stable assignments exist in the case of two alternatives, they do not always exist for three or more alternatives.
In this paper, we present work on implementing the proposed formalism in the proof assistant
Isabelle/HOL [
Isabelle/HOL [
More generally, theorem provers are software for conducting mathematical proofs on a
computer to obtain a high degree of confidence [
Initially we intended to take the main theorem of [
We have modelled our development as closely as possible on our source [
The rest of this paper is organised as follows: the next section defines the basic concepts.
Section 3 presents the algorithm for finding a stable assignment and the proof of this fact.
Section 4 gives additional results concerning uniqueness and elicitation. Section 5 concludes.
For space reasons, some of the proofs are not presented here; a technical report is available [
In this section we recall the formalism of [
Definition 1.
• Consider a set of alternatives {, } and a set of voters1 = {1, . . . , }. • A community is an element of := {, }× N, i.e., an alternative paired with the number of voters who have chosen this alternative. • A preference is a subset of × , i.e., a relation on communities. We assume that preferences are monotonic, i.e., (, ) ≻ (, − 1) ≻ . . . ≻ (, 1) and (, ) ≻ (, − 1) ≻ . . . ≻ (, 1) (and antisymmetric and transitive). • A preference profile is an element of (2× ). It states the preferences of all voters. We denote by ≻ the preference of voter .
Example 1. Consider = {1, 2}, where the preference profile is given by 1 : (, 2) ≻ 1 (, 1) ≻ 1 (, 2) ≻ 1 (, 1) and 2 : (, 2) ≻ 2 (, 1) ≻ 2 (, 2) ≻ 2 (, 1). E.g., 1 prefers being alone with to being in a group of 2 with . 1We use this word rather than “agent” to avoid the letter , to be confused with .
At this point we state an amazing observation: in [
In Isabelle, we have a so-called theory file containing all definitions and theorems, with their proofs, of our development. For modelling the above definitions, the theory file contains the following: type_synonym ’Al community = "’Al * nat" type_synonym ’Al preference = "(’Al community) rel" definition monotonic :: "’Al preference ⇒ bool" where "monotonic pref = (∀ S j k. k≤ j →− ((S,j),(S,k)) ∈ pref)"
In contrast to Def. 1, the set of alternatives is not fixed to being {, } but rather it is modelled by a type parameter ’Al for the sake of generality.
Note that the above lines define monotonicity but do not yet impose that all preferences used should actually be monotonic.
Definition 2. An assignment is a function : → {, }. It can be lifted to a community assignment, i.e., for any voter ∈ , the pair ( (), | − 1( ())|) gives the community of .
We often denote an assignment as ⟨, ⟩ where and are the sets of voters mapped to and respectively.
In Isabelle, these definitions look as follows: type_synonym (’V,’Al) assignment = "’V ⇒ ’Al" definition commAss ::"(’V,’Al) assignment ⇒ ’V ⇒ ’Al community" where "commAss f v = (f v, card (f -‘ {f v}))"
In Isabelle/HOL, -‘ gives the inverse of a function, so f -‘ {f v} is the set of voters mapped to f v by f, and card (f -‘ {f v}) is the cardinality of that set.
Given an assignment , a subset of voters may be interested in deviating, i.e., there may be an assignment ′ such that for all voters in the subset, ′ assigns them to another alternative, and they all prefer their “ ′-community” over their “ -community”. Formally we define:
• Given an assignment : → {, }, a deviation is an assignment ′ : → {, } such that ̸= ′ and for all voters where () ̸= ′(), ( ′(), | ′− 1( ′())|) ≻ ( (), | − 1( ())|). (1) • If no deviation exists, then an assignment is stable.
Example 2. Consider again Ex. 1. Each voter has an alternative at which she definitely wants to be. Thus, the only stable assignment is ⟨{1}, {2}⟩, and the community of 1 is (, 1) and that of 2 is (, 1).
Before we present the Isabelle versions of these definitions, we introduce the convenient
Isabelle feature of locales. A locale allows us to xfi a certain preference profile and make certain
assumptions that are also made in [
UNIV denotes the universal set, which can be enhanced with a type declaration, so that finite (UNIV :: ’V set) says: the voter set is finite.
We could have also fixed the alternative set to {, } here, but we decided to make the assumption of a two-element alternative set only where needed.
There is an Isabelle syntax feature allowing us to write ⪰ ′ rather than (, ′) ∈ preferenceProfile .
Now the Isabelle version of Def. 3: definition stable :: "(’V,’Al) assignment ⇒ bool" where "stable f = (∄ f’. deviation f’ f)" definition deviation :: "(’V,’Al) assignment ⇒ (’V,’Al) assignment ⇒ bool" where "deviation f’ f = (f’̸=f ∧ (∀ v. (f’ v) ̸= (f v) →−
(commAss f’ v) ⪰ (commAss f v)))"
Observe that the use of ⪰ in the definition of deviation means that the definition depends
on the preference profile, which is not visible in the declared type of deviation since an element
of the type (’V,’Al) assignment does not carry any information about the preferences in
it. This is possible thanks to the locale, fixing a preference profile. Around 80% of the lines of
our Isabelle code are within the scope of the locale.
3. An Algorithm for Finding a Stable Assignment
Given a (monotonic) preference profile, one may wonder whether a stable assignment always
exists and if yes, how it can be found. In [
= , = ∅, ← | |, ← | | while true do ← max{ : 0 ≤ ≤ , |{ ∈ : (, + ) ≻ (, )}| ≥ } if = 0 then
return {, } else let = { ∈ : (, + ) ≻ (, )} ← ∪ , ← ∖ ← | |, ← | | endif endwhile Theorem 1. For any monotonic profile, there is a stable assignment.
Incidentally, the presentation in [
To understand the algorithm better, it is useful to refine the notions of deviation and stability by restricting the direction in which voters move:
• Given an assignment , an -deviation is a deviation ′ such that for any with ′() ̸= (), we have ′() = .
• If no -deviation exists, then an assignment is -stable.
In Isabelle these definitions look as follows: definition stable_alt :: "(’V,’Al) assignment ⇒ ’Al ⇒ bool" where "stable_alt f S = (∄ f’. dev_alt f’ f S)" definition dev_alt :: "(’V,’Al) assignment ⇒ (’V,’Al) assignment ⇒ ’Al⇒bool" where "dev_alt f’ f S =
(deviation f’ f ∧ (∀ v. (f’ v) ̸= (f v) →− f’ v = S))"
The following Isabelle lemma, whose proof has 24 lines, states that for the two-alternative case, -stability and -stability together imply stability: lemma stabilityAB : assumes "stable_alt f A" and "stable_alt f B" and "∀ x. (x=A) = (x̸=B)" shows "stable f"
The third assumption states that there are exactly two distinct alternatives.
So the algorithm initially places all voters in the -community, and the while-loop computes a sequence of -deviations. For any threshold value ≤ , the set { ∈ : (, + ) ≻ (, )} is the set of all voters who would switch from to under the condition that, well, the size of the -community grows by at least voters. If the cardinality of that set is ≥ , then a -deviation exists, and the algorithm actually uses the maximum value of in each step.
While the algorithm uses the maximal possible -deviation in each step, its correctness and
termination are guaranteed even for arbitrary -deviations.
3.1. A Paper-and-pencil Version of the Induction Step
The Isabelle/HOL implementation of the formalism of [
Concerning the correctness of the algorithm, the proof of the theorem given in [
So at the heart of the correctness proof for the algorithm lies an “induction step” saying that
due to monotonicity, there could not possibly occur a situation where voters would want to
move (back) to . This induction step is presented in [
We formalise the induction step as the following lemma: Lemma 1. Let be an -stable assignment and ′ be a -deviation of . Then ′ is -stable.
Developing the paper-and-pencil proof of this induction step helped us implement the Isabelle/HOL proof and vice versa. Before we present the paper-and-pencil proof, we give a brief outline: Our proof assumes, for the purpose of deriving a contradiction, that after some “forward” step (voters moving to ), there are voters moving (back) to . If this “backward” step only concerns voters just arrived from , then the fact that they want to go back to contradicts them wanting to go to in the “forward” step. If this “backward” step concerns at least one voter previously in , it turns out that this voter would have wanted to move to even before the “forward” step, which breaks our induction hypothesis.
Proof. (Lemma 1) Throughout this proof, we frequently use monotonicity of preferences, and for this, knowing the set inclusions between certain sets of voters is crucial. With the help of some diagrams (see Fig. 2 and 3), these inclusions are easy to see.
The symbol ⊎ denotes disjoint union.
In this proof we consider a hypothetical “backward step” leading to assignment ′′. We use a three-letter notation for voter sets, indicating in what community the voters are according to , AXX
BBX ⇝
AAA
XBX ⇝ ?
AXA
XBB ′, and ′′ respectively. E.g., ABX := { | () = ∧ ′() = } is the set of voters moving from to in the forward step with nothing specified for the backward step. Some voters move from to as illustrated by the boxes linked by ⇝ in Fig. 2, where AXX := − 1(), BBX := − 1(), AAA = ′− 1()3, XBX = ′− 1(), ABX := { | () = ∧ ′() = }. For every voter ∈ ABX , since she moved, we have (, |XBX |) ≻ (, |AXX |) (we suggest to look at Fig. 2 again).
For the purpose of deriving a contradiction, assume there was a “backward step” from (possibly back) to . We denote by ′′ the assignment after this backward step. Case 1: The backward step only concerns voters originally in , i.e., { | ′() = ∧ ′′() = } ⊆ ABX , or equivalently, { | ′() = ∧ ′′() = } = { | () = ∧ ′() = ∧ ′′() = } =: ABA. This case is illustrated in Fig. 2 and we write AXA := ′′− 1(), XBB := ′′− 1().
For every voter ∈ ABA, since she moved, we have By monotonicity By transitivity, (2) and (4) imply that (, |AXA|) ≻ (, |XBX |). (, |AXX |) ≻ (, |AXA|).
(, |XBX |) ≻ (, |AXA|).
This gives a contradiction to (3).
Case 2: The “backward step” concerns at least one voter originally in , i.e., { | ′() = ∧ ′′() = } ∖ ABX ̸= ∅. This case is illustrated in Fig. 3 and we write XXA := ′′− 1(), XBB := ′′− 1(), BBA := { | () = ′() = ∧ ′′() = }. 3Note that by construction ′− 1() ⊆ − 1() and ′− 1() ⊆ ′′− 1(), so we write AAA and not XAX . (2) (3) (4) ABX AXX
BBX ⇝
AAA ABA
XBX ⇝ ? ABA
XXA
AXX XBB
AXX ⊎ BBA For every voter ∈ BBA, since she moved, we have
(, |XXA|) ≻ (, |XBX |).
We now consider a further set, namely AXX ⊎ BBA, i.e., the voters originally in , plus the voters originally in that move to in the backward step. It is also illustrated in Fig 3 all to the right. Observe that XXA ⊆ AXX ⊎ BBA, and so by monotonicity we have that for every voter, in particular any ∈ BBA, and again by monotonicity, By transitivity, (5)-(7) imply that (, |AXX ⊎ BBA|) ≻ (, |XXA|),
(, |XBX |) ≻ (, |BBX |).
(, |AXX ⊎ BBA|) ≻ (, |BBX |) which contradicts the assumption that is -stable. In short, if there was such a voter , she would have wanted to move to even before the “forward step” took place. So in any case, the assumption that there was a “backward step” leads to a contradiction. □ (5) (6) (7) 3.2. Induction Step in Isabelle In Isabelle, Lemma 1 looks as follows: lemma staysStable : assumes "stable_alt f A" and "∀ x. (x=A) = (x̸=B)" and "dev_alt f’ f B" shows "stable_alt f’ A"
The proof of this lemma has around 120 lines of Isabelle proofscript but it relies on numerous auxiliary lemmas. It is the main contribution of this work. Some of the additional overhead in the Isabelle proof is related to the subset relations among the various sets of voters and the arities of these sets. Such set-theoretic reasoning is considered trivial in paper-and-pencil proofs but must be spelt out in the smallest detail in Isabelle. 3.3. The Entire Algorithm The previous two subsections talk about deviations (Def. 3) and -deviations (Def. 4). These definitions do not tell us how to construct an ′, given . In contrast, Algorithm 1 calculates a number and then a set based on , which translates into an assignment. But is this assignment really a -deviation? On the paper-and-pencil level this might be considered “obvious by construction” but in Isabelle, it requires some overhead that we outline here.
Given an assignment , the4 alternative and a natural number , we define the set of voters who would switch to provided the size of the -community grows by at least . We also define the maximum such that the cardinality of that set is greater or equal to , exactly as this is done in the algorithm: definition deviators :: "(’V,’Al) assignment ⇒ ’Al ⇒ nat ⇒ ’V set" where "deviators f B j = { v. f v ̸= B ∧
(B, card (f -‘ {B}) + j) ⪰ (f v, card (f -‘ {f v}))}" definition dev_max :: "(’V,’Al) assignment ⇒ ’Al ⇒ nat" where "dev_max f B = Max {j. card (deviators f B j) ≥ j}"
We continue our Isabelle implementation of the algorithm, which is naturally in a functional
programming style, as Isabelle/HOL is based on the typed -calculus [
( v. if v∈deviators f B (dev_max f B) then B else f v)"
If the deviators set is empty, then this assignment will be identical to and we have reached a fixpoint, which is the break condition of the algorithm loop. In this case, the assignment reached is -stable: lemma max_dev_alt_is_stable : assumes "max_dev_alt f B = f" shows "stable_alt f B" which takes 20 lines to prove using some auxiliary lemmas.
The function algo iterates max_deviat_alt, starting with the initial assignment . A, i.e., the assignment assigning all voters to A: 4The lemmas are formulated for Algorithm 1, which moves voters from to , but technically, A and B are just variables, so the lemmas also hold for and swapped. fun algo where "algo 0 A B = ( v. A)" | "algo (Suc j) A B = max_dev_alt (algo j A B) B"
This function is written using the function package of Isabelle/HOL which provides excellent
support for proving termination and other things [
The following lemma completes the induction proof based on Lemma 1 (staysStable); the computed assignment is -stable at all times: lemma staysStableInduct : assumes "∀ x. (x=A) = (x̸=B)" shows "stable_alt (algo n A B) A"
The following lemma states that after at most a number of iterations corresponding to the number of voters, a fixpoint is reached: lemma is_fixpoint : shows "algo (Suc (Suc (card (UNIV::’V set)))) A B =
algo (Suc (card (UNIV::’V set))) A B"
For space reasons, this paper does not present any Isabelle/HOL proofs, except the proof of the Isabelle version of Thm. 1. This proof has just five lines, and is based on some comprehensible lemmas stated above, so we consider it the occasion to show how lemmas are tied together in an Isabelle/HOL proof.
The theorem states that after at most a number of iterations corresponding to the number of voters, the algorithm has computed a stable assignment. In the proof, the successor of the cardinality of the voter set is abbreviated by the macro ?n1 for readability: lemma algo_finds_stable_assignment : assumes "∀ x. (x=A) = (x̸=B)" shows "stable (algo (Suc (card (UNIV::’V set))) A B)"
(is "stable (algo ?n1 A B)") proof have "stable_alt (algo ?n1 A B) A"
using assms by (rule staysStableInduct) moreover have "algo (Suc ?n1) A B = algo ?n1 A B"
by (rule is_fixpoint) hence "max_dev_alt (algo ?n1 A B) B = algo ?n1 A B" by simp hence "stable_alt (algo ?n1 A B) B" by (rule max_dev_alt_is_stable) ultimately show ?thesis using assms by (rule stabilityAB) qed
Note that the third line of the proof efectively uses the recursive definition of above. algo given
This completes the presentation of the Isabelle/HOL development concerning Algorithm 1
and thus the main result of [
Unlike [
We found that this result can be generalised to an arbitrary, even infinite, number of alternatives, so we make this assumption, in this subsection only.
We say that a preference is clear if there exists an alternative that is preferred to any other alternative even for the smallest, i.e., one-member, community. Note that this is a generalisation of “non-interleaving” to an arbitrary number of alternatives. It is defined in Isabelle as follows: definition clear :: "’Al preference ⇒ bool" where "clear p = (∃ S. ∀ T. S̸=T →−
(∀ n. ((S,1),(T,n)) ∈ p))"
E.g., for three alternatives, (, 2) ≻ (, 1) ≻ (, 2) ≻ (, 2) ≻ (, 1) ≻ (, 1) is a clear preference (for ). The example also illustrates that the name “non-interleaving” would have been inappropriate for more than two alternatives.
For space reasons we only present the final result, stating that any stable assignment is necessarily the assignment mapping each voter to her clearly preferred alternative. This additional development consists of about 130 lines. lemma genericUniqueStable :
assumes "∀ v. clear (preferenceProfile v)" and "stable f"
shows "f = ( v. THE S. ∀ T. S̸=T →− (∀ n. (S,1) ⪰ (T,n)))"
4.2. Non-critically-interleaving Preferences for Elicitation
A somewhat weaker condition than “non-interleaving” is also proposed by [
The essential point is this: for a voter, there is a threshold value at which she would definitely want to be at her preferred alternative. Note that for = 1, the definition stipulates · · · ≻ (, 0); this spurious part simply disappears.
Non-critically-interleaving preferences facilitate elicitation. The threshold of each voter is suficient for deciding the condition (, + ) ≻ (, ) of Algorithm 1. We contribute the following lemma.
Lemma 2. Consider , , ∈ [1, ] such that + = and 0 < ≤ and a non-criticallyinterleaving preference ≻ .
If the threshold of ≻ is (, ) for some ≤ + , or (, ) for some > , then (, + ) ≻ (, ). Otherwise, (, ) ≻ (, + ).
In Isabelle the lemma looks as follows. This development has around 80 lines. lemma nci_elicitation : assumes "a+b= card (UNIV::’V set)" (is "a+b=?n") and "j ≤ a" and "monotonic pref" and "trans pref" and "threshold pref B t A ∨ threshold pref A t B" shows "if ((threshold pref B t A ∧ t ≤ b+j) ∨
(threshold pref A t B ∧ t > a)) then ((B,b+j),(A,a)) ∈ pref else ((A,a),(B,b+j)) ∈ pref" 4.3. Strong Preferences for Uniqueness [2, Prop. 2] states conditions for uniqueness of assignments, assuming non-critically-interleaving preferences. We make the assumptions both weaker (we do not require non-criticallyinterleaving preferences) and more explicit.
Below, ′ (′) denotes the set of voters with preferred alternative () who will definitely
be with () in any stable assignment. Our definition of these sets is equivalent to that of [
:= ′ := max{ : 0 ≤ ≤ , |{ ∈ : (, ) ≻ (, )}| ≥ } { ∈ : (, ) ≻ (, )} and ′ be defined analogously. If for each voter ∈ ∖ (′ ∪ ′), either (, |′| + 1) ≻ (, − | ′|) or (, |′| + 1) ≻ (, − | ′|), then there is a unique stable assignment. Example 3. Consider = 9 and suppose that (, 1) ≻ 1 (, 9), ≻ 2=≻ 1, (, 2) ≻ 3 (, 9), (, 5) ≻ 4 (, 9), ≻ 5=≻ 4, (, 2) ≻ 6 (, 9), ≻ 7=≻ 6, (, 3) ≻ 8 (, 7), (, 6) ≻ 9 (, 4) Then ′ = {1, 2, 3, 4, 5} and ′ = {6, 7}. Moreover 8 will necessarily join ′ and 9 will join ′, so there is a unique stable assignment.
Here is the Isabelle version of Prop. 1: lemma argmaxUniqueStable : assumes "stable f" and "∀ x. (x=A) = (x̸=B)" and "(∀ v. v∈/ sureFirstAlt B A ∪ sureFirstAlt A B →− ((B,card (sureFirstAlt B A) + 1) ⪰
(A,card (UNIV::’V set)-card (sureFirstAlt B A))) ∨ ((A,card (sureFirstAlt A B) + 1) ⪰
(B,card (UNIV::’V set)-card (sureFirstAlt A B))))" shows "f = ( v. if v ∈ (sureFirstAlt A B) ∨ (A,card (sureFirstAlt A B) + 1) ⪰ (B,card (UNIV::’V set)-card (sureFirstAlt A B)) then A else B)"
The Isabelle development consists of approximately 250 lines of code. 4.4. A Characterisation of Uniqueness [2, Thm. 2] states that there is a unique stable assignment if and only if Algorithm 1 returns the same assignment as its symmetric version starting from ⟨∅, ⟩. The proof of this theorem refers to “the properties of Algorithm 1” which we find too vague. In fact, we were very surprised when we discovered that we needed preferences to be total, but for all previous results we do not! And even here, we are not sure that the result really needs total preferences.
To prove Thm. 2, the following lemma is useful. It says that there cannot be two distinct stable assignments such that one is obtained from the other by switching some voters. Lemma 3. Let = ⊎ ⊎ ⊎ where ̸= ∅ and ̸= ∅. Let 1 = ⟨ ⊎ , ⊎ ⟩ and 2 = ⟨ ⊎ , ⊎ ⟩. Assume all preferences are total.
Then 1 and 2 cannot both be stable assignments.
Proof. For the purpose of deriving a contradiction, let us assume that 1 and 2 are both stable assignments.
Since 1 is stable, and preferences are total, there is at least one voter ∈ such that (, | ⊎|) ≻ (, | ⊎ ⊎|) (otherwise the group would move to ). By monotonicity (, | ⊎ |) ≻ (, | ⊎ |). If || + 1 ≥ | |, then (, | ⊎ | + 1) ≻ (, | ⊎ |) and thus (, | ⊎ | + 1) ≻ (, | ⊎ |), so would want to deviate from 2, contradicting the stability of 2. Therefore || + 1 < ||.
In the previous paragraph, by switching the roles of and , and and , we can show that || + 1 < ||.
This is a contradiction, so our assumption that 1 and 2 are both stable is false. □
Its Isabelle version looks as follows: lemma noSwapStable : assumes "∀ x. (x=A) = (x̸=B)" and "(∀ v x y. x̸=y →− (x ⪰ y) ∨ y ⪰ x)" and "VA ∩ C = {} ∧ VA ∩ D = {} ∧ D ∩ C = {}" and "C̸={}" and "D̸={}" shows "¬ (stable ( u. if u∈VA∪C then A else B) ∧
stable ( u. if u∈VA∪D then A else B))"
So if a profile admits (at least) two distinct stable assignments, then one must be obtained from the other by shufling some voters from to or vice versa, but not both ways.
Proof. One direction is trivial and already clearly stated in [
Now assume that Algorithm 1 as well as the reverse Algorithm 1 both return the assignment 1, and for the purpose of deriving a contradiction, that another stable assignment 2 exists. Without loss of generality, using Lemma 3, assume that 1 has the form ⟨, ⊎ ⟩ and 2 has the form ⟨ ⊎ , ⟩. As Algorithm 1 starts from the assignment ⟨, ∅⟩ and terminates in ⟨, ⊎⟩, at some iteration it must have “skipped over” ⟨ ⊎, ⟩, i.e., it must be possible to write = ′ ⊎ ′′ with ′′ ̸= ∅, = ′ ⊎ ′′ ⊎ ′′′ with ′ ̸= ∅, such that some iteration of Algorithm 1 goes from ⟨ ⊎ ′ ⊎ ′′ ⊎ ′ ⊎ ′′, ′′′⟩ to ⟨ ⊎ ′ ⊎ ′, ′′′ ⊎ ′′ ⊎ ′′⟩. This means that for each voter ∈ ′′, we have
(, |′′′ ⊎ ′′ ⊎ ′′|) ≻ (, | ⊎ ′ ⊎ ′′ ⊎ ′ ⊎ ′′|).
By monotonicity,
(, |′ ⊎ ′′′ ⊎ ′′ ⊎ ′′|) ≻ (, | ⊎ ′ ⊎ ′′|), which means that the voters in ′′ have a reason to deviate from
2 = ⟨ ⊎ ′ ⊎ ′′, ′ ⊎ ′′ ⊎ ′′′⟩ This contradicts the assumption that 2 is a stable assignment. □
The proof of Lemma 3 is the only place where we use the assumption of total preferences; Thm. 2 inherits this assumption. We strongly suspect that the assumption of totality could be replaced by an assumption along the lines “only assignments arising during the run of Algorithm 1 are considered”, and so totality would not really be needed. But given that Algorithm 1 is run in two directions and that we rely on contradiction proofs, a-priori excluding some assignments from the reasoning seems complicated.
The Isabelle version looks as follows. The development has around 550 lines of code. lemma twoDirectionsImplyUniqueness : assumes "∀ x. (x=A) = (x̸=B)" and "(∀ v x y. x̸=y →− (x ⪰ y) ∨ y ⪰ x)" and "algo (Suc (card (UNIV::’V set))) A B =
algo (Suc (card (UNIV::’V set))) B A" and "stable f2" shows "algo (Suc (card (UNIV::’V set))) A B = f2"
Theorem 2 is not obvious and while trying to prove it we had doubts whether it actually holds. The Isabelle code for this result corresponds to 25% of our entire Isabelle development.
Stable assignments do not always exist for more than two alternatives: Example 4. Olivier Létofé, a student doing an internship at at Toulouse University in 2022, has found this example: 1 : (, 3) ≻ 1 (, 2) ≻ 1 (, 3) ≻ 1 (, 2) ≻ 1 (, 3) ≻ 1 (, 2)
≻ 1 (, 1) ≻ 1 (, 1) ≻ 1 (, 1) 2 : (, 3) ≻ 2 (, 2) ≻ 2 (, 3) ≻ 2 (, 2) ≻ 2 (, 3) ≻ 2 (, 2)
≻ 2 (, 1) ≻ 2 (, 1) ≻ 2 (, 1) 3 : (, 3) ≻ 3 (, 2) ≻ 3 (, 3) ≻ 3 (, 2) ≻ 3 (, 3) ≻ 3 (, 2)
≻ 3 (, 1) ≻ 3 (, 1) ≻ 3 (, 1)
Starting in (, 3), we turn in circles. No stable assignment exists. Independently, [
Generalising the work to more than two alternatives is the obvious direction for future work: under which conditions does a stable assignment exist, and which algorithm can find it?
In [
Another interesting issue for future work is strategy-proofness, i.e., immunity to false reporting of preferences.
During the above-mentioned internship, some implementation work was done using Coq
rather than Isabelle/HOL. We found this implementation less natural, i.e., less close to the
source [
Relatively little work has been done on applications of proof assistants to game theory. To the
best of our knowledge, no work on formalising the framework of [