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 lulu.com, 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 amazon.com also go up for sale on the Canadian site amazon.ca, 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 Lulu.com ($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!

New Chapters for #OpenEducationWk

We have new chapters on non-standard (and standard) models of arithmetic and on second-order logic.  First drafts, so please provide feedback and report mistakes you find (especially in the second-order logic part).

They are part of the new remixed text on incompleteness, too.

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).

UPDATE: The code is now on GitHub and runs on proofs.openlogicproject.org

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 lulu.com.

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.