Using Theorema in the Formalization of Theoretical Economics

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 pseudo-code 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.