HomePage RecentChanges

Terms, Definitions, and Systems of Axioms

Introduction

The basic unit of mathematical writing is the mathematical term or symbol. Mathematical expressions, formulas, statements, and the like are formed by combining these terms according to a suitable syntax.

Mathematcal terms may be seen as standing for various concepts. The way in which this meaning is assigned is implicit. By themselves, the terms have no meaning; whatever meaning they might have arises from the axioms and rules of inference in which the terms occur. This also means that the meanings of terms are interdependant. For more thoughts on this point of view, see Linguistic analysis of mathematics, by Arthur F. Bentley.

The way mathematics works may be formalized in the notion of an axiomatic system. To specify an axiomatic system, one needs to specify three items, the primitive terms, the axioms, and the rules of inference. Starting with the axioms, one proves theorems using the rules of inference.

While this is a pretty good description of how mathematicians work, it can be too static. In addition to proving theorems within a given axiomatic system, mathematicians also define new terms and rules of inference from time to time. Strictly speaking, adding new terms and rules of inference changes the axiomatic system. Since this is a common practise in mathematics, any computer system which is supposed to reflect the practise of mathematicians should be able to deal with this process. Therefore, we will consider how and when it is legitimate to add new terms to a theory here. We will deal with adding rules of inference elsewhere.

General Theory

One may formulate a general principle which explains under what circumstances it is legitimate to add terms to a theory. This principle states that one can add a set of new terms to the list of primitive terms and a set of statements which serve to define the meaning of these terms to the axioms provided that any theorem whose statement does not involves the new terms can be proven using the new terms and their defining statements only if it could be proven without them.

This principle explains the practise one occasionally sees of accompanying definitions of new terms with proofs that they are well-defined. These proofs can be seen as demonstrations that the new terms and their defining statements meet the criterion ennunciated above.

There are a few simple ways in which one can introduce terms. As will be seen, these can be seen as simple instances of the general principle.

Replacement Definitions

The simplest way to introduce a new term is by defining it to stand for a replacement text. Any occurrences of the term can be replaced with the replacement text. For example, one could make the difinition "a right triangle is a triangle with a right angle". Then, wherever the term "right traingle" appears, one could replace it with the phrase "traingle with a right angle".

This is what is considered a definition in the popular sense of the term. It is also rather trivial to understand it in terms of the general principle. Since any occurrence of the new term in a proof can be replaced by the replacement text, any statement which can be proven using the new term could also be proved without using it.

Existential Generalization

Another common procedure for introducing new terms is existential generalization. If one can prove a statement of the form ⌈(exists (x) (P x))⌉, and a term "y" which has not appeared in any axiom or rule of inference, one may then add ⌈(P y)⌉ to the list of axioms.

The justification for this procedure in terms of the general rule is as follows. Suppose that term "y" appears in a statement ⌈S⌉ in a proof. Replace ⌈S⌉ by ⌈(forall (y) (if (P y) S)⌉. One can show that the new proof obtained by this procedure is valid provided that the old proof was valid and that ⌈(exists (x) (P x))⌉ is true. To show this metatheorem, one examines the various rules of inference and shows that they are still valid after this transformation provided that ⌈(exists (x) (P x))⌉ is true.

Universal Specialization

Here one starts with a proposition in which there appears a term which has not been used in any axiom or rule of inference. One then quantifies over this term using a universal quantifier.

Discussion

See http://www.earlham.edu/~peters/writing/psa/ for some general talk about self-amendment. --jcorneli