cl-banner

Formal Microeconomic Foundations and the First Welfare Theorem

Julian Parsert, Cezary Kaliszyk

7th ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP 2018), pp. 91-101, 2018.

Abstract

Economic activity has always been a fundamental part of society. With recent social and political changes economics has gained even more influence on our lives. In this paper we formalize two economic models in Isabelle/HOL: the pure exchange economy, where the only economic actors are consumers, as well as a version of the Arrow-Debreu Model, a private ownership economy, which includes production facilities. Interestingly, the definitions of various components of the economic models differ in the economic literature. We therefore show the equivalences and implications between various presentations, which allows us to create an extensible foundation for formalizing microeconomics and game theory compatible with multiple economic theories. We prove the First Theorem of Welfare Economics in both economic models. 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. The formal proofs allow us to find more precise assumptions than those found in the economic literature.

 

  PDF |    doi:10.1145/3167100  

BibTeX 

@inproceedings{JPKC_CPP_2018,
author = {Parsert, Julian and Kaliszyk, Cezary},
title = {Formal Microeconomic Foundations and the First Welfare Theorem},
booktitle = {Proceedings of the 7th ACM SIGPLAN International Conference on
Certified Programs and Proofs},
series = {CPP 2018},
year = {2018},
pages = {91--101},
doi = {10.1145/3167100},
publisher = {ACM}
}
Nach oben scrollen