In the first part of chapter 3 'figure and ground', Hofstadter is discussing a formal system to represent multiplication, then making use of this system to create another for composite numbers.
RULE: suppose x, y, and z are hyphen strings. If x - ty - qz is a theorem, then Cz is a theorem.
This seems well enough so far to me. He goes on to propose a rule for generating primes :
PROPOSED RULE: suppose x is a hyphen string. If Cx is not a theorem, then Px is a theorem.
He then says that this rule won't do, that it is not an explicitly typographical operation. He says that it has similar problems to the MIU system of chapter 1, namely, as I understood it, that to test whether a string was a theorem involved a 'test' which might take an infinite time to complete; concluding that the string MU could not be attained required thinking 'outside the system'.
But here it seems to me, and this is where I suspect I'm mistaken, that it would be possible to take any string of the form Cz and perform a sort of bottom up decision procedure within his tq-system for multiplication to find if any string x - ty - qz is a theorem.
Simply by starting with - - t - q - - and applying the rule of inference proceeding until the third hyphen string is z itself or comes to exceed z. If it equals z you've shown Cz is a theorem and Pz is not, if it comes to exceed z then start from the next simplest axiom, - - - t - q - - - and repeat the procedure. If you haven't shown theoremhood by the time you've reached the axiom zt - qz, then Cz must not exist and Pz is a theorem.
This procedure seems finite to me no matter what string Cz you consider, and thus seems to qualify as a proper bottom up decision procedure. Perhaps though, it is the last step in reasoning, that if you reach the axiom zt - qz you've gone too far that qualifies as thinking 'outside the system' and violating his requirement of formality? Are all decision procedures based on thinking 'outside the system'? If my procedure is sound, what disqualifies it as a decision procedure? I'm certainly a little confused on these ideas.
It is particularly concerning to me because at the end of the chapter he describes using a decision procedure to generate all the nontheorems of a system, explaining that this would qualify as a typographical method for generating the set of nontheorems! So somehow this isn't possible with his system of describing composite numbers but I'm having trouble seeing the reason.
Sorry if I was confusing, I know I left too much unexplained for those who haven't read the book to properly understand, but I'm not sure I understand what I've read well enough to give a proper explanation in those cases. Thanks for those who read the whole thing and especially anyone who tries to explain it to me!