You are here

The Great Formal Machinery Works: Theories of Deduction and Computation at the Origins of the Digital Age

Jan von Plato
Princeton University Press
Publication Date: 
Number of Pages: 
[Reviewed by
Mark Causapin
, on

As this book’s title suggests, the author sought to connect the development of the concepts of deduction, formal mathematical proofs, and theories of computation to the development of modern day computers. Von Plato makes the claim right in the first sentence: “if around 1930 Kurt Gödel had not thought very deeply about the foundations of mathematics, there would be no information society in the form in which we have it today.”

In the first chapter, von Plato traces the historical development of the study of logic and the foundations of mathematics, beginning from Aristotle’s syllogisms. He then gives an overall view of how these ideas connected to mathematical developments in the 19th to the early 20th century, giving the readers a glimpse of the contents of the entire book.

The book’s narrative begins with the emergence of the study of the foundations of mathematics — the study of the justifications of procedures and ideas in arithmetic. Here, von Plato expounds on the ideas of Grassmann and Peano — the use of axioms, recursion, and mathematical formalization — which the author suggests is a requisite for subsequent “machine executability.” He then writes about the beginning of algebraic logic, Boole’s “calculus of deductive reasoning,” which has its origins in Aristotle’s syllogisms. Next would be people who would build upon Boole’s mathematics, such as Schröder and Skolem. The author dedicates a whole chapter to Frege and his ideas on formal reasoning: that proofs can be decomposed into simple logical steps and that mathematics can be reduced to logic. Finally, he writes about the contributions of various mathematicians such as Russell, Wittgenstein, Hilbert, Bernays, Gentzen, and, of course, Gödel.

The effort that von Plato put into the book is evident. It is a historical exposition that does not avoid the specialized notations and ideas inherent to this area of mathematics. It presents the evolution of ideas within the context of what was happening in Europe; for example, readers get a glimpse of Bernays’s life, fired from Göttingen because he was a Jew.

The book is not for leisurely reading, however. The suitable audience for this book includes people who have sufficient background in logic or theory of computation. As the author explains, the chapters are based on his lecture notes. What may be lacking, which in no way lessens the substance and significance of this book, is a more careful explanation of the connection claimed by the author, between the study of logic and foundations of mathematics on the one hand and modern day computing on the other. The only chapter that covers this is the prologue, which seems short given that the title suggests a more nuanced explanation of how the areas of mathematics connect to the digital age. Nevertheless, this book is an important contribution to the study of the history of mathematics, and any student, educator, or practitioner of mathematics or computer science, would benefit from reading this work.

Mark Causapin is an Assistant Professor of Mathematics at Aquinas College in Nashville, Tennessee.

Preface ix
Prologue: Logical Roots of the Digital Age 1
1. An Ancient Tradition 5
1.1. Reduction to the Evident 5
1.2. Aristotle's Deductive Logic 7
1.3. Infinity and Incommensurability 16
1.4. Deductive and Marginal Notions of Truth 21
2. The Emergence of Foundational Study 29
2.1. In Search of the Roots of Formal Computation 31
2.2. Grassmann's Formalization of Calculation 40
2.3. Peano: The Logic of Grassmann's Formal Proofs 50
2.4. Axiomatic Geometry 57
2.5. Real Numbers 69
3. The Algebraic Tradition of Logic 81
3.1. Boole's Logical Algebra 81
3.2. Schröder's Algebraic Logic 83
3.3. Skolem's Combinatorics of Deduction 86
4. Frege's Discovery of Formal Reasoning 94
4.1. A Formula Language of Pure Thinking 94
4.2. Inference to Generality 110
4.3. Equality and Extensionality 112
4.4. Frege's Successes and Failures 117
5. Russell: Adding Quantifiers to Peano's Logic 128
5.1. Axiomatic Logic 128
5.2. The Rediscovery of Frege's Generality 131
5.3. Russell's Failures 137
6. The Point of Constructivity 140
6.1. Skolem's Finitism 140
6.2. Stricter Than Skolem: Wittgenstein and His Students 151
6.3. The Point of Intuitionistic Geometry 167
6.4. Intuitionistic Logic in the 1920s 173
7. The Göttingers 185
7.1. Hilbert's Program and Its Programmers 185
7.2. Logic in Göttingen 191
7.3. The Situation in Foundational Research around 1930 210
8. Gödel's Theorem: An End and a Beginning 230
8.1. How Gödel Found His Theorem 230
8.2. Consequences of Gödel's Theorem 243
8.3. Two "Berliners" 248
9. The Perfection of Pure Logic 255
9.1. Natural Deduction 256
9.2. Sequent Calculus 286
9.3. Logical Calculi and Their Applications 303
10. The Problem of Consistency 318
10.1. What Does a Consistency Proof Prove? 319
10.2. Gentzen's Original Proof of Consistency 326
10.3. Bar Induction: A Hidden Element in the Consistency Proof 343
References 353
Index 373