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 builds.openlogicproject.org. 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.