The idea of reducing reasoning to computation in some kind of formal calculus
is an old dream, surveyed by *[marciszewski-murawski]*. Some trace the idea
back to Raymond Lull, though this is perhaps dubious. Certainly
*[hobbes-leviathan]* made explicit the analogy in the slogan 'Reason
[...] is nothing but Reckoning'.^{5} This parallel was developed by Leibniz, who envisaged a
'characteristica universalis' (universal language) and a 'calculus
ratiocinator' (calculus of reasoning). His idea was that disputes of all kinds,
not merely mathematical ones, could be settled if the parties translated their
dispute into the * characteristica* and then simply calculated. Leibniz even
made some steps towards realizing this lofty goal, but his work was largely
forgotten. Meanwhile, mathematics continued to acquire new symbolisms, which as
*[whitehead-intro]* says:

[...] have invariably been introduced to make things easy. [...] by the aid of symbolism, we can make transitions in reasoning almost mechanically by the eye, which otherwise would call into play the higher faculties of the brain. [...] Civilisation advances by extending the number of important operations which can be performed without thinking about them.

It was to be expected that the use of symbolism would eventually extend beyond
the subject matter of mathematics, to the reasoning used * in* mathematics.
*[boole-article]* developed the first really successful formal system for
logical and set-theoretic reasoning. What's more, he was one of the first to
emphasize the possibility of applying formal calculi to several different
situations, and doing calculations according to formal rules without regard to
the underlying interpretation. In this way he anticipated important parts of
the modern axiomatic method. However Boole's logic was limited to propositional
reasoning, and it was not until the much later development of quantifiers that
formal logic was ready to be applied to general mathematics. The first systems
adequate for this purpose were developed by Frege and Peano. Both were
mathematicians, and to some extent they had a common motive of making
mathematical reasoning more precise. But there were many contrasts between
them.

*[frege-beg]* devised his 'Begriffsschrift' ('concept-script' or
'ideography') for formal logic and mathematics, with the particular aim of
carrying through what later became known as the logicist programme. He wanted
to prove that not only the reasoning used in mathematics, but the *
underlying assumptions too*, and therefore the whole of mathematics, are just
pure logic. This would show that mathematics is analytic, refuting Kant's
dictum that it is synthetic a priori. Frege made all his deductions using a
precisely defined formal deductive system. For this reason above all others he
is nowadays commonly regarded as the founding father of modern logic. Moreover,
he independently invented quantifiers, and drew attention to numerous important
distinctions (e.g. between x and {x} and between and ).
However his Begriffsschrift, whatever its merits, was a two-dimensional system
of lines which was quite unlike conventional mathematical notation, and was a
nightmare for printers.^{6}

Peano's teaching experience led him to be interested in stating mathematical
results and arguments precisely. He developed a formal notation for expressing
mathematical propositions, which was rather closer to conventional symbolism
than was Frege's concept-script. He was not so interested in a foundational
reduction, but concentrated on rewriting mathematics in a formal framework.
Together with his colleagues and assistants he published a substantial amount
of formalized mathematics: his journal * Rivista di Matematica* was
published from 1891 until 1906, and polished versions were collected in various
editions of the * Formulaire de Math{é*matique}. However, although he
stated mathematical propositions in symbolic form, and seemed to be striving
towards a way of transforming assertions by analogy with algebraic equations,
he never developed a formal deductive system.

On meeting Peano at a mathematical congress, Russell was sufficiently impressed
to adopt Peano's symbolism in his own foundational investigation of
mathematics. He had started a similar programme to Frege, at first
independently, before becoming aware, via Peano, of how much Frege had already
done. On studying his works, Russell found a logical inconsistency at the core
of Frege's system (the Russell paradox which we have already mentioned). The
story of how he informed Frege of this just as the second volume of Frege's
book was in the press is well-known. Peano did not escape either:
*[zermelo-new]* waspishly rebutted Peano's criticism of the Axiom of Choice
by remarking that since Peano's system was inconsistent, AC was deducible in it
along with everything else.

Russell developed his own logic, which was distinguished from others by its
introduction of the notion of * type*. (We shall have more to say about this
idea later.) His logic combined, to some extent, the notational convenience of
Peano's system with the precision and foundational aspirations of Frege's work;
moreover it wasn't obviously inconsistent. In their monumental work '*
Principia Mathematica*', *[whitehead-principia]* began a formal development
of mathematics from this basis. Without the flexibility which typelessness
allowed, it was no longer possible to derive the existence of an infinite set
from logic alone,^{7} and a separate Axiom of Infinity needed to be posited (as well as
an Axiom of Reducibility, but that was a consequence of the unnecessary
complication of ramified types). For this reason, * Principia* failed to
establish the logicist thesis that mathematics is completely reducible to
logic. Moreover, as *[godel-russell]* remarks:

It is to be regretted that this first comprehensive and thorough going presentation of a mathematical logic and the derivation of mathematics from it is so greatly lacking in formal precision in the foundations (contained in^{*}1--^{*}21 ofPrincipia), that it presents in this respect a considerable step backwards as compared with Frege. What is missing, above all, is a precise statement of the syntax of the formalism.

Despite these misgivings, * Principia* unmistakably succeeded in showing
that important parts of real mathematical reasoning could be written out in a
completely formal logic, albeit starting from a few non-logical axioms. In a
way this was a triumph that has never been surpassed. But the resulting text
demands extremely close attention from the reader, and there can be few who
made the effort. Indeed, *[russell-autobiog]* remarks that his own
intellect 'never quite recovered from the strain of writing it'.^{8} Given this, the idea of a practical project
to formalize mathematics completely, or even to use formal logic at all, seemed
a dubious one. The development of * Principia* was never carried further,
perhaps because of Russell's exhaustion, or simply because his primary interest
was the logicist thesis rather than formal mathematics * per se*.
Increasingly, formal logic came to be seen as a theoretical device, rather than
as a practical tool. The aim of the pioneers of actually * using* logic was
widely dismissed. For example *[rasiowa-sikorski]* say:

... this mechanical method of deducing some mathematical theorems has no practical value because it is too complicated in practice.