formalization an abstract representation of a theory that must satisfy requirements sharper than those imposed on the structure of theories by the axiomatic-deductive method. That method can be traced back to Euclid’s Elements. The crucial additional requirement is the regimentation of inferential steps in proofs: not only do axioms have to be given in advance, but the rules representing argumentative steps must also be taken from a predetermined list. To avoid a regress in the definition of proof and to achieve intersubjectivity on a minimal basis, the rules are to be ‘formal’ or ‘mechanical’ and must take into account only the form of statements. Thus, to exclude any ambiguity, a precise and effectively described language is needed to formalize particular theories. The general kind of requirements was clear to Aristotle and explicit in Leibniz; but it was only Frege who, in his Begriffsschrift (1879), presented, in addition to an expressively rich language with relations and quantifiers, an adequate logical calculus. Indeed, Frege’s calculus, when restricted to the language of predicate logic, turned out to be semantically complete. He provided for the first time the means to formalize mathematical proofs.
Frege pursued a clear philosophical aim, namely, to recognize the ‘epistemological nature’ of theorems. In the introduction to his Grundgesetze der Arithmetik (1893), Frege wrote: ‘By insisting that the chains of inference do not have any gaps we succeed in bringing to light every axiom, assumption, hypothesis or whatever else you want to call it on which a proof rests; in this way we obtain a basis for judging the epistemological nature of the theorem.’ The Fregean frame was used in the later development of mathematical logic, in particular, in proof theory. Gödel established through his incompleteness theorems fundamental limits of formalizations of particular theories, like the system of Principia Mathematica or axiomatic set theories. The general notion of formal theory emerged from the subsequent investigations of Church and Turing clarifying the concept of ‘mechanical procedure’ or ‘algorithm.’ Only then was it possible to state and prove the incompleteness theorems for all formal theories satisfying certain very basic representability and derivability conditions. Gödel emphasized repeatedly that these results do not establish ‘any bounds for the powers of human reason, but rather for the potentialities of pure formalism in mathematics.’ See also CHURCH’S THESIS, FREGE, GÖDEL’S INCOMPLETENESS THEOREMS , PROOF THEOR. W.S.
