The IMPS methodology for formalizing mathematics is based on a particular version of the axiomatic method. The axiomatic method is commonly used both for encoding existing mathematics and for creating new mathematics. A chunk of mathematics is represented as an axiomatic theory consisting of a formal language plus a set of sentences in the language called axioms. The axioms specify the mathematical objects to be studied, and facts about the objects are obtained by reasoning logically from the axioms, that is, by proving theorems.
The axiomatic method comes in two styles, both well established in modern mathematical practice. We refer to them as the ``big theory'' version and the ``little theories'' version. In the ``big theory'' version all reasoning is performed within a single powerful and highly expressive axiomatic theory, such as Zermelo-Fraenkel set theory. The basic idea is that the theory we work in is expressive enough so that any model of it contains all the objects that will be of interest to us, and powerful enough so that theorems about these objects can be proved entirely within this single theory.
In the little theories version, a number of theories are used in the course of developing a portion of mathematics. Different theorems are proved in different theories, depending on the amount and kind of mathematics that is required. Theories are logically linked together by translations called theory interpretations which serve as conduits to pass results from one theory to another. We argue in [10] that this way of organizing mathematics across a network of linked theories is advantageous for managing complex mathematics by means of abstraction and reuse.
IMPS supports both the big theory and little theories versions of the axiomatic method. However, the IMPS little theories machinery of multiple theories and theory interpretations offers the user a rich collection of formalization techniques (described in Chapter 9) that are not easy to imitate in a strict big theory approach.