OpenLogicProject / OpenLogic

An open-source, customizable intermediate logic textbook
http://openlogicproject.org/
Creative Commons Attribution 4.0 International
1.02k stars 234 forks source link

Minor typesetting issue #370

Closed marethyu closed 2 months ago

marethyu commented 3 months ago

I believe that all instances of O here should be $\overline{0}$

capture1

automaton777 commented 3 months ago

This isn't a typo. The $\mathtt{0}$ here is written in a different font from the metalanguage 0, so it's syntactically identical to $\overline 0$, which you can see if you look at the recursive definition of numerals on page 313 in the current build of Sets, Logic, Computation.

However the usage in this part of the book is very inconsistent so it makes sense that you were confused. The text continually switches between the object language $\mathtt{0}$ (as shown above) and the notation $\overline 0$ throughout the sections on Representing Turing Machines, Verifying the Representation, The Decision Problem Is Unsolvable, and Trakthenbrot's Theorem. It would make sense to pick one notation and standardize the usage.

rzach commented 3 months ago

Alright, I'll fix this.

automaton777 commented 3 months ago

Very minor additional issue I noticed here — “Trakhtenbrot” is the correct spelling (see https://en.wikipedia.org/wiki/Boris_Trakhtenbrot), but it is misspelled in the relevant section as “Trakthenbrot.”

automaton777 commented 3 months ago

Oh and one further note while I’m looking at this section — the editorial for the Turing Machines section says: “The proof of the unsolvability of the decision problem uses a successor function, hence all models are infinite.”

But I’m pretty sure this is no longer true since the text was revised to drop injectivity of successor and irreflexivity of < and add discussion of Trakhtenbrot’s Theorem.