gesang reviewed Incompleteness and Computability by Open Logic Project (Open Logic Project)
Mediocore
3 stars
The version I read is $F21\alpha$. I skipped the second-order logic chapter.
It has been years since Open Logic Project started their textbook project, but the text is still cluttered. Early on, on page 10, there's a mysterious $s$ appearing without any explanation, which, though, can only be thought of as a function that maps a variable, there $x$, to an element of the model, is still frustrating to read. Also maybe because the text if designed for philosophy students, the notion of /computable function/ is distinguished from /partial recursive function/ here, and that introduces unnecessary confusions. I prefer Cutland's approach, which is really clear.
The exposition of Goedel's theorem is mediocore. It's a text for philosophy students, not for real logicians, so no introduction of $\Sigma^0_1$-sentences, etc., which are the more important concepts if one really wants to see what's going on: $\Sigma^0_1$- and $\Pi^0_1$-formulas do not match, co-r.e. …
The version I read is $F21\alpha$. I skipped the second-order logic chapter.
It has been years since Open Logic Project started their textbook project, but the text is still cluttered. Early on, on page 10, there's a mysterious $s$ appearing without any explanation, which, though, can only be thought of as a function that maps a variable, there $x$, to an element of the model, is still frustrating to read. Also maybe because the text if designed for philosophy students, the notion of /computable function/ is distinguished from /partial recursive function/ here, and that introduces unnecessary confusions. I prefer Cutland's approach, which is really clear.
The exposition of Goedel's theorem is mediocore. It's a text for philosophy students, not for real logicians, so no introduction of $\Sigma^0_1$-sentences, etc., which are the more important concepts if one really wants to see what's going on: $\Sigma^0_1$- and $\Pi^0_1$-formulas do not match, co-r.e. sets are not r.e if they're not $\Delta_1$. It's THAT simple. The intuition behind sencond incompleteness is also simple: consistency should be characterized by $\Pi^0_1$-formulas, existential quantifier has nothing to do with consistency, hence they're not $\Delta_1$.
After all Goedel's theorem, in its traditional form, is a very /boring/ theorem to go through. Most of the energies are spent in coding symbols and terms and functions, and representing partial recursive functions in $\mathsf{Q}$. The main argument is the fixed-point argument which is, though buried by technical details, is fairly easy to grasp, while, similar to Yoneda's lemma, becomes confusing when really working with (in particular when it comes to Lob's theorem). Cutland in his chapter 8 proves the first incompleteness beautifully, in contrast, with the help of creative and productive sets, which is far more illuminating than the original proof. And Cutland's book doesn't abuse the word "true" like philosophers do, by the way, which is still present in the Open Logic text. But I think it's better than some classics /that the textbook copy-pastes a lot/ like /Boolos, Burgess, Jeffrey/.
Still, for beginners, they may want to read this text, since other books may not mention that partial recursive functions are already representable in $\mathsf{Q}$ and go straightforward to $\mathsf{PA}$.