I asked about this before here, but I am still not clear on something.
In Boolos, Burgess, and Jeffrey (2007, 5th edition), the following statement is found on p. 224:
"[Consider] that the set of sentences that are provable and the set of sentences that are disprovable from any recursive set of axioms is semirecursive, and that all recursive sets are definable by ∃-rudimentary formulas. It follows that there are formulas PrvT (x) and DisprvT (x) of forms ∃y PrfT (x, y) and ∃y DisprfT (x, y) respectively, with Prf and Disprf rudimentary, such that A is a theorem of T if and only if the sentence PrvT ( A ) is correct or true in the standard interpretation."
The passage starts in a way that seems to imply that the set of provable formulae is recursive. That of course is incorrect. Regardless, there is another way to show that the provability relation is defined by an ∃-rudimentary formula. The problem, however, is that this alternate argument gets us to an ∃-rudimentary formula in which the unbound existential quantifier does not attach to PrfT (as the Boolos et al. argument would suggest); rather, it attaches to something else that is rudimentary. (Details below.) So I still don't know how we can show that PrfT in particular must be rudimentary.Can you help?
The altnernate argument to show that provability is defined by an ∃-rudimentary formula is as follows. We at least know that PrfT(x,y) defines a recursive set; hence, we know that PrfT(x,y) is an ∃-rudimentary formula. Suppose in more detail that PrfT is ∃zF(x,y) wherein 'x' and 'y' remain free. It is clear that ∃y∃zF(x,y) would then be a provability predicate and a generalized ∃-rudimentary formula. Now: Using Boolos et al.'s 16.10 proposition on p. 206, we can then infer that ∃y∃zF(x,y) is arithmetically equivalent to an ∃-rudimentary formula of the form ∃w∃y<w∃z<wF(x, y). (See Boolos et al.'s proof of proposition 16.10 on pp. 205-206.) But in this case, the unbound quantifier does not attach to the proof predicate ∃zF(x,y), but rather to a different rudimentary formula, ∃y<w∃z<wF(x,y). So as I mentioned above, it doesn't seem enough to show that the proof predicate itself is rudimentary. After all, ∃y<w∃z<wF(x,y) is NOT arithmetically equivalent to ∃zF(x,y) since they don't even have the same free variables.
Again, this was just to elaborate on why Boolos et al's argument can't be easily revised to show that there is a rudimentary proof predicate. So my primary question remains: How DO you show that the proof predicate is rudimentary? Thanks in advance.