Join GitHub today
GitHub is home to over 28 million developers working together to host and review code, manage projects, and build software together.Sign up
More motivation in "Arithmetization of Syntax" #67
Smith: "Ch. 14 is on the Arithmetization of Syntax. It is difficult to do this stuff with a light touch, and (as elsewhere in OLT) I’d go for adding quite a lot more arm-waving motivation, here along the lines of “Look, consider the relation Pr(p, n) which holds when p codes for a well-formed proof in Q of the wff with number n. It’s easy to see that you can check whether Pr(p, n) without going in for any open-ended searches; here, informally, is how. So Pr is going to be primitive recursive, right?”"