Fall 2016 edition of Sets, Logic, Computation

The Fall 2016 edition of the OLP remix Sets, Logic, Computation is ready. As before, it includes the OLP part on sets, relations, and functions; the part on first-order logic (with natural deduction chosen as the proof system); and the part on Turing computability including the unsolvability of the halting and decision problems. The methods chapter on induction and biographies of Cantor, Church, Gentzen, Gödel, Noether, Russell, Tarski, Turing, and Zermelo appear as appendices.

At students’ request, problems are now listed at the end of each chapter. Many typos and errors have been corrected, a number of examples and problems have been added, and several proofs rewritten for clarity. I’ve also added chapter summaries and a glossary. There are also a few added sections, notably introduction sections to Chapters 5 and 7, as well as discussion of Russell’s Paradox in both Chapter 1 and 6.

You can order a printed copy on Lulu, or download the PDF from the builds page. Read about what last term’s students thought of it here.

SLC F16

More Photos of Logicians

As previously mentioned, the Open Logic Project now has a separate repository for photos of logicians to illustrate your OLP-derived materials.  They are automatically included in the biographies that live in content/history.  I’ve just uploaded a whole bunch of photos that don’t have associated biographies (yet).  Some of them are not well-known, even.

For the technicalities, I’ll repeat myself from the previous post:

We have a separate repository for photos: github.com/OpenLogicProject/photos. We’ve separated them because (a) the licensing issues are more complicated: some of the photos are under copyright, and we wanted everything in the main repository to be available under a Creative Commons license; (b) the main repository would become very large if it included all these pictures. To use the pictures, clone the photos repository into the assets/ subdirectory of your local OLP clone. There’s a PDF with all the photos on the build site.

Tracking down these pictures and getting permissions was (and continues to be) a surprising amount of work.  Thanks to all the people and archives who provided them and granted permissions: the IAS archives, Princeton University Library, Berkeley’s Bancroft Library, the Russell Archives at McMaster, the Archives of the Universities of Warsaw and Wittenberg-Halle, the ILLC, the Austrian National Library, the NSUB at Göttingen, the National Portrait Gallery, the Oslo Museum, the American Philosophical Society, Neil Reid (Julia Robinson’s brother-in-law), Libby Marcus (Ruth Barcan Marcus’s daughter), Kim Heffernan (Haskell Curry’s granddaughter), Béla and Eszther Andrásfai (Péter’s adoptive son and granddaughter), Christian Thiel, Volker Peckhaus, Lothar Kreiser, Eckhardt Menzler-Trott, Craig Smorynski, and Peter van Emde Boas. Detailed photo credits are included with the photos.  Thanks also to the Alberta OER initiative for providing some funding to do this.  And last, but not least, thanks to Joel Fuller for doing an awesome job with PhotoShop restoring some of these photos (the original Curry photo, in particular, had a big tear right through the middle)!

No thanks to the Oberwolfach Photo Collection, who outright refused to share their images.

More to come!

An Actual Textbook, and: Photos!

Two exciting new things from the Open Logic Project. The first one is another sample textbook. I’ve previously written about how to make a custom logic textbook and how to get your textbook to print, and for my course “Logic II (Phil 379)” this term, I’ve done that. Properly: perfect bound paperbacks, with a nice cover, proper front and back matter, professional illustrations, and an (I think) appealing book design. The source for generating it is on GitHub (of course): github.com/rzach/phil379. If you want to compile it, just clone that repository into the courses/ subdirectory of your local OLP clone. It should compile out of the box.  There are three files you can compile: phil379-screen.tex makes a multi-color PDF suitable for on-screen reading; phil379-print.tex makes a black-and-white PDF suitable for printing via lulu.com.  The third is cover-lulu-quarto.tex, which generates the PDF lulu.com uses for the cover. You can see the product on the builds site:

The second exciting thing is that we’ve started to put photos of logicians into the text. Right now, they’re imported into the biographies. The photos themselves are not in the main repository, however. We have a separate repository for them: github.com/OpenLogicProject/photos. We’ve separated them because (a) the licensing issues are more complicated: some of the photos are under copyright, and we wanted everything in the main repository to be available under a Creative Commons license; (b) the main repository would become very large if it included all these pictures. To use the pictures, clone the photos repository into the assets/ subdirectory of your local OLP clone. (If the files aren’t there, the biographies including them will happily compile but leave out the photos.) There’s a PDF with all the photos also on the build site.

(PS: If you want to buy an actual copy of the Sets, Logic, Computation book, go here. It sells for CAD 9.42 (USD 8.36, EUR 8.55). But be warned; we’ve already corrected a bunch of typos and errors, so that version is not up-to-date.)

New in the Open Logic Project: Turing Machines

We’ve had a very rudimentary chapter on Turing machines in the OLP for a while.  Samara and I have been working on expanding this over the last few months, using Nicole’s notes and writing some stuff from scratch. It is now is mature enough, I think, that it can be included. So I have merged the turing-machines branch into master.

A decisions of which variant of Turing machines to use had to be made. We opted for a version that allows the machine to write and move at the same time, since most of the online emulators work that way. We also decided to let the tape be infinite in one direction only. This makes the proof of undecidability of logic, which requires describing Turing machine configurations, a lot simpler.

It still needs work, of course, like everything else. More examples, more problems, a more in-depth discussion of the Church-Turing thesis, proofs of equivalence of different Turing machine variants, for instance. To tie it to the other computability material, I’d like to show that recursive functions are Turing computable. It would also be great to have some discussion of computational complexity and non-deterministic computation; Dean indicated that he might work in that direction.

In the meantime, enjoy, and please give feedback!

Walter Dean (Warwick) Joins Editorial Board

We’re happy to announce that Walter Dean, Associate Professor of Philosophy at the University of Warwick, has joined the Open Logic Project’s editorial board.  Walter regularly teaches courses on the material currently covered in the text, as well as modal logic (inclusion of which is planned for next year) and provability logic and computational complexity theory.  He is planning to contribute to these topics in particular.

Making a New Logic Textbook in Seven Easy Steps

I’ll be teaching the University of Calgary’s second logic course, imaginatively titled “Logic II,” next term.  It’ll be the first time for me to use the Open Logic Text for this course.  I used it for McGill’s “Intermediate Logic” earlier this year, and Nicole Wyatt has been using parts of the text the last time she taught it a year ago.  Lots has changed, and I’m aiming to provide a nice, self-contained book.  I’ll document the steps to make this happen.

To start, I have to pick the material to include. Logic II is supposed to cover “Introduction to the metatheory of logical systems. Completeness, compactness, Löwenheim-Skolem, and undecidability theorems for first-order logic.”  In previous iterations, I’ve used Boolos, Burgess, and Jeffrey’s Computability and Logic as a textbook, and that’s also what my colleagues who also teach it have used.  In part because of this, I’ve previously covered set theory, then Turing machines, first-order logic, undecidability, completeness and Löwenheim-Skolem theorems in that order: it’s the order BBJ covers it. But with an open text, I can rearrange things if I want to. And I think I do.  Once you cover relations, it’s sort of natural to continue with first-order semantics, definability, and expressibility.  So I’ll go with set theory, metatheory of first-order logic, Turing machines, and undecidability. (Right?)

To make a new book, you have to start by setting up a driver file that does all the setup and loads the parts and chapters you want in the right order.  Of course, I’ll use Git also for that driver file and anything else I’ll need to pull things together. So,

Step 1: set up a GitHub repository [You can skip this step if you don’t want to use Git to keep track of changes.].

Step 2: Clone the repository, so I have it on my local drive.  The Git URL is git@github.com:rzach/phil379.git.  I use SSH, but there’s also an HTTS URL: https://github.com/rzach/phil379.git.  Where do you put it?  It’s probably easiest if it lives with the other courses in the OLP directory.  So I go to where my OLP clone lives, then to the subdirectory holding the courses, and clone there:

$cd ~/tex/openlogic/courses/$ git clone git@github.com:rzach/phil379.git \$ cd phil379

[If you don’t want to use git, just make a new subdirectory of the /courses directory.]
Step 3: We have to start somewhere, so I’ll copy the files courses/sample/open-logic-sample.tex and courses/sample/open-logic-sample-config.tex from courses/sample to my new directory, renaming them to phil379.tex and phil379-config.tex, respectively. I’ll also add a license and a Makefile, but you wouldn’t have to.

