Today’s short episode is a second ‘Interlude’, separating the chapters on the first incompleteness theorem from the final three chapters on the second theorem. But it mentions (or at least, gestures at) enough interesting points for it to be worth its own post.
[There a reference to a Theorem 51, which is the previously unnumbered result — now indeed to be recognized as a theorem in its own right — at the end of §13.3. which says that if a theory T is p.r. axiomatized and contains Q, the formal predicate ProvT does not capture the property of being a T-theorem.]
[Link now removed]
On the last point in particular, yes. Was careless to use “elementary” (ambiguous between “easy” and something like “using only finitary concepts”). Will rephrase.
p 104, “The primitive recursive functions are the numerical functions that can be computed without open-ended searches” —
I think it’s good that there’s no mention of ‘for’ loops there. Indeed, I think the ‘for’-loop connection should be explained once, and then it’s better to talk just of open-ended or bounded searches, rather than continually adding something about ‘for’ loops.
p 105, “introducing a minimization operator” — We already have bounded minimisation, though, don’t we? This section reads as if we don’t.
p 105, footnote 2. — Is it so odd if we know (as in footnote 1) that the search will always succeed? It just means we haven’t computed a specific bound in advance. A great many things are written that way in ordinary programming languages. (I gave an example in my comments on Slowly, 11.)
p 107, “It would take us too far afield to define the Goodstein function; and neither the proof that it really is a total function nor the proof that it isn’t provably- total-according- to- PA is elementary.” —
Just want to check what “elementary” means. Mathematical use of “elementary” doesn’t always have a meaning that would be obvious to the uninitiated. (For example, when “elementary” means without using complex numbers.)