Updates to OLP for Fall 2021 edition of Sets, Logic, Computation

In preparation for the Fall 2021 edition of Sets, Logic, Computation, the material in the Open Logic Project has seen a number of recent changes and additions. Here’s a rundown. I’d be glad to get feedback on the changes, esp. if you find any errors. If you do, please submit an issue on Github.

  • The part on first-order logic has long needed an introductory chapter that motivates why we need all the technical details on syntax and semantics. The syntax and semantics chapter has grown overly long and the details are daunting. So there is now a new chapter with an overview of the part on first-order logic, and the syntax and semantics chapter has been split into two. This results in renumbering of some chapters in the textbooks (Chapters 5, 6, 7 in Sets, Logic, Computation). (changes)
  • The definition of satisfaction only made use of variable assignments and x-variants; this made it hard to see how the definitions say “for some domain element” and “for all domain elements”. We’ve introduced the notation \(s[m/x]\) as the assignment just like \(s\), except assigning \(m\) to \(x\). See the discussion here and Section 7.4 in SLC. (changes)
  • Previously, the output of a Turing machine was taken to be whatever the longest non-blank block of symbols on the tape is after it halts. In particular, it was not required that a TM leaves its input at the beginning of the tape. That makes it difficult to chain together Turing machines: after the first machine halts, it must be possible to find its output. So the definition of output now is: the sequence of symbols between square 1 and the last non-blank symbol (Definition 14.10 in SLC). There now is also a definition of a “disciplined” Turing machine which halts on square 1 and also leaves the tape-end marker alone. Concatenations of disciplined machines is now safely defined (Section 14.8 of SLC). (changes)
  • The discussion of how Turing machines can be enumerated, and how their descriptions can be represented on the tape of another Turing machine were defective in that they required that the symbols of the described machine are all part of the symbol set of the machine dealing with the description. This makes it impossible to have a universal machine. Instead, we must standardize the vocabulary (and states), e.g., by assigning numbers to symbols and states, and then using unary representation for these numbers. This has been fixed (see Section 15.2 of SLC). Since it’s now possible to talk about the tape representations of arbitrary machines, we now have a section on universal Turing machines too (Section 15.3 of SLC). (changes)
  • The representation of Turing machines as first-order sentences (Section 15.6 in SLC) in the proof of the unsolvability of the decision problem unnecessarily required that the successor function is injective. This forced all models of \(T(M,w)\) to be infinite, even if \(M\) halts on \(w\). This has been fixed. Since it’s now relatively easy to expand the proof to Trakhtenbrot’s theorem, this has been added (Section 15.9 in SLC). (changes)
  • The discussion of inverse function has been improved (Section 3.4 of SLC) (changes)