Now With Axiomatic Derivations!

In addition to sequent calculus and natural deduction, the Open Logic Text now covers axiomatic derivations as well. Happy Holidays!

forall x YYC: Winter is coming

Pulled the switch on the new natural deduction rules; the Winter 2018 ß version is now out. If you have corrections etc. you want included in the next edition or want to proof read the changes before the new version goes up on Amazon, now is the time.

ISSOTL 2017 Presentation of Student-Oriented Logic Course

Aaron had a poster presentation at last week’s ISSOTL conference in Calgary, presenting the results of our evaluation of his intro logic course using some novel delivery techniques and the Calgary remix of forall x.


Download the poster here.

Natural Deduction Rules in forall x: Calgary

Prompted by a good suggestion by Richard Lawrence and support from Catrin Campbell-Moore, we’ve been working on revising the natural deduction rules used in the Calgary Remix of forall x, the intro logic text by P. D. Magnus.  The proposal is to rename some rules so the nomenclature is in line with that used in the literature on natural deduction, e.g., where the rule A, \lnot A \vdash \bot is \lnot-elimination, not \bot-introduction, and \bot \vdash A is now called “explosion,” not \bot-elimination. We’re also planning to replace the tertium non datur rule with an indirect proof rule, i.e., Prawitz’s classical absurdity rule. (Tertium non datur, which we now slightly less pretentiously call “law of excluded middle” LEM,  will stay an “official” derived rule.) The proof checker recognizes both the old and the new rules.

We have an issue on GitHub tracking the progress and a branch with the revisions. The current version of the result is attached (see esp. Sections 15.7, 16.5, 19.4-5), but a few exercises elsewhere were changed, as were some of the solutions. Comments welcome!


Textbook Satisfaction Survey Results: Intro Logic Edition

As previously reported, we here at Open Logic Central have run surveys to gather some data on the relative success our open textbooks have with students. The first survey was done in several sections of Calgary’s Logic II course, where some sections of the course used Boolos, Burgess, and Jeffrey’s Computability and Logic, and some used the OLP-derived Sets, Logic, Computation.  We’ve now run these surveys also in Logic I, our first course in formal logic. One section, taught by Aaron, used forall x: Calgary Remix, four others used either Goldfarb’s Deductive Logic or Chellas’s Elementary Formal Logic. forall x was provided free as a PDF; the hardcopy retailed in the bookstore for $12, Goldfarb for $54, and Chellas for $40. The highlights are below. But first a

HUGE CAVEAT: As encouraging as they are, of course, the result must be taken with a large grain of salt. The sections surveyed were taught by different instructors and with different TAs, at different times of day, in different terms, with different modes of delivery, and different modes of evaluation. Students’ attitudes towards a text used in a course depend not only on the text itself, but also on their experience in the course overall. If the material covered and tested in lecture doesn’t match up with the text, they may see it as a failure of the text. The quality of instruction may influence the perception of the quality of the textbook as well. Which direction? I think either is possible. If lectures are clear, students find it easier to understand the textbook, and so find it clearer. Or, if lectures are unclear, the textbook may look clearer by comparison.

As in the previously reported results in Logic II, students consulted the open textbook much more frequently than the other two textbooks.

They also consistently used forall x more for specific purposes.

forall x also ranks significantly better on every measure of textbook quality we asked about.

Last time I made the plots laboriously in Excel and This time, the plots were done in R. (Still laborious, since I knew and still know pretty much zero about R.) If you’re curious exactly how, I wrote it up. Data and code on Github.

A Fistful of Commits

I just checked in a whole bunch of changes to the part on first-order logic. Most of it is in preparation for a new version of the Logic II textbook Sets, Logic, Computation, which Nicole is planning to use in the Fall term.  Also important, and that’s why I put it right here at the top:

PDFs now live on The builds site has a nice index page now rather than a plain file list. If you link to a PDF on my ucalgary site, please update your link; that site will no longer be updated and will probably disappear sometime soon.

Here’s a list of changes:

  • I’ve revised the completeness theorem thoroughly. (This was issue 38.) The main change is that instead of constructing a maximally consistent set, we construct a complete and consistent set. Of course, those are extensionally the same; but both the reason for why we need them and the way we construct them is directly related to completeness and only indirectly to maximal consistency: We want a set that contains exactly one of A or ¬A for every sentence so we can define a term model and prove the truth lemma. And we construct that set by systematically adding either A or ¬A (whichever one is consistent) to the original set. So it makes pedagogical sense to say that’s what we’re doing rather than confuse students with the notion of maximal consistency, prove that the Lindenbaum construction yields a maximally consistent set, and show that maximally consistent sets are complete so we can define the term model from it. Credit for the idea goes to Greg Restall, who does this in his course on Advanced Logic.  (I kind of wonder why standard textbooks mention maximally consistent sets. I’m guessing it’s because if you consider uncountable languages you have to use Zorn’s lemma to prove Lindenbaum’s theorem, and then using maximality is more natural. Is that right?) A bonus effect of this change is that a direct proof of the compactness theorem is now a tedious but relatively easy adaptation of the completeness proof; and I’ve added a section on this (leaving most of the details as exercises).
  • I’ve revised the soundness proofs for sequent calculus and natural deduction, where the individual cases are now more clearly discussed. (This was issue 74 and issue 125.)
  • In the process I also simplified a bunch of things, filled in some details, and corrected some errors. This includes fixing issue 110, and cleaning up the whole stuff about extensionality. There is a new section on assignments which you may need to add to your driver file unless you include fol/syn/syntax-and-semantics.tex in its entirety.
  • The natural deduction system now uses Prawitz’s standard rules, i.e., the double negation elimination rule has been replaced with the classical absurdity rule, and the negation rules are now the special cases of the conditional rules with ⊥ as consequent. This was issue 144. Comparing the system to other treatments in the literature is now easier, and the chapter will integrate more seamlessly with the part on intuitionistic logic that’s in the works.
  • The sequent calculus chapter now uses sequents that are made up of sequences, not sets, of formulas. This was issue 145. This is the standard way of doing it, and will make it easier to add material on substructural logics. It also makes the soundness proof a lot easier to understand.
  • In both the sequent calculus and natural deduction chapters, the material on quantifiers is now separated from that on propositional connectives. Eventually it should be possible to present propositional logic separately (or only), and now you can reuse only the material on propositional logic. (This was issue 77.)
  • There is a new chapter on proof systems, and the intro sections from both the natural deduction and sequent calculus chapters have moved there. So if you only want one of the proof systems, you’ll have to include the relevant intro section in the chapter on the proof system “by hand.” But if you include both, you now have an additional chapter that introduces and compares them.  (This was issue 61.)
  • Sets, Logic, Computation (the textbook for Logic II) now includes both sequent calculus and natural deduction!

Note: The formatting of the rules in both systems now uses a defish (“definition-ish”) environment. If your remix uses a custom -envs.sty file, you will need to add a definition for that at the end (see open-logic-envs.sty). The textbooks for Logic II and Logic III have been updated accordingly.

Diagrams, and a Chapter on How to do Proofs

Two major new additions: Paul Daniell has contributed a number of very nice illustrations for the “Sets” and “Functions” chapters, and I’ve turned Samara’s handout on how to do and write proofs into a new chapter in the “Methods” part.

The diagrams are done in Illustrator and I’ve fiddled with various ways of turning them into tikz code so they can be styled in LaTeX (e.g., the colors changed). We’ll have to define and document a “house style” for additional diagrams, and also the way the conversion to tikz code works.  (The .tikz files live in assets/diagrams for now).

The “Proofs” chapter is a brief intro on how to do mathematical proofs; all examples are from the “Sets” chapter, so don’t require a whole lot of mathematical background.  There are lots of examples, and some tips for what to do when you get stuck. Feedback welcome!

New in Print: forall x (Summer 2017 edition), and Incompleteness and Computability

New on Amazon: the print version of the Summer 2017 edition of forall x: Calgary Remix, as well as the text I made for Phil 479 (Logic III) last term, Incompleteness and Computability.

The new edition of forall x includes a number of corrections submitted by Richard Lawrence, who taught from it at Berkeley in the Spring term. I’ve also noticed that if you don’t want Amazon to distribute the book to libraries and bookstores, you can make it a lot cheaper: USD 7.62 instead of USD 11.35.  Of course, the PDF is still free. (There’s now also a version for printing on letter-sized paper.) With Richard’s and Aaron’s help, the solutions manual now matches the text and has fewer errors.

Links to Amazon: US UK Canada Germany

The print version of Incompleteness and Computability incorporates a number of corrections and improvements suggested by my Logic III students. Compared to the version announced earlier, it also includes the two new chapters on Models of Arithmetic and on Second-order Logic. It, too, is still available free in both PDF and source code.

Links to Amazon: US UK Canada Germany

forall x: YYC is now on Amazon (and how it got there)

Back when I described the process to publish a text on, commenter penrodyn suggested to try CreateSpace, Amazon’s self-publishing platform.  So I did. You can now purchase forall x: Calgary Remix on Amazon (Canada, UK). (Apparently it already ranks #27 in the Math/Logic category!?)

It turns out it wasn’t hard to do at all. CreateSpace works pretty much the same way Lulu does. You need a PDF of the interior that matches one of the sizes offered. I picked 7.44″ x 9.69″, which is almost the same as Lulu’s Quarto size, so I could use the same PDF as for Lulu.  Getting the dimensions for the cover was a bit harder, since CreateSpace doesn’t tell you what the specific dimensions should be, and lets you compute them yourself.  You also need to include .125″ bleed on all sides. On the upside, they put the ISBN bar code on it for you.  The file to produce the CreateSpace cover is here. Before the book is ready to sell in the Amazon store, the PDF has to be reviewed–this takes about a day.

The final product is slightly lower quality than Lulu’s, and is probably comparable to Lulu’s “value” print option (in the US store called “standard”). Note, though, that only two format options are available at “value” prices for Lulu (e.g., if you want quarto, value isn’t an option). The cover print is less vibrant, the inside stock used is lighter and less bright. It also ended up being slightly more expensive (US$11.35 vs. US$10.64 at Lulu; CAD 15.47 vs CAD 12.08 at Lulu). Depending on if you catch Lulu at one of their very frequent discount deals,  you might be much better off with Lulu, especially if you (or your bookstore) orders a whole bunch. But if it’s not the only book you’re buying, Amazon probably will get it to you faster and the shipping will be free.

The price point surprised me a bit because the original comment said CreateSpace is a lot cheaper. And it in fact is, but only for yourself: I can order the book for $4.54.  $11.35 was the minimum list price I could enter, and apparently I get $2.27 in royalties for every book sold. I feel bad about that, but I promise to use it only for good (like pay for the website!).  [UPDATE: If you deselect “Expanded Distribution,” the minimum US list price is a lot less and you don’t have to take royalties.] Another difference is that CreateSpace only does USD, GBP, and EUR, so proof copies ship from the US and you have to pay US$. [UPDATE: Also, you should be aware that it can take a few days for the book to become available on Amazon. CreateSpace books sold on also go up for sale on the Canadian site, but it can take up to 30 days.]

Lulu also lets you list your book on Amazon (and Barnes&Noble, etc.), but: you have to purchase a physical proof copy before it’s approved, the list price will be higher than what you can set it to on ($8 more), and I suspect it will ship from an Amazon seller and so you won’t be able to bundle it with other Amazon orders for free shipping. But I haven’t tried that yet.

Overall, it was easy enough, the quality is decent, and if your bookstore can’t bulk order for your class, your students may prefer ordering from Amazon. If you want a really cheap but perfect-bound book, use Lulu, go with the standard/value option, and sell at cost. If you care about the quality, use Lulu’s standard/premium print option. If you want it to be available ASAP, use Lulu. If you want convenience and visibility, use CreateSpace.



OLP at the Pacific APA/Spring ASL Meeting

The Open Logic Project will be part of the Thursday afternoon session “Inclusiveness in Logic Education” (session 7P) at the Pacific Division Meeting of the APA. The session is part of the Spring Meeting of the Association for Symbolic Logic, and is organized by Audrey Yap on behalf of the ASL Committee on Logic Education.

It is followed by a reception sponsored by the ASL!