Metamathematics

enUK

metamathematics

[¦med·ə‚math·ə′mad·iks] (mathematics) The study of the principles of deductive logic as they are used in mathematical logic.

Metamathematics

(proof theory), in the broad sense of the term, the metatheory of mathematics that assumes no special limitations on the nature of the metatheoretical methods that can be used, on the method of presentation or on the domain of the “mathematics” investigated in metamathematics.

A more specialized understanding of the term “metamathematics,” stemming from D. Hilbert, is more widespread and is historically earlier (as metamathematics in general was the first example of a “metascience”). The discovery of paradoxes (antinomies) in logic and set theory at the beginning of the 20th century introduced the problem of reconstructing the foundations of mathematics and logic on a new basis that would exclude any contradictions. To achieve this, the program of logicism sought to “reduce” mathematics to logic by means of the axiomatic method. However, independently of the success of such a “reduction” in the reconstructed mathematics (or the logic underlying mathemtics), the absence of known antinomies and the impossibility of new ones arising can be guaranteed only by the consistency proof.

The proponents of mathematical intuitionism proposed a radical reexamination of the content of the concept of mathematics itself such that the abstractions of classical mathematics (as, for example, the abstraction of actual infinity) giving rise to antinomies (or only suspected of doing so) would forever be expelled from it. Hilbert’s mathematical formalism denied the logicist illusions regarding the possibility of providing a foundation for mathematics by reducing it to logic, on the one hand, but decisively did not share the intuitionist skepticism regarding the possibilities of a logically satisfactory axiomatic construction of mathematics, on the other. Hilbert, while accepting much of the intuitionist criticism of traditional classical mathematics, nevertheless sought to “rehabilitate” the axiomatic approach. “No one can drive us from the paradise that Cantor created for us,” Hilbert stated. This above all necessitated a consistent formalization of the mathematical theories underlying foundations of mathematical theories (axiomatic set theory, axiomatic arithmetic), that is, the representation of the theories in the form of calculi (formal systems). A number of concepts in these calculi were to be defined “purely formally,” these being the concepts of an axiom (formulas of a particular form), derivation (sequence of formulas each of which is obtained from preceding formulas according to strictly defined rules of inference), proof (inference from axioms), and theorem (a formula that is the final formula of a given proof). Then, by making use of certain “completely objective” and “one-hundred percent reliable” contensive methods of reasoning, one must show the unprovability of a contra-diction in the given formal theory, that is, the impossibility of a situation in which both a given formula and its negation would turn out to be theorems of the theory.

The set of such “objective” and “reliable” (in any case, invulnerable to intuitionist criticism) methods should constitute metamathematics (theory of mathematical proof). Hilbert characterized as finitism the complex of limitations imposed on the methods admissible in metamathematics. This “finitistic approach” prohibits, in a more radical way than intuitionism, the use of any “metaphysical” premises regarding infinite sets. Such important metatheoretical results as Gödel ’s completeness theorem for the predicate calculus and the theorem of L. Lowenheim and T. Skolem on the satisfiability of any consistent theory in the domain of natural numbers do not satisfy these limitations, since the concept of the universal validity of a formula of the predicate calculus used in them is defined by means of a “nonfinitary” concept of the “set of all possible interpretations.” Thus, these metatheorems, strictly speaking, do not belong to metamathematics and are therefore often said to belong to metalogic or to what is called set-theoretic predicate logic.

However, (meta)theorems on the consistency of the propositional calculus and predicate calculus have been successfully obtained on the basis of a finitistic standpoint, that is, in a strictly metamathematical fashion. Hilbert’s program in its complete form nevertheless proved to be unrealizable. Gödel showed (1931) that no consistent formalization of mathematics could encompass all of classical mathematics (or even all formal arithmetic) and that so-called undecidable formulas will be necessarily found in it, that is, formulas that can be expressed in the formalized language but are neither provable nor disprovable within it (yet are nevertheless intuitively true). A formula that asserts its own unprovability is an example of such a formula. Gödel was able to specify a formula with such a seemingly paradoxical interpretation by using an ingenious method he devised—his system of arithmetic coding (Gödel numeration) of the symbols, formulas, and sequences of formulas of a formal system that uniquely assigns to every element of the system a Gödel number. Owing to such an “arithmetization of syntax,” Gödel was able to represent not only predicates of a given formal system but also related metamathematical predicates (such as “is a formula,” “is a proof,” “is a theorem”) by means of certain arithmetic predicates. The statement of what is now known as Gödel’s first theorem is then proved using reasoning remarkably similar to Richard’s paradox and in general to Liar-type paradoxes (“I am lying”) and variants of Russell’s antinomy (a village barber who shaves all those and only those villagers who do not shave themselves and so on). A corollary of this theorem is Gödel’s second theorem, according to which the consistency of any consistent formal system of the arithmetic of natural numbers cannot be proved by means that are formalizable in this system.

In these theorems, one speaks of not only the properties of a given formal system but also of some particular metamathematical properties, so that they are not even metatheorems but, strictly speaking, metametatheorems. The unrealizability of Hilbert’s finitistic program stems from these theorems. Not only all of mathematics but even the arithmetic of natural numbers does not allow formalization that would be both complete and consistent. Moreover, the entire apparatus of finitism is expressible by the methods of intuitionist arithmetic, from which by virtue of Gödel’s second theorem there follows the impossibility of a finitistic proof of the consistency of arithmetic. (An additional fundamental result in metamathematics is Church’s theorem on the undecidability of arithmetic and the predicate calculus, according to which there does not exist an algorithm for recognizing provability for formulas of the corresponding calculi.)

In some sense, Gödel’s theorems can be understood as the “end of metamathematics.” However, while attesting to the limitations of finitism, formalism, and the related Hilbert program, as well as to the axiomatic method as a whole, these theorems at the same time have served as a powerful stimulus to the search for methods of proof (in particular, consistency proofs) that are stronger than finatary ones but that are in some sense constructive. One such method is that of transfinite induction to the first constructively inaccessible ordinal number. This method has been used to obtain a proof of the consistency of arithmetic by G. Gentzen, W. Ackermann, P. S. Novikov, K. Schiitte, and P. Lorenzen. Another example is the ultraintuitionist program in the foundations of mathematics, which has made it possible to obtain an absolute (not using reductions to any other system) proof of consistency of the Zermelo-Fraenkel set-theoretic system of axioms.

REFERENCES

Hilbert, D. Osnovaniia geometrü. Moscow-Leningrad, 1948. Appendices 6–10. (Translated from German).
Kleene, S. C. Vvedenie v metamatematiku. Moscow, 1957. (Translated from English.)
Kleene, S. C. Matematicheskaia logika. Moscow, 1973. (Translated from English.)
Curry, H. B. Osnovaniia matematicheskoi logiki. Moscow, 1969. Chapters 2–3. (Translated from English.)
Gentzen, G. “Neprotivorechivosf chistoi teorii chisel.” In Matematicheskaia teoriia logicheskogo vyvoda. Moscow, 1967. Pages 77–153. (Translated from German.)
Nagel, E., and J. von Neumann. Teorema Gedelia. Moscow, 1970. (Translated from English.)
Tarski, A. Vvedenie v logiku i metodologiiu deduktivnykh nauk. Moscow, 1948. (Translated from English.)
Gödel, K. “Über formal unent scheidbare Sätze der Principia Mathematica und verwander System, I.” Monatshefte Mathematic Physik, 1931, vol. 38, pp. 173–98.
Rosser, B. “Extensions of Some Theorems of Gödel and Church.” Journal of Symbolic Logic, 1936, vol. 1, no. 3.
Tarski, A. Logic, Semantics, Metamathematics. Oxford, 1936.

IU. A. GASTEV

metamathematics