Towards Formal Foundations for Game Theory

Julian Parsert, Cezary Kaliszyk

Interactive Theorem Proving, Lecture Notes in Computer Science 10895, pp. 495 – 503, 2018.


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.


  PDF |    doi:10.1007/978-3-319-94821-8_29  


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"
Nach oben scrollen