left up

The History of Formal Logic

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 memberof and subsetof). 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 of Principia), 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.

left right up home John Harrison 96/8/13; HTML by 96/8/16