The idea of reducing reasoning to computation in some kind of formal calculus is an old dream, going back at least to Raymond Lull. Hobbes in his ''Leviathan'' coined the slogan 'Reasoning is but Reckoning'. A particularly well-known statement of the idea was Leibniz's. He 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 mathematical reasoning. 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) 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, were just pure logic. This would show that mathematics is analytic, refuting Kant's dictum that it is synthetic a priori. In his work, Frege established such a standard of precision, and made so many important distinctions (e.g. between x and {x} and between and ), that he is commonly regarded as the founding father of modern logic. However his Begriffsschrift was cumbersome, quite unlike conventional mathematical notation, and a nightmare for printers.

Peano's teaching experience led him to be interested in stating mathematical results and arguments precisely. He developed a formal notation for expressing mathematical reasoning, 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.

On meeting Peano at a mathematical congress, Russell was sufficiently impressed to adopt Peano's symbolism in his own foundational investigation of mathematics. He started a similar programme to Frege, at first independently, though on becoming aware of Frege's work, he was to some extent directly influenced. Though some people opine that even Russell's subsequent work was a step backwards from Frege's in terms of precision, Russell also 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: the co-discoverer of Russell's paradox, [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.) This 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, and a separate Axiom of Infinity needed to be posited (as well as an Axiom of Reducibility, but that was an artifact of the unnecessary complication of ramified types). For this reason, Principia failed to establish the logicist thesis that mathematics is completely reducible to logic.

What Principia unmistakably succeeded in doing was 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 which 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's own intellect, he reports, never quite recovered from the strain of writing it. 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 aims of the pioneers of actually using logic were 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.

John Harrison 96/2/22; HTML by 96/4/5