Abstract

Utility functions form an essential part of game theory and economics. In order to guarantee the existence of these utility functions sufficient properties are assumed in an axiomatic manner. In this paper we discuss these axioms and the von-Neumann-Morgenstern Utility Theorem, which names precise assumptions under which expected utility functions exist. We formalize these results in Isabelle/HOL. The formalization includes formal definitions of the underlying concepts including continuity and independence of preferences. We make the dependencies more precise and highlight some consequences for a formalization of game theory.

BibTeX

@InProceedings{JPCK-ITP18,
  author    = "Julian Parsert and Cezary Kaliszyk",
  title     = "Towards Formal Foundations for Game Theory",
  editor    = "Jeremy Avigad and Assia Mahboubi",
  booktitle = "Proceedings of the 9th International Conference on 
               Interactive Theorem Proving",
  series    = "Lecture Notes in Computer Science",
  volume    = 10895,
  pages     = "495--503",
  year      = 2018,
  doi       = "10.1007/978-3-319-94821-8_29"
}