Using Theorema in the Formalization of Theoretical Economics
Using Theorema in the Formalization of Theoretical Economics
复制标题
在理论经济学的形式化中使用定理
DOI：
--
复制
发表时间：
2011
期刊：
影响因子：
--
通讯作者：
W. Windsteiger
中科院分区：
文献类型：
--
作者：
Manfred Kerber;C. Rowat;W. Windsteiger
理论经济学使用严格的数学方法。例如，冯·诺依曼和摩根斯坦引入的游戏允许对某些公理化的经济情况进行正式的数学证明。这样的证明--至少在原则上--也可以在形式系统中进行，比如定理。在本文中，我们描述了使用Theorema系统进行的实验，以证明有关称为掠夺游戏的特定形式的游戏的定理。每一场掠夺游戏都形成了对权力的特定理解。然后，分析试图推导解集的性质（特别是核心和稳定集），询问解集的存在性、唯一性和特征。
具体地说，我们使用定理显示先前证明的文件上的两个合作者的掠夺游戏与三个代理的属性。特别令人感兴趣的是一些伪代码，它总结了前面显示的结果。由于计算涉及无限集合，因此伪代码在几个方面是非计算性的。然而，在适当引理的存在下，伪代码具有足够的计算内容，Theorema可以计算稳定集（总是有限的）。我们已经具体地证明了这三个不同的重要的权力职能。
Theoretical economics makes use of strict mathematical methods. For instance, games as introduced by von Neumann and Morgenstern allow for formal mathematical proofs for certain axiomatized economical situations. Such proofs can--at least in principle--also be carried through in formal systems such as Theorema. In this paper we describe experiments carried through using the Theorema system to prove theorems about a particular form of games called pillage games. Each pillage game formalizes a particular understanding of power. Analysis then attempts to derive the properties of solution sets (in particular, the core and stable set), asking about existence, uniqueness and characterization.
Concretely we use Theorema to show properties previously proved on paper by two of the co-authors for pillage games with three agents. Of particular interest is some pseudo-code which summarizes the results previously shown. Since the computation involves infinite sets the pseudocode is in several ways non-computational. However, in the presence of appropriate lemmas, the pseudo-code has sufficient computational content that Theorema can compute stable sets (which are always finite). We have concretely demonstrated this for three different important power functions.