Adil Sanaulla has emailed to point out that the Proof Sketch at the bottom of p. 178 of IGT is flawed. I cheerfully say [with an obvious slight change of notation] that “it will be easy to prove that the Sigma_1 wff NPrf(w, x) is equivalent to the Pi_1 wff (Az)(NPrf(w, z) –> z = x)“, which is just false. Suppose w is such that NPrf(w, z) is false for every z because w is not a super Gödel number. Ouch. I guess I must have been bamboozled by Theorem 13.1, unthinkly applying the same argument while forgetting that NPrf(w, x) is not functional.
I wonder what the minimum mutilation repair is …
Something like “it will be fairly easy to prove that the Sigma_1 wff NPrf(w, x) is equivalent to a Pi_1 wff of the form Sg(w) ^ (Az)(NPrf(w, z) –> z = x), where Sg(w) says that w is a super Gödel number” should work, but isn’t pretty.