Tags:Economics, Expected Utility, formal proof, Game Theory, Isabelle, Utility Theory and Von Neumann-Morgenstern Utility Theorem

Abstract:

Utility functions form an essential part of game theory and theoretical 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 a formal proof of the existence of linear utility functions. Furthermore, we consider the von-Neumann-Morgenstern Utility Theorem, its importance for game theory and economics, and a formalization thereof. The formalization includes precise 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.

Towards Formal Foundations for Game Theory (Short Paper)