Predicate Logic with Definitions and the General Concept of Algorithm
by
Victor Makarov
Brooklyn, New York (USA)

Development of more general (and more suitable for applications) precise concepts of algorithm is important both for mathematics and computer science [1, 2, 3]. In [4] the following concept of abstract algorithm was suggested:

Any algorithm is defined in a certain mathematical theory (for example, graph algorithms in the graph theory). That is, the concept of algorithm is inseparable from the concept of mathematical theory and actually is subordinate to it because before the development of an algorithm we should have a mathematical theory. An algorithm is an explicit definition in this theory.

The aim of this paper is to suggest a new (more precise and simple comparing to the author’s previous papers [4, 5]) practical formalism - Predicate Logic with Definitions (or D-logic or simply DL) - for defining mathematical theories and writing definitions inside the theories. DL is a modification of the first-order logic by adding to its main syntactic constructs - terms and formulas - a new syntactic construct, called definition. As an example, we show that the abstract state machines of Gurevich[2] can be naturally represented in DL.

To make the concept of abstract algorithm precise, we at first should have a precise definition of the concept “mathematical theory”. Fortunately, the last century’s work on the foundations of mathematics has provided such a definition [6, p. 215], accepted by the most of mathematicians:

A mathematical theory T is an extension of the first-order theory ZFC (Zermelo-Fraenkel set theory with the axiom of choice) by adding to ZFC a finite number of new constants c_1, … , c_k and an axiom A, implicitly defining these constants.

In DL, the theory T can be defined in the following way:

Let z be any tuple (z_1, …, z_k) where z_1, …, z_k are some terms, and the formula A1 is the result of substitution in the formula A the terms z_1, …, z_k instead of the constants c_1, …, c_k , respectively. The tuple z is called a model of the theory T if the formula A1 is a theorem (note that this definition differs from the definition of model in the model theory).

The rest of the abstract can be read at my webpage: http://home.nyu.edu/ yvm204/vm/DL-alg.htm

The abstract has been also sent to the Programme Committee as a MS Word document (4 pages).

References

[1] A.N. Kolmogorov and V.A. Uspenski. On the definition of algorithm. Uspekhi Mat. Nauk, 13 (1958), 3-28 (Russian).

[2] Yuri Gurevich. Sequential Abstract State Machines Capture Sequential Algorithms. ACM Transactions on Computational Logic, vol. 1, no. 1 (July 2000), pp. 77-111. Also: http://research.microsoft.com/ gurevich/Opera/141.pdf

[3] Yannis N. Moschovakis. What Is an Algorithm? Mathematics Unlimited – 2001 and beyond, ed. by B. Engquist and W. Schmid, Springer, 2001, pp. 919-936. Also see: http://www.math.ucla.edu/ ynm/papers.htm.

[4] Victor Makarov. Towards a theory of abstract algorithms. Nauchno-Technicheskaya Informatsiya, ser. 2, 1982, N9, pp. 35-40 (Russian). Also see: http://home.nyu.edu/ yvm204/vm/vm.htm

[5] Victor Makarov. MSL - A Mathematical Specification Language, in: “Logical Foundations of Computer Science – Tver’92”, Lecture Notes in Computer Science, Vol. 620 (1992), pp. 305-313.

[6] Dieudonne J.A. A Panorama of Pure Mathematics. New York: Academic Press, 1982.

Date received: April 29, 2003