Step 4: The main file, phil379.tex contains the instructions for what to include and in what order.  I’ve changed it so that only what I need is included.  Here is what it looks like at this point, and here are the changes I made to the original open-logic-sample.tex file.  I haven’t yet done anything to the formatting or layout, just changed the title page and what chapters are included.

Step 5: I do want to do a few things a bit different from the default.  First of all, I’ll make the text unpretentious: no Greek formulas, no Fraktur letters for structures.  I haven’t yet made up my mind about terminology, but I think I might want to use “countable” instead of “enumerable”.  (I wouldn’t if I were going to talk about “computably” or “recursively enumerable” sets, but I think I won’t.  And when you’re talking about sizes of sets, “countable” and “uncountable” is a bit more conventional and easier to say. Maybe. I might change my mind later.)  There are some switches I can adjust, too: e.g., I’d like to have everything but biconditional and “true” be primitive symbols: That way there are more cases to prove, but I’ll get all the cases for the conditional and the universal quantifier as exercises.  Lastly, the first-order-logic part includes both sequent calculus and natural deduction as proof systems, but I’ll cover only one.  Maybe natural deduction.  Might change my mind on that too.  Anyway, all these things can easily be specified in phil379-config.sty.

Step 6: Run phil379.tex through LaTeX, get a nice PDF.

Step 7: Commit everything and push to GitHub, so it’s saved (and I can link to the source files here).

[UPDATE: (a) The current version has phil379.tex containing only the content, and the layout and setup is done by phil379-screen.tex and phil379-print.tex, which generate a version for on-screen reading and a version for printing, respectively. See also this post.]

After some internal discussion and canvassing of the Open Educational Resources community, we’ve switched the license from Creative Commons Attribution-ShareAlike (CC-BY-SA) to Creative Commons Attribution (CC-BY).  BY-SA requires that anyone is free to use & modify a work as long as the modified work is “shared alike,” i.e., under a compatible license.  The idea is that if you use it, you have to let others use your improvements & modifications as well.  This is a laudable goal, of course, and we hope anyone who does build upon the OLP will do so!  But it does, e.g., require that everyone who builds their own version of a textbook on the basis of OLP to license it under CC-BY-SA.  An instructor may not want to allow redistribution of their adopted text at all, for instance. So CC-BY-SA potentially restricts the usefulness of the project and inhibits uptake.

More Documentation

The master configuration file that holds all the commands that OLP texts use to typeset things — the file you mainly want to change to adapt OLP to your own needs — is now documented. The LaTeX comments that document it are written in Markdown, and the comments are automagically converted into a nice PDF that serves as a reference guide for the commands. Find it under “builds” as open-logic-config.pdf.

Additional documentation, of course, is all on the GitHub wiki.

The Open Logic Project

Tired of having to use an advanced logic text that isn’t quite right for your class?  Do you want to change the terminology, change the order in which material is covered, pick-and-choose what’s included, or add your own stuff directly to the text instead of distribute handouts?  And, in particular, would you like your text to be available for free?

That’s what the Open Logic Project is about: providing customizable building blocks for an advanced logic text.  We’re interested mainly in the kind of course aimed at advanced undergraduate/graduate students in philosophy.  (Why? There are good, standard texts in mathematical logic and logic for computer science, lots of material of interest to philosophers isn’t covered in standard logic texts, and philosophy students prefer a more verbose style of exposition and less mathematical examples.)

The current status of the text is “pre alpha” — it’s more a proof of concept than a finished product.  But it has been used already in Calgary’s Logic II course, which covers basics of set theory, soundness and completeness, Turing machines, and undecidability of first-order logic.

In addition to a modular mix-and-match approach, we’re planning some other features, like configurable nomenclature (change whether you want to call them “interpretations,” “structures,” or “models,” for instance, without search-and-replace), assistance with formatting the final PDF, etc.

All of this is not only open (free to use), but open source: you can download the source code, modify it to your liking, and if you like, contribute to the project. To find out more, start at the About page.  You can look at PDFs at builds.openlogicproject.org, and find the source code on GitHub.