In Which Form do Foundations of Mathematics Exist?
by
Svyatoslav Lavrov
Institute of Applied Astronomy RAS

In 1972, when I studied mathematical logic more thoroughly than before, I was impressed by the fact that metamathematics (foundations of mathematics, Grundlagen der Mathematik) has no formal model. Therefore an appropriately restricted natural language should be used to build an informal one.

As a result many deep mathematical notions have no strong sense or even no sense at all. Among them are the consistency of any advanced theory (e. g., ZF), the correctness of a nontrivial algorithm, the diagonal method as a general tool of proving the unsolvability of a decision problem etc.

There were attempts to improve the situation, mainly by constructing various abstract machines. A. A. Markov in the precomputer era proposed such a machine with a rather flexible structure and a high level language. It was an essential step forward.

The action of any machine may be described in its own language. This creates an illusion of a rather full formalization. Still it is quite impossible to exclude the natural language from the description.

I have to accept that logicians whome I happened to discuss this matter with reject my position more or less strongly. However, each of them has his own objection. No two of them coincide. It leaves me some hope that I may be right.

Bibliography

[]

Lavrov S. S. On the Relationship of Programming and Mathematics (in Russian) / ``Programmirovanie'', 2001, N 6, pp. 3-12. There exists an English translation.

Date received: June 10, 2003