Towards Formal Foundations for Game Theory

Utility theory seeks to describe how humans evaluate and compare alternatives or outcomes using mathematical tools. This theory forms the basis of game theory and therefore several fields in economics. Hence, we believe that formalizations in either of those areas require a solid base in utility theory.

In their pioneering work “Theory of Games and Economic Behavior” von Neumann and Morgenstern axiomatically describe, how actors evaluate uncertain outcomes [22]. They developed the theory of expected utility, which describes a scheme based on the expected value of outcomes. Utility functions allow the use of many mathematical tools for optimization etc. Hence, much effort is put into precisely specifying properties which guarantee the existence of such functions. To this end, von Neumann and Morgenstern dedicate the first chapters of [22] to specifying the assumptions necessary (and sufficient) for preference relations to admit expected utility representation. This is now known as the von-Neumann-Morgenstern Utility Theorem. These assumptions are introduced as axioms upon which the entire book is based. Kahneman and others criticized [20] the theory of expected utility and developed alternatives [7]. Moreover, impossibility results were proven [19]. Nevertheless, it still remains the standard theory in game theory [14] and the most common tool in economic reasoning [9].

Our goal is to provide a solid foundation of utility theory upon which further work in both economics and game theory can be conducted. We do so by introducing formal definitions in Isabelle/HOL and deriving results that not only support the intuition of expected utility, but also help automated theorem provers in proving subsequent results. With that we prove the von-Neumann-Morgenstern Expected Utility Theorem.

Related Work. Arrow’s impossibility theorem has been formalized by Wiedijk [25] and Nipkow [13]. Gammie has formalized some results in social choice theory, as well as stable matching [4, 5]. Kuhn’s theorem has been formalized by Vestergaard [21] and generalized by Le Roux [17]. The same author later worked on a formalization of Nash equilibria for two player games [18]. Recently, Martin-Dorel and Soloviev formalized boolean games with non-deterministic aspects. In addition, algorithmic game theory results have been formalized in Coq [1].

The concepts we discuss are also relevant for the formalization of economic concepts. Related work includes the verification of financial systems [16] and binomial pricing models [3]. As part of the ForMaRE project [10] VCG-Auctions [8] have been formalized. In microeconomics we discussed a formalization of two economic models and the First Welfare Theorem [15].

To our knowledge the only work that uses expected utility theory is that of Eberl [2]. The focus there is not the underlying utility theory, but rather its use in social decision schemes. Since our focus is the this underlying theory and in particular the von Neumann-Morgenstern Utility Theorem, we found that there is only little overlap.

Isabelle/HOL [24] is an Interactive Theorem Prover based on higher-order logic. Due to space limitations, we refer the reader to the Isar reference manual [23] for Isabelle’s foundations and notations. We introduce a few reoccurring notions of HOL-Probability, but we refer to [6] for a more detailed explanation.

It is common to denote the composition of probability mass functions (pmfs) p and q with a probability \(\alpha \) as follows \(\alpha \;p + (1-\alpha )\;q\). This notation corresponds to the following Isabelle definition:

In particular, we compose a Bernoulli distribution that returns either True or False with probability a, with a function that returns p if the random variable is True or q otherwise. We use Isabelle’s standard definition for the support of a pmf, set_pmf, while return_pmf applied to x returns a pmf yielding x with the probability 1.

A preference relation is a transitive and reflexive binary relation (i.e. a preorder). The notations \(x \succeq y\), \(x\ {\succeq }[R]\ y\), and R(x, y) are equivalent and denote a preference relation where x is weakly preferred to y. Despite its potential ambiguity, we will be using the first alternative if the specific relation can be inferred from context. Similarly, the symbols \(x \succ y\) and \(x\ {\succ }[R]\ y\) denote the strict preference relation where \(x \succ y\) iff \(x \succeq y \wedge \lnot y \succeq x\), whereas \(x \approx y\) and \(x\ {\approx }[R]\ y\) denote the indifference relation where \(x \approx y\) iff \(x \succeq y \wedge y \succeq x\).

We will use the terms “pmf” and “lottery” interchangeably. In economic and game theoretic literature the latter is more common, while the former is used in probability theory and Isabelle/HOL.

We present and discuss important definitions which we will use in subsequent sections.

First we briefly introduce rational preferences and Utility functions. However, since both have been thoroughly discussed and formalized in the authors’ previous work [15] we will not go into detail or mention results involving these.

We refer to [15] or the sources for a more detailed account of the Definitions 1 and 2 as well as derived results.

Based on these two definitions we continue with the new additions. Firstly, we consider continuous preferences. Definition 3 is sometimes also called the Archimedean axiom.

Intuitively this means that if \(p \succ q\), then lotteries that are close to p are also preferred to q. An alternative interpretation would be, that if preferences are continuous, there are no outcomes that are so bad (not preferred with respect to R) that no probability is small enough to “redeem” them by composing with a better alternative.

Next, we define independence of preferences. Informally, we want independence to entail that the (preference) relation between two elements p and q only depends on the parts where p and q differ.

Independence implies that the relation between \(\alpha \;p + (1-\alpha )\;x\) and \(\alpha \;q + (1-\alpha )\;x\) only depends on the relation of p and q rather than their combination with x.

Notice that Definition 5 introduces two kinds of utility functions, the expected utility function \(\mathcal {U}\) and the Bernoulli utility function u. The function \(\mathcal {U}\) assigns a utility value to lotteries/pmfs that range over outcomes, while u assigns a utility value to outcomes themselves. The utility of a lottery p which equals \(\mathcal {U}(p)\) is then defined to be the expected value of the utility function u with the lottery p.

In this section we introduce notations that we use and discuss further concepts and assumptions.

First, we assume the set of outcomes \(\mathcal {O}\) to be a non-empty finite set³. Next, we define the carrier set \(\mathcal {P}\) to be the set of all probability mass functions (pmf) over the finite set of outcomes \(\mathcal {O}\), \(\mathcal {P}:= \{l \mid support \;l \subseteq \mathcal {O}\}\). This set can be visualized using a probability simplex. Figure 1 shows such a simplex with three outcomes. Note, that if \(| \mathcal {O}|>1\) then the set P is uncountable. Now, we can define degenerate lotteries to be all lotteries that yield one outcome with the probability 1. In Fig. 1 these are simply the corner points (i.e., the points \(\mathcal {O}\) \(_{1-3}\)). A rational preference relation over \(\mathcal {P}\) is denoted with \(\mathcal {R}\). Since the final result requires \(\mathcal {R}\) to be continuous and independent (cf. Definitions 3 and 4) most literature assumes these from the get go. We found that not all assumptions were necessary for the results. Therefore, in the formalization we chose to introduce assumptions only when necessary. Nevertheless, for the sake of readability we assume \(\mathcal {R}\) to be rational (1), continuous (3), and independent (4) in the subsequent sections. For more detail on the necessity of assumptions we refer to the formalization.

With this setup, we can state the theorem we are aiming for, the von-Neumann-Morgenstern Utility Theorem (Theorem 1).

We will present the key insights and ideas leading to a proof of Theorem 1. All the definitions and proofs can be found in the formalization. Since we use the setup introduced in the previous section all assumptions and notations carry over. In particular \(\succeq \) will denote the previously introduced relation \(\mathcal {R}\).

Theorem 1 is proved by showing two implications. Both directions can be found in the formalization. However, we will discuss the more difficult direction. That is, a preference relation satisfying (1), (3), and (4) admits expected utility representation.

The set of degenerate lotteries is finite, trivially there exists at least one most preferred element (with respect to \(\mathcal {R}\)). Moreover, we can prove Lemma 1.

The same can be shown for the worst (least preferred) elements. Thus proving that there exists at least one best \(\mathcal {B}\) and one worst \(\mathcal {W}\) element in \(\mathcal {P}\) such thatIf \(\mathcal {B}\approx \mathcal {W}\) any constant function would represent the preference relation \(\mathcal {R}\), thus proving Theorem 1 for this special case. Hence, we will assume \(\mathcal {B}\succ \mathcal {W}\).

From the assumption of continuity and Property 1, we know that \(\forall p \in \mathcal {P}\),Moreover, we can show that such an \(\alpha \) is unique. If it was not, we could create two distinct lotteries \(p = \alpha \;\mathcal {B} + (1-\alpha )\;\mathcal {W}\) and \(q=\beta \;\mathcal {B} + (1-\beta )\;\mathcal {W}\) with \(\alpha > \beta \) and \(p \approx q\). However, since \(\mathcal {B}\succ \mathcal {W}\) and p has a higher chance of the best outcome than q, we deduce \(p \succ q\), a contradiction. This shows that for all lotteries \(p \in \mathcal {P}\), there exists a unique calibration probability \(\alpha \), such that, \(\alpha \mathcal {B}+ (1-\alpha ) \mathcal {W}\approx p\).

The key idea is to define a function that assigns the unique calibration probability to every lottery in \(\mathcal {P}\). This is realised with the utility function util. Given a pmf p its unique calibration \(\alpha \) is obtained (using the indefinite choice operator SOME) and returned.

The next lemma shows that util indeed is a utility function as per Definition 2.

Lemma 2 is already an important result. However, since we are not only interested in general utility functions, but utility functions that adhere to expected utility form (Definition 5), we also need to prove the following Lemma.

One of the most prominent modern books on game theory [11] defines von-Neumann-Morgenstern utility functions simply as linear functions which util indeed is (Lemma 3). Since linearity is the defining property of expected utility functions Lemma 4 can be proven. Note, that util has the wrong type \('\alpha \ pmf \Rightarrow real\). Therefore, we simply define the Bernoulli utility function u with the following lambda abstraction \((\lambda x.\ {{\texttt {util}}}({{\texttt {return\_pmf}}}\ x))\) of type \('\alpha \Rightarrow real\).

This shows the existence of an expected utility function assuming (1), (3), and (4), thus proving one direction of Theorem 1.

As mentioned in Sect. 1 multiple prominent books including [11, 22], introduce the theory of expected utility as a set of axioms upon which their work is based. Thus, a formalization of utility theory is crucial for further development in game theory and economics. The presented formalization amounts to almost 2400 lines of code including over 120 lemmas. These can be used for future work such as Nash’s theorem [12] on the existence of mixed strategy equilibria.