[FOM] Class Abstractions are a Natural Way for Representation of Mathematical Theories
Victor Makarov
viktormakarov at hotmail.com
Wed Mar 9 12:20:05 EST 2005
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.
More information about the FOM
mailing list