I just read the following sentence:
"[T]here is no effective decision procedure for determining whether or not an argument T/X is valid, where T is any subset of PA or RA and X is any sentence."
I don't understand how this squares with the fact that proof[m, k] is recursive, where m is the Godel number of a derivation of sentence with Godel number k. For any alleged proof of X from T, can't we decide in a finite number of steps whether it's a proof in fact? Isn't this what the quoted sentence denies? Thanks!
[I now mention the source and context of the quote below.]
Given the context of a paragraph on page 257, from which the quote is taken, the author is only saying that it is not decidable whether a given sentence follows from a given set of axioms of PA. The paragraph is all about logical validity, not about checking particular proofs. When the author writes "An argument T/X" I believe the meaning is simply "the claim that X is a logical consequence of T". Just before the quote, the author writes "There are many decidable PL sets such that the sets of all their logical consequences are undecidable". The reference to PA is meant to be an example of that phenomenon.