### Abstract

Economic activity has always been a fundamental part of society. Due to modern day politics, economic theory has gained even more influence on our lives. Thus we want models and theories to be as precise as possible. This can be achieved using certification with the help of formal proof technology. Hence we will use Isabelle/HOL to construct two economic models, that of the the pure exchange economy and a version of the Arrow-Debreu Model. We will prove that the First Theorem of Welfare Economics holds within both. The theorem is the mathematical formulation of Adam Smith's famous invisible hand and states that a group of self-interested and rational actors will eventually achieve an efficient allocation of goods and services.

### License

GNU Lesser General Public License (LGPL)

### History

June 17, 2018
  Added some lemmas and a theory file, also introduced Microeconomics folder.

### Topics

- Mathematics/Games and economics

### Session First_Welfare_Theorem

- Syntax
- Argmax
- Preferences
- Utility_Functions
- Consumers
- Common
- Exchange_Economy
- Private_Ownership_Economy
- Arrow_Debreu_Model

### Used by

- Von-Neumann-Morgenstern Utility Theorem

## Cite

×

First_Welfare_Theorem-AFP

    @article{First_Welfare_Theorem-AFP,
      author  = {Julian Parsert and Cezary Kaliszyk},
      title   = {Microeconomics and the First Welfare Theorem},
      journal = {Archive of Formal Proofs},
      month   = {September},
      year    = {2017},
      note    = {\url{https://isa-afp.org/entries/First_Welfare_Theorem.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 18, 2020 : Isabelle2020
- Jun 11, 2019 : Isabelle2019
- Aug 16, 2018 : Isabelle2018
- Oct 10, 2017 : Isabelle2017
- Sep 5, 2017 : Isabelle2016-1
- Sep 4, 2017 : Isabelle2016-1