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.

- COMPUTATION
- COMPUTATIONAL THEORY OF MIND
- LANGUAGE AND THOUGHT
- MENTAL MODELS
- RULES AND REPRESENTATIONS

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 .