1.6.1—
Formalization

In the second half of the nineteenth century, one of the most important issues in mathematics was the formalization of mathematical systems. The formalization of a mathematical system consists in the elimination from the system's deduction rules of anything dependent upon the meanings of the terms. Formalization became an important issue in mathematics after Gauss, Bolyai, Lobachevski, and Riemann independently found consistent geometries that denied Euclid's parallel postulate. This led to a desire to relieve the procedures employed in mathematical deductions of all dependence upon the semantic intuitions of the mathematician (for example, her Euclidean spatial intuitions). The process of formalization found a definitive spokesman in David Hilbert, whose book on the foundations of geometry, published in 1899, employed an approach to axiomatization that involved a complete abstraction from the meanings of the symbols. The formalization of logic, meanwhile, had been undertaken by Boole and later by Frege, Whitehead, and Russell, and the formalization of arithmetic by Peano.

While there were several different approaches to formalization in nineteenth-century mathematics, Hilbert's "symbol-game" approach is of

special interest for our purposes. In this approach, the symbols used in proofs are treated as tokens or pieces in a game, the "rules" of which govern the formation of expressions and the validity of deductions in that system. The rules employed in the symbol game, however, apply to formulae only insofar as the formulae fall under particular syntactic types. This ideal of formalization in a mathematical domain requires the ability to characterize, entirely in notational (symbolic and syntactic) terms, (a ) the rules for well-formedness of symbols, (b ) the rules for well-formedness of formulas, (c ) the axioms, and (d ) the rules that license derivations.

What is of interest about formalizability for our purposes is that, for limited domains, one can find methods for producing derivations that respect the meanings of the terms but do not rely upon the mathematician's knowledge of those meanings, because the method is based solely upon their syntactic features. Thus, for example, a logician might know a derivation-licensing rule to the effect that, whenever formulas of the form p and pÉq have been derived, he may validly derive a formula of the form q . To apply this rule, he need not know the interpretations of any of the substitution instances of p and q , or even know what relation is expressed by É , but need only be able to recognize symbol structures as having the syntactic forms p and p Éq . As a consequence, one can carry out rational, sense- and truth-preserving inferences without attending to—or even knowing—the meanings of the terms, so long as one can devise a set of syntactic types and a set of formal rules that capture all of the semantic distinctions necessary to license deductions in a given domain.