Copyright © 1999 Massachusetts Institute of Technology
Formal systems or theories must satisfy requirements that are sharper than those imposed on the structure of theories by the axiomatic-deductive method, which can be traced back to Euclid's Elements. The crucial additional requirement is the regimentation of inferential steps in proofs: not only axioms have to be given in advance, but also the logical rules representing argumentative steps. To avoid a regress in the definition of proof and to achieve intersubjectivity on a minimal basis, the rules are to be "mechanical" and must take into account only the syntactic form of statements. Thus, to exclude any ambiguity, a precise symbolic language is needed and a logical calculus. Both the concept of a "formula" (i.e., statement in the symbolic language) and that of a "rule" (i.e., inference step in the logical calculus) have to be effective; by the Church-Turing Thesis, this means they have to be recursive.
FREGE (1879) presented a symbolic language (with relations and quantifiers) together with an adequate logical calculus, thus providing the means for the completely formal representation of mathematical proofs. The Fregean framework was basic for the later development of mathematical logic; it influenced the work of Whitehead and Russell that culminated in Principia Mathematica. The next crucial step was taken most vigorously by Hilbert; he built on Whitehead and Russell's work and used an appropriate framework for the development of parts of mathematics, but took it also as an object of mathematical investigation. The latter metamathematical perspective proved to be extremely important. Clearly, in a less rigorous way it goes back to the investigations concerning non-Euclidean geometry and Hilbert's own early work (1899) on independence questions in geometry.
Hilbert's emphasis on the mathematical investigation of formal systems really marked the beginning of mathematical logic. In the lectures (1918), prepared in collaboration with Paul Bernays, he isolated the language of first order logic as the central language (together with an informal semantics) and developed a suitable logical calculus. Central questions were raised and partially answered; they concerned the completeness, consistency, and decidability of such systems and are still central in mathematical logic and other fields, where formal systems are being explored. Some important results will be presented paradigmatically; for a real impression of the richness and depth of the subject readers have to turn to (classical) textbooks or to up-to-date handbooks (see Further Readings.)
Completeness has been used in a number of different senses, from the quasi-empirical completeness of Zermelo Fraenkel set theory (being sufficient for the formal development of mathematics) to the syntactic completeness of formal theories (shown to be impossible by Gödel's First Theorem for theories containing a modicum of number theory). For logic the central concept is, however, Semantic completeness: a calculus is (semantically) complete, if it allows to prove all statements that are true in all interpretations (models) of the system. In sentential logic these statements are the tautologies; for that logic Hilbert and Bernays (1918) and Post (1921) proved the completeness of appropriate calculi; for first order logic completeness was established by Gödel (1930). Completeness expresses obviously the adequacy of a calculus to capture all logical consequences and entails almost immediately the logic's compactness: if every finite subset of a system has a model, so does the system. Ironically, this immediate consequence of its adequacy is at the root of real inadequacies of first order logic: the existence of nonstandard models for arithmetic and the inexpressibility of important concepts (like "finite," "well-order"). The relativity of "being countable" (leading to the so-called Skolem paradox) is a direct consequence of the proof of the completeness theorem.
Relative consistency proofs were obtained in geometry by semantic arguments: given a model of Euclidean geometry one can define a Euclidean model of, say, hyperbolic geometry; thus, if an inconsistency could be found in hyperbolic geometry it could also be found in Euclidean geometry. Hilbert formulated as the central goal of his program to establish by elementary, so-called finitist means the consistency of formal systems. This involved a direct examination of formal proofs; the strongest results before 1931 were obtained by Ackermann, VON NEUMANN, and Herbrand: they established the consistency of number theory with a very restricted induction principle. A basic limitation had indeed been reached, as was made clear by Gödel's Second Theorem; see GÖDEL'S THEOREMS. Modern proof theory -- by using stronger than finitist, but still "constructive" means -- has been able to prove the consistency of significant parts of analysis. In pursuing this generalized consistency program, important insights have been gained into structural properties of proofs in special calculi ("normal form" of proofs in sequent and natural deduction calculi; cf. Gentzen 1934-35, 1936; Prawitz 1966). These structural properties are fundamental not only for modern LOGICAL REASONING SYSTEMS, but also for interesting psychological theories of human reasoning (see DEDUCTIVE REASONING and Rips 1994).
Hilbert's Entscheidungsproblem, the decision problem for first order logic, was one issue that required a precise characterization of "effective methods"; see CHURCH-TURING THESIS. Though partial positive answers were found during the 1920s, Church and TURING proved in 1936 that the general problem is undecidable. The result and the techniques involved in its proof (not to mention the very mathematical notions) inspired the investigation of the recursion theoretic complexity of sets that led at first to the classification of the arithmetical, hyperarithmetical, and analytical hierarchies, and later to that of the computational complexity classes.
Some general questions and results were described for particular systems; as a matter of fact, questions and results that led to three branches of modern logic: model theory, proof theory, and computability theory. However, to reemphasize the point, from an abstract recursion theoretic point of view any system of "syntactic configurations" whose "formulas" and "proofs" are effectively decidable (by a Turing machine) is a formal system. In a footnote to his 1931 paper added in 1963, Gödel made this point most strongly: "In my opinion the term 'formal system' or 'formalism' should never be used for anything but this notion. In a lecture at Princeton . . . I suggested certain transfinite generalizations of formalisms; but these are something radically different from formal systems in the proper sense of the term, whose characteristic property is that reasoning in them, in principle, can be completely replaced by mechanical devices." Thus, formal systems in this sense can in principle be implemented on computers and provide (at least partial) models for a wide variety of mental processes.
Frege, G. (1879). Begriffsschrift, eine der arithmetischen nachgebildete Formelsprache des reinen denkens. Halle: Nebert.
Frege, G. (1893). Grundgesetze der Arithmetik, begriffsschriftlich abgeleitet, vol. 1. Jena: Pohle.
Gentzen, G. (1934-35). Untersuchungen über das logische Schliessen 1, 2. Math. Zeitschrift 39: 176 - 210, 405 - 431. Translated in Gentzen (1969).
Gentzen, G. (1936). Die Widerspruchsfreiheit der reinen Zahlentheorie. Mathematische Annalen 112:493-565. Translated in Gentzen (1969).
Gentzen, G. (1969). The Collected Papers of Gerhard Gentzen. M. E. Szabo, Ed. Amsterdam: North-Holland.
Gödel, K. (1930). Die Vollständigkeit der Axiome des logischen Funktionenkalküls. Monatshefte für Mathematik und Physik 37:349-360. Translated in Collected Works 1.
Gödel, K. (1931). Über formal unentscheidbare Sätze der Principia Mathematica und verwandter Systeme 1. Monatshefte für Mathematik und Physik 38:173-198. Translated in Collected Works 1.
Gödel, K. (1986). Collected Works 1. Oxford: Oxford University Press.
Hilbert, D. (1899). Grundlagen der Geometrie. Leipzig: Teubner.
Hilbert, D. (1918). Die Prinzipien der Mathematik. Lectures given during the winter term 1917-18. Written by Paul Bernays. Mathematical Institute, University of Göttingen.
Hilbert, D., and W. Ackermann. (1928). Grundzüge der theoretichen Logik. Berlin: Springer.
Post, E. (1921). Introduction to a general theory of elementary propositions. Amer. J. Math. 43:163-185.
Prawitz, D. (1966). Natural Deduction: A Proof-Theoretical Study. Stockholm: Almqvist and Wiskell.
Rips, L. (1994). The Psychology of Proof-Deductive Reasoning in Human Thinking. Cambridge, MA: MIT Press.
Barwise, J., Ed. (1977). Handbook of Mathematical Logic. Amsterdam: North-Holland.
Börger, E., E. Graedel, and Y. Gurevich. (1997). The Classical Decision Problem. New York: Springer.
Kleene, S. C. (1952). Introduction to Metamathematics. Groningen: Wolters-Noordhoff Publishing.
Rogers, H. Jr. (1967). Theory of Recursive Functions and Effective Computability. New York: McGraw Hill.
Shoenfield, J. R. (1967). Mathematical Logic. Reading, MA: Addison-Wesley.
van Dalen, D. (1989). Logic and Structure. New York: Springer .
Copyright © 1999 Massachusetts Institute of Technology