[FOM] Class Abstractions are a Natural Way for Representation of Mathematical Theories

[Victor Makarov]

Dear FOMers:

Below is an excerpt from my draft paper "Predicat Logic with Classes:
A Natural Approach to Practical Formalization of Mathematics".
The paper (8 pages) is available from the author.

Victor Makarov,   vmakarov at acm.org         or      ViktorMakarov at hotmail.com
---------

It is now a well established view[1, p.215], that any mathematical theory T
is an extension of ZFC set theory  by adding to ZFC a finite number of new
constants c_1, ..., c_k and an axiom A(c_1, ..., c_k), (k >= 1),
implicitly defining these constants.

In CL, the theory T can be introduced by using the following theory 
definition:

        T := {c_1, ..., c_k | A(c_1, ..., c_k)}

That is, mathematical theories in CL are represented as class abstractions
(see an example below).

Any element of the class T, that is, any tuple (z_1, ..., z_k), where z_1, 
... , z_k
are some terms of the first-order theory ZFC such that the formula A(z_1, 
... , z_k)
is a theorem of ZFC, is called model of the theory T.

Note that this notion of model is different from the notion of model used in 
model theory,
it is actually the notion of model [2, p. 190], which has been used in 
mathematics well
before the emergence of  model theory.

Suppose, that P is a theorem of T and z is a model of T. Let us replace, in 
the formula
P, each constant c_i with z_i, (i = 1, ... ,k). As well known[?], the 
resulting formula
will be again a theorem (of the host theory, ZFC).

In CL, the corresponding inference rule can be written as follows:

    (z \in d,  P) => S[d, P, z]

where d is a syntactic variable for class abstractions,
S[d, P, z] is a notation for substitution used in CL.

A theory definition is a special case of the syntactic construct 
"definition", which, in
the general case, has the  form

                        T_1 :: M := K

where T_1 is a previously introduced theory, K is a term or a formula
of the theory T_1, M is the name of K. The theory T_1 is the host of M.

If T_1 is the root theory (like ZFC), then T_1 can be omitted.
(The `::'- notation was borrowed from the object-oriented programming 
language C++ [3] ).

Note, that K can be again a class abstraction. In that case M is the name of 
the theory
represented by the class abstraction K.

The theory definitions are a natural way for formalization of the "little 
theories"
approach [4] and the following  important advantages(comparing to [4]) can 
be mentioned:

1)  There is no need for a special syntactic construct for theory 
interpetations
   (because models can be used instead interpretations);

2)  For introducing "little theories" a standard well-known syntactic 
construct
   is used (class abstractions).


Let us consider the group theory which can be introduced in the following 
way:

              Group := {G, m| A(G,m)}

where G and m are constants, representing,respectively, the carrier set and
the law of composition and the formula A(G,m) is a conjunction of  axioms
of the group theory.

The notion of abelian group could be introduced in the similar way:

      AbelGroup := {G, m| A(G,m) \land Comm(m)\};

where Comm(m) is a formula expressing commutativity of the operation m.

But it can be done in a  better, structured way:

           AbelGroup := Group &  Comm(m)

(see a definition of `&' in section~\ref{CL2}).

                        References

1. J.Dieudonne. A Panorama of Pure Mathematics. New York: Academic Press, 
1982.

2. P.Bernays. Axiomatic Set Theory. New York: Dover Publications, 1991.

3. B. Stroustrap. The Design and Evolution of C++. Addison-Wesley, 1994

4. W. M. Farmer, J .D. Guttman and F. J. Thayer:  Little Theories. in D. 
Kapur, editor,
    Automated deduction --- CADE-11, vol. 607 of Lecture Notes in Computer 
Science,
    pages 567-581. Springer-Verlag, 1992.