### Abstract

Utility functions form an essential part of game theory and economics. In order to guarantee the existence of utility functions most of the time sufficient properties are assumed in an axiomatic manner. One famous and very common set of such assumptions is that of expected utility theory. Here, the rationality, continuity, and independence of preferences is assumed. The von-Neumann-Morgenstern Utility theorem shows that these assumptions are necessary and sufficient for an expected utility function to exists. This theorem was proven by Neumann and Morgenstern in “Theory of Games and Economic Behavior” which is regarded as one of the most influential works in game theory. The formalization includes formal definitions of the underlying concepts including continuity and independence of preferences.

### License

GNU Lesser General Public License (LGPL)

### Topics

- Mathematics/Games and economics

### Session Neumann_Morgenstern_Utility

- PMF_Composition
- Lotteries
- Neumann_Morgenstern_Utility_Theorem
- Expected_Utility

### Depends on

- Microeconomics and the First Welfare Theorem

### Auto-related entries

- Arrow and Gibbard-Satterthwaite

## Cite

×

Neumann_Morgenstern_Utility-AFP

    @article{Neumann_Morgenstern_Utility-AFP,
      author  = {Julian Parsert and Cezary Kaliszyk},
      title   = {Von-Neumann-Morgenstern Utility Theorem},
      journal = {Archive of Formal Proofs},
      month   = {July},
      year    = {2018},
      note    = {\url{https://isa-afp.org/entries/Neumann_Morgenstern_Utility.html},
                 Formal proof development},
      ISSN    = {2150-914x},
    }

Download

## Download

× Download latest

Older releases:

- Sep 13, 2023 : Isabelle2023
- Oct 27, 2022 : Isabelle2022
- Dec 14, 2021 : Isabelle2021-1
- Feb 23, 2021 : Isabelle2021
- Apr 20, 2020 : Isabelle2020
- Jun 11, 2019 : Isabelle2019
- Aug 16, 2018 : Isabelle2018
- Jul 4, 2018 : Isabelle2017