Proof Checker for forall x: Cambridge and Calgary

Kevin Klement has done up a prototype of his online natural deduction proof builder/checker that works with the natural deduction system of the Cambridge and Calgary versions of forall x.  The system was originally written for UMass’s Intro Logic course, based on Gary Hardegree’s online textbook. Kevin writes:

Earlier I mentioned making some online exercises for the “forall x” book. Not sure how far I’ll follow through with it, but I did go ahead and mock up a proof builder and checker, and sample exercises using them. That seems like the most fun/interesting part. I wasn’t intending to target the Calgary remix, but that’s the version I was looking at when I made it. I realized only later that the proof system and notation is different from the original, but I left it stand. Anyway, I thought I’d post a demo before taking it any further, so others can take a look, make suggestions, and help identify bugs. The user interface was the hardest part, and I’m not entirely happy with it as is, but not sure how to improve. Let me know what you think.

If you find a bug or have suggestions for improvements, please let Kevin know! The code is open source (download link at the bottom of the page).

New Textbook on Incompleteness

I’m teaching the incompleteness theorems (and related material) this term, and of course I’m using the Open Logic Project as a text. The relevant sections are based on Jeremy Avigad’s notes, which originally were meant as a supplement to Epstein & Carnielli’s textbook Computability. I’ve spent a fair bit of time revising them, and making them independent of that text. That meant adding a bunch of material, reformatting things, adding explanations and examples, etc. I think it’s now in sufficiently good shape that I can share it. However, it’s by no means done (we’re only halfway through the semester). I’m waiting to hear what else my students want to hear about; and I’ll update the project with additional chapters from the OLP (perhaps yet to be written). The most unusual aspect of it so far is perhaps that I’m doing everything in natural deduction, including arithmetization of provability.

The most recent PDF version should be available here, but I’ll also attach the current version to this post. All the actual material (with the exception of the chapter summaries and the front matter) comes from the Open Logic Text. The code to produce the text in this version is on GitHub. As usual, suggestions more than welcome!

Incompleteness and Computability

forall x: Calgary Remix

Aaron is teaching our intro logic course (“Logic I”) this term, and as part of a pilot project to redesign that course (which also includes partially “flipping” it), we’ve also adapted P. D. Magnus’s open textbook forall x. To be more precise, we’ve remixed a remix by Tim Button of P.D. Magnus’ textbook with some material from J. Rob Loftis’s remix plus some material from Tim Button’s Metatheory and then added our own material and revisions.  (Aaron previously wrote about how we decided on these changes.) Thanks to Creative Common open licensing, we can do this: just shamelessly take other people’s work and make it work for us, without paying them. In this case, the license is CC BY-SA, which requires only that we give credit (the “BY” part) and that we make the end product available under the same terms (the “SA”) part.

In order to keep track of our changes, I’ve put our remix as well as PDM’s original and TB’s remix on GitHub. (JRB maintains his own GitHub repository of the Lorain County remix/expanded “Open Introduction to Logic”.) is  So if you want to start your own remix and also want to use Git, you can start from any of the four version by forking the respective repository.

Here’s a rundown of the most important changes, with links to the corresponding Git commits where you can see what’s changed.

  • We put some material from PDM’s original version back into TB’s version (b3b6f97).
  • We added some material from JRL’s remix, mainly a discussion of soundness and completeness and many exercises (09b6d3a) and glossary entries (3f1276c).
  • We added a chapter on normal forms and truth-functional completeness from TB’s Metatheory (f49b6b3) and make it independent of the rest of that book (0721158)
  • We moved the chapter on natural deduction for TFL to before the FOL part.
  • We made a whole bunch of smaller stylistic changes, e.g., change all I’s to we’s, shall’s to will’s, change some examples to make them less reliant on a US or British background, etc. (fd9b99e, f091b03, 2a95058), added a preface (afd969d), glossary entries for the part on FOL (367d614), as well as some changes to terminology (ffa6567).
  • Changed the typography and layout to match the Sets, Logic, Computation layout and to fit on Crown Quarto paper for printing at

You can see a complete line-by-line comparison on GitHub.

You can download the final product if you don’t want to compile it yourself, and you can even buy a printed copy if you want!

Warning: We have not done anything with the solutions yet, so those do not match the numbering in the book and in fact might not match the exercises themselves!

Four New Photos

Fresh from the Archives of American Mathematics at UT Austin, the photos repository now includes Henkin, Huntington, Rosser, and von Neumann.

Revisions to enumerability and size of sets sections

As per issues 107 and 109, the material in sets-relations-functions/sizes-of-sets needs to be cleaned up. It was inconsistent in its assumption about whether functions are always total (they are, according to the definition in the preceding chapter), it gave an incorrect formal definition of enumerability (leaving out the empty set), and whenever it mentions \mathbb{N} it inconsistently assumes that \mathbb{N} begins at 1. Issue 109 deals with the problem that the section size-of-sets uses the cardinality notation \left|X\right| which leads students to assume that they can manipulate cardinalities as they can in the finite case; the proposal is to replace \left|X\right| \le \left|Y\right| with X \preceq Y to avoid this.

Commit a6a70a4 fixes issue 109; commit 370cb02 fixes issue 107. The latter also reformulates the diagonal proofs to make them direct instead of reductio proofs.

If you teach these sections, these changes may affect you. Please comment on the issues in GitHub if you have concerns. They will be merged into the master branch in a week otherwise.

Choosing an Open Introductory Logic Text

I will be teaching our Logic I course beginning in January 2017, and we have decided to modify an existing free and open logic text for use in that and (hopefully) future sections of Logic I here in Calgary. We have decided to take Tim Button’s Cambridge Version of PD Magnus’s forallx as a starting point. This is part of a larger project aimed at updating that introductory logic course. In this post I’ll say a bit about why I made chose that remix of forallx, point to some changes we intend to make to that text, and a bit about the other texts I looked at.

One of the first, and least content centred considerations was typesetting software. Picking a version of forallx as a starting point meant we could typeset the book in LaTeX. This is important for three reasons. First, Richard Zach and I are both used to working in LaTeX. Second, LaTeX allows for easy manipulation and restructuring of the text; swapping material between versions, or even inclusion of material in or from the Open Logic Project. Third, LaTeX is also free and open, which we think is important.

The result of sticking to books written in LaTeX was to move texts produced in LaTeX to the top of the pile, so to speak. So, for LaTeX-y and other considerations related to ease of use and modification, I choose to concentrate on the forallx family of open logic texts. As far as I’m aware, there are three versions of that text (not including the YYC remix that we’re developing) – the original by P.D. Magnus, the Cambridge version put together by Tim Button, and the Open Introduction to Logic aka the Lorain County Remix, put together by J. Robert Loftis. One major difference is worth noting at this point. Loftis’ version includes a great deal more material taken from Cathal Woods’ critical thinking text, that I would classify as belonging to an informal logic curriculum. The Magnus and Button versions, on the other hand, cover almost exactly the range of material that we cover in the Logic I course that I’ll be teaching.

Now we wanted to try to ensure that we wouldn’t be giving ourselves extra work when preparing forallx-YYC, so the goal was to pick a book that would need as little revision as possible. I suspect that changes will continue to be made to the text over the next couple of years at least, but having a text that meets our needs and will be ready for students to download in January is the first priority. This meant that simple things like using our preferred symbols for the connectives (¬, ∧, ∨, ↔, →), or using “first-order logic” instead of “predicate logic” put Button’s version ahead from the start. Most of us who’ve spent a large amount of time around symbolic logic have preferences when it comes to symbols and terminology, but in this case another major concern was continuity with the Open Logic Project. This was also a factor in making some of the other terminological and notational decisions, as it would be great to have it be possible for there to be continuity between the free and open texts for our first two logic courses, which are required for many students in philosophy and computer science. It turned out that Button’s book matched our preferences on many of these issues as well.

Although terminology and notational conventions are often important, especially for those students who go on to do more logic or philosophy of logic, more pedagogically and philosophically important are decisions related to how the proof theory and model theory (semantics) of first-order quantified predicate logic are set up.

I’ll start with proof theory. All three texts use Fitch-style natural deduction systems. So far so good – such systems are widely used, perspicuous, and useful. The first decision then was to decide whether to include a symbol for what Frege called the False, i.e. ‘⊥’ which I call “bottom”. Magnus and Loftis don’t, Button does. We went with ‘yes’ for a couple of reasons (Button gives some similar justifications). For one, it makes certain features of classical logic like the rule ex falso quod libet (explosion), that says that you can derive absolutely anything from a contradiction, more obvious. Relatedly, including bottom means that if students go on to study non-classical logics, and especially intuitionistic logic, the relationships between the logics are easy to see. Finally, it cleans up rules like those for negation by making the relationship between (classical) negation and truth clearer.

In this case, although Button includes bottom, he takes it to be defined by a canonical contradiction, whereas we will take it as primitive. Although this won’t be of great importance in this level course, it will hopefully make things less confusing, and raise fewer tough philosophical issues. (It also jives well with my ever more frequent Fregean tendencies.)

The other major issue in introducing the proof theory of first-order logic is how to deal with disjunction elimination. In introductory logic texts and courses the primitive disjunction elimination rule is very often disjunctive syllogism (¬A, A∨ B ⊢ B); it’s simple and there’s no doubt that DS plays an important role in classical deduction, but taking DS as primitive also inextricably ties disjunction to negation. Instead, I, like Button, and unlike Magnus and Loftis, prefer to use proof by cases (A∨ B, [A⊢C, B⊢C], ⊢C) for disjunction elimination. A further reason to do this is that proof by cases is a common proof strategy in mathematics, mathematical logic, and metalogic, and thus important in its own right.

In the case of model theory, I vacillated between wanting to include explicit set talk as per Magnus as Loftis, or instead eschew set talk in favour of plural locutions a la Button. Although there are benefits to including sets — that’s how model theory is usually done, students going on to take Logic II will need to learn about sets – we eventually decided that the difficulties in using sets, mostly related to added notational and conceptual complexity, outweighed the benefits. Additionally, I think there are good philosophical reasons for avoiding sets when doing model theory. Issues relating to intensionality, absolute generality, and indefinite extensibility come immediately to mind.

At the end of the day, the most significant goals in an introductory logic course are getting students used to doing the proof theory and model theory for formal languages, so given our preferences, Tim Button’s Cambridge Remix was the obvious choice as a starting point. We’ve sat down with printouts of all three versions and made a “Frankenbook,” slightly rearranging the material, adding some bits and pieces from Magnus’ original (mainly exercises) and the Woods/Loftis’ remix (exercises, a section on soundness and completeness, and the glossary), as well as a chapter on normal forms and expressive completeness from Button’s Metatheory book.  All of that’s now up on Richard’s GitHub (and the PDF here); we’ll continue to revise and add material, of course. (Magnus’ and Button’s source code is also available on GitHub through the OLP, and Loftis has his own repository).

Of course there are many other issues to consider when choosing or building an introductory logic text, but I hope to at least have given a good overview of how Richard and I are thinking about some of the relevant issues. I look forward to comments and suggestions from logic teachers current, past, and future. Keep your eye out for more updates from this project.

For Ada Lovelace Day: Julia Bowman Robinson

Julia Bowman Robinson was an American mathematician. She is known mainly for her work on decision problems, and most famously for her contributions to the solution of Hilbert’s tenth problem. Robinson was born in St. Louis, Missouri on December 8, 1919. At a young age Robinson recalls being intrigued by numbers. At age nine she contracted scarlet fever and suffered from several recurrent bouts of rheumatic fever. This forced her to spend much of her time in bed, putting her behind in her education. Although she was able to catch up with the help of private tutors, the physical effects of her illness had a lasting impact on her life.

Despite her childhood struggles, Robinson graduated high school with several awards in mathematics and the sciences. She started her university career at San Diego State College, and transferred to the University of California, Berkeley as a senior. There she was highly influenced by the mathematician Raphael Robinson. They quickly became good friends, and married in 1941. As a spouse of a faculty member, Robinson was barred from teaching in the mathematics department at Berkeley. Although she continued to audit mathematics classes, she hoped to leave university and start a family. Not long after her wedding, however, Robinson contracted pneumonia. She was told that there was substantial scar tissue build up on her heart due to the rheumatic fever she suffered as a child. Due to the severity of the scar tissue, the doctor predicted that she would not live past forty and she was advised not to have children .

Robinson was depressed for a long time, but eventually decided to continue studying mathematics. She returned to Berkeley and completed her PhD in 1948 under the supervision of Alfred Tarski. The first-order theory of the real numbers had been shown to be decidable by Tarski, and from Gödel’s work it followed that the first-order theory of the natural numbers is undecidable. It was a major open problem whether the first-order theory of the rationals is decidable or not. In her thesis , Robinson proved that it was not.

Interested in decision problems, Robinson next attempted to find a solution Hilbert’s tenth problem. This problem was one of a famous list of 23 mathematical problems posed by David Hilbert in 1900. The tenth problem asks whether there is an algorithm that will answer, in a finite amount of time, whether or not a polynomial equation with integer coefficients, such as 3x2 − 2y + 3 = 0, has a solution in the integers. Such questions are known as Diophantine problems. After some initial successes, Robinson joined forces with Martin Davis and Hilary Putnam, who were also working on the problem. They succeeded in showing that exponential Diophantine problems (where the unknowns may also appear as exponents) are undecidable, and showed that a certain conjecture (later called “J.R.”) implies that Hilbert’s tenth problem is undecidable. Robinson continued to work on the problem for the next decade. In 1970, the young Russian mathematician Yuri Matijasevich finally proved the J.R. hypothesis. The combined result is now called the Matijasevich-Robinson-Davis-Putnam theorem, or MRDP theorem for short. Matijasevich and Robinson became friends and collaborated on several papers. In a letter to Matijasevich, Robinson once wrote that “actually I am very pleased that working together (thousands of miles apart) we are obviously making more progress than either one of us could alone” .

Robinson was the first female president of the American Mathematical Society, and the first woman to be elected to the National Academy of Science. She died on July 30, 1985 at the age of 65 after being diagnosed with leukemia.

(This short biography is part of the Open Logic Project; PDF here).

Have You Taught Using the Open Logic Project?

Have you used material from the Open Logic Project in your courses? We’d like to hear from you; please fill out this form:

How to Get (Printed) Open Textbooks to Your Students

One problem open textbooks (and instructors adopting open textbooks) face is how to make the texts available to their students. Of course, it’s easy to distribute electronic OERs. But if you want to provide your students a nice, printed version they can take to the coffee shop, you’re in a bind. First, you have to have it printed.  This is a bit of work, but with online print-on-demand services like it’s possible.  But students would have to order the text themselves, and tax and shipping can almost double the (low) cost of a print-on-demand paperback, especially if you want it fast.

So big props to our campus bookstore, especially its manager Brent Beatty, who agreed to order 30 copies for my class and sell them at cost. Brent has been a member of UCalgary’s OER Working Group, so he’s attuned to the issues and challenges of open textbooks. All I had to do was send him the order link; with volume discount, low volume shipping cost, and’s frequent (constant?) promotional discount (25%) the shelf price is just a few cents above the list price on lulu (C$11).

Now I just hope enough students buy it so they’re not making a loss!

Line Art Portraits of Logicians

You’ve probably seen some of the line art portraits of logicians we’ve commissioned. They were done by Calgary illustrator and graphic designer Matthew Leadbeater. We’re pleased to release them all now under a Creative Commons BY-NC license: anyone is free to use them in their own work, to create derivative works from them, and to share them, provided (a) credit to Matt Leadbeater is properly given and (see license terms!) (b) they are not used for any commercial purposes.

They each come in two versions, one with a line below, and one with the portrait in a circle.

You can download the original Adobe Illustrator files. For PNG and PDF formats, we have set up a GitHub repository.

Commissioning these illustrations was made possible by a grant from the Alberta OER initiative. We gratefully acknowledge the support.

[Bonus: an image file with all of them that tiles nicely, for your desktop background.]