I well remember, after many years, my surprise and awe at the beauty of the structure of my undergraduate course on logic and computability, which led students from the basics of propositional logic to Gödel’s incompleteness theorems. Unfortunately, I realized this only as I was going over the material before the final; until then, I was frustrated by the nit-picking details of each lecture and didn’t see the forest for the trees. Sadly, this is a common experience for many undergraduates, who never see the beauty.
This would seem to be unavoidable, because the topic is full of details that are essential to the whole structure. Gonczarowski and Nisan present a radical approach to Logic 101, in which the drudgery is relegated to Python code instead of dry mathematics. This doesn’t make it disappear, but it becomes much more palatable to computer science (CS) students, who are used to writing code and even enjoy it. Because much of Logic 101 is a set of definitions and (effective) computations on syntax, models, and proofs, it is very natural to study it using a concrete programming language. A small part of the course, which deals with infinite structures or non-computable procedures, is left in conventional mathematical form. Sometimes the switch between programs and mathematical reasoning is quite subtle, as when using proof by contradiction (where the program computes the steps leading to the contradiction) inside a larger proof.
This approach has the added advantage of clarifying the distinction between formal proofs (represented as Python objects) and meta-mathematical proofs, which are done in the usual way and whose subject matter consists of Python objects. On the other hand, carrying this approach to its logical conclusion requires a discussion of program correctness (including termination), which is omitted in this book and instead supplemented by tests.
The book has two parts: propositional and predicate calculus. Both have a similar structure: syntax and semantics (chapters 1, 2, and 7); proofs (4, 5, 8, and 9); and tautology and completeness theorems (6, 11, and 12). Additional material discusses alternative sets of operators (chapter 3), examples of proofs in several axiom systems (9), the deduction theorem (11), and a lightning-quick overview of Gödel’s first incompleteness theorem (13). Each chapter (except the last) contains a set of programming tasks to be solved by students, based on a framework provided by the authors. Each task is described in detail and is accompanied by skeleton code and extensive test cases. As such, most of the study in this course is done as homework by the students--I believe there is no better way for students to understand the various algorithms and constructions than by programming them themselves.
The skeleton code for each task contains extensive checks for its preconditions, which is very helpful. I would also have liked to see postcondition checks (except when they are identical to the body of the function). The code is almost always functional, except for some unfortunate lapses (such as the way to obtain fresh variables).
The book sometimes deviates from the standard logical formalism (the most striking example is the treatment of substitution). This is perhaps justified by the wish to simplify it for students; however, it may cause difficulties for them later on, when they are expected to know the standard formalisms in subsequent courses or texts.
The book’s text is rather terse and concise, and appears to be addressed more to teachers than students (who I suspect would struggle to understand its finer points alone). (This is particularly true for the footnotes, some of which introduce advanced concepts.) Sometimes there is inadvertent confusion, caused, for example, by referring to a non-constructive procedure as a “construction,” or by the use of the same symbol for slightly different purposes (S sometimes denotes a finite and sometimes an infinite set in the same paragraph).
In spite of these growing pains (which I’m sure would be improved in the next edition), this book presents a fresh and unique approach to a course that has been taught in essentially the same way for decades, making it much more accessible and enjoyable for today’s students, who are comfortable programming and thinking in computational terms even if their major is not CS. Every teacher of a first course in logic should consider trying this approach. On a related note, I’m looking forward to the second part, which will use the same method to get to Gödel’s first incompleteness theorem. This should be very appropriate since much of the way to that proof also consists of computational content.
