A theory library is a collection of theories, theory interpretations, and theory constituents (e.g., definitions and theorems) which serves as a database of mathematics. The basic unit of a theory library is a section; each section is a body of mathematics. Each section consists of a sequence of def-form specifications which are stored in a set of text files.
The IMPS initial theory library contains a large variety of basic mathematics. It is intended to provide you with a starting point for building your own theory library. It also is a source of examples that illustrates some of the diverse ways mathematics can be formulated in IMPS.
This chapter contains only a sampling of the sections that are contained in the IMPS initial theory library with a partial description of each section. Some of the descriptions contain a listing of the theories and some of the more important theorems and definitions included in that section.
Each section description begins with the symbol § followed by the section name. Each theory description begins with the symbol ¶ followed by the theory name.
The main theory of this section is normed-spaces. The section develops the basic notions of calculus (e.g., the derivative and the integral) in the context of normed spaces.
This section has a proof of the Banach contractive mapping fixed point theorem, which states that any contractive mapping on a complete metric space has a unique fixed point.
This section introduces the basic notions of cardinality. It also proves some basic theorems about finite cardinality such as the fact that every subset of a finite set is itself finite.
The main theory of this section is fields. The section develops the machinery of field theory sufficiently for installing an algebraic processor for simplification.
This section contains two principle theories: groups and group-actions. The section includes a proof that the quotient of a group by a normal subgroup is itself a group. Also, several interpretations of group-actions in groups are defined.
This section contains the theories monoid-theory and commutative-monoid-theory. In monoid-theory a constant monoid%prod is defined recursively as the iterated product of the primitive monoid operation. Basic properties of this constant are proved in monoid-theory and then are transported to theories with their own iterated product operators, such as h-o-real-arithmetic with the operators and .
Binary relations are represented in this section as certain partial functions in the same way that sets are represented as indicators. Several basic operations on binary relations are formalized as quasi-constructors. As an exercise, the transitive closure of the union of two equivalence relations is shown to be an equivalence relation.
This section proves the combinatorial identity and the binomial theorem for fields.
This section contains a proof of the fundamental counting theorem for group theory. Several consequences of this theorem are proved including Lagrange's theorem.
This section is always loaded with IMPS. It contains the theory h-o-real-arithmetic and a number of definitions, theorems, and macetes in this theory. It also adds a number of definitions and theorems in the ``generic theories'' named generic-theory-1, generic-theory-2, generic-theory-3 and generic-theory-4 and the theory indicators.
This section interprets monoid-theory in groups and then proves the telescoping product formula.
The main interest of this section is the statement and proof of the Knaster fixed point theorem which states that on a complete partial order with a least element and a greatest element, any monotone mapping has a fixed point. One important application of this result included in this section is a proof of the Schröder-Bernstein theorem.
metric-spaces is the only new theory included in this section.
Contains h-o-real-arithmetic as a component theory.
This section introduces the theory metric-space-pairs.
This theory is defined by the theory ensemble mechanism. Alternatively, it can be described as follows:
This section develops continuity and related notions in the context of metric spaces.
This section develops the rudiments of number theory. The fundamental theorem of arithmetic and the infinity of primes are proved.
A pair of elements a,b of sort is represented as a function whose domain equals the singleton set . The basic operations on pairs are formalized as quasi-constructors.
This section contains the following theories:
Two IMPS theories of the real numbers are included in the pre-reals section:
In this theory, the real numbers are specified as a complete ordered field and the rational numbers and integers are specified as substructures of the real numbers. Exponentiation to an integer power is a defined constant denoting a partial function.
This is another axiomatization of the real numbers which we consider to be our working theory of the real numbers. The axioms of h-o-real-arithmetic include the axioms of complete-ordered-field, formulas characterizing exponentiation as a primitive constant and formulas which are theorems proven in complete-ordered-field. These theorems are needed for installing an algebraic processor and for utilizing the definedness machinery of the simplifier. The proofs of these theorems in the theory complete-ordered-field require a large number of intermediate results with little independent interest. The use of two equivalent axiomatizations frees our working theory of the reals from the burden of recording these uninteresting results.
The theory h-o-real-arithmetic is equipped with routines for simplifying arithmetic expressions and rational linear inequalities. These routines allow the system to perform a great deal of low-level reasoning without user intervention. The theory contains several defined entities; e.g., the natural numbers are a defined sort and the higher-order operators and are defined recursively.
h-o-real-arithmetic is a useful building block for more specific theories. If a theory has h-o-real-arithmetic as a subtheory, the theory can be developed with the help of a large portion of basic, everyday mathematics. For example, in a theory of graphs which includes h-o-real-arithmetic, one could introduce the concept of a weighted graph in which nodes or edges are assigned real numbers. We imagine that h-o-real-arithmetic will be a subtheory of most theories formulated in IMPS.
Sequences over a sort are represented as partial functions from the natural numbers to . Lists are identified with sequences whose domain is a finite initial segment of the natural numbers. The basic operations on sequences and lists, including nil, car, cdr, cons, and append are formalized as quasi-constructors.