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.

Just FYI if you’re thinking of doing that yourself: all three existing versions (and now also ours) are on GitHub. With a GitHub account you can “fork” those, ie, make your own copy of them, and then make changes in that fork. That way, if the original version changes (e.g., when an error is corrected) you can send yourself a pull request and incorporate that change into your version. You (and others) can then also compare (“diff”) your version with the original to see what changes you’ve made. If none of that meant anything to you you, here’s my primer on Git: https://github.com/rzach/git4phi/blob/master/git4phi.md

Well done Aaron and Richard! !!