0

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.

nontology
  • 19
  • "The passage starts in a way that seems to imply that the set of provable formulae is recursive. " No, the passage says that the set of provable formulas is semi-recursive. Do you know the difference? In a nutshell - applied to provability - recursive means that we have a procedure that, starting with a formula whatever, answer in a finite number of steps with Yes or No, according to the fact that the formula is provable or not. – Mauro ALLEGRANZA Aug 22 '22 at 06:41
  • semirecursive means that we have a procedure that "produces" (in a finite number of steps) every theorem. The procedure is: list all derivations in increasing length: (1) all derivations of length 1: the axioms. (2) length 2: formulas derivable from axioms with a one-premise rule (Gen), and so on. – Mauro ALLEGRANZA Aug 22 '22 at 06:43
  • Conclusion: IF the set of axioms is recursive (that means that we can always "ascertain" in a finite number of steps if a formula is an instance of an axiom) then we can "produce" mechanically all theorems, that means that "the set of sentences that are provable" is semirecursive. – Mauro ALLEGRANZA Aug 22 '22 at 06:45
  • Useful to compare with other sources: P.Smith, page 140: "To determine $\text {Prf} (m, n$), proceed as follows. First doubly decode $m$: that’s a mechanical exercise. Now ask: is the result a sequence of wffs? That’s algorithmically decidable (since it is decidable whether each separate string of symbols is a wff). If it does decode into a sequence of wffs, ask: is this sequence a properly constructed proof in the particular proof system of logic that you have fixed on in your official version of $\mathsf {PA}$ ? – Mauro ALLEGRANZA Aug 23 '22 at 11:26
  • That’s decidable too (check whether each wff in the sequence is either an axiom or is an immediate consequence of previous wffs by one of the rules of inference of the system). If the sequence is a proof, ask: does its final wff have the g.n. $n$? That’s again decidable. Putting all that together, there is a computational procedure for telling whether $\text {Prf (m, n)}$ holds. Moreover, it is again clear that, at each and every stage, the computation involved is once more a bounded procedure." Conclusion of the informal argument above: $\text {Prf}(m,n)$ is primitive recursive. – Mauro ALLEGRANZA Aug 23 '22 at 11:28
  • The second part of the recipe is the result (Smith, page 129) that in $\mathsf Q$ and similar we can express primitive recursive functions by fomulas called $\Sigma_1$-type i.e. formulas built from a matrix that uses only connectives and bounded quantifiers prefixed by (unbounded) existential one. Thus, $\text {Prf}(m,n)$ is $\Sigma_1$ and $\text {Prv}(m) = \exists y \text {Prf}(m,y)$ is $\Sigma_1$. – Mauro ALLEGRANZA Aug 23 '22 at 11:31
  • Conclusion: the set of provable formulas is semirecursive (and not recursive) because we get it form a primitive recursive predicate by way of unbounded existential quantification. Maybe your concern can be answered noting that the text above reads: we have to say " 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 [functions] are definable by ∃-rudimentary formulas." The link between the two is through an existential quantifier. – Mauro ALLEGRANZA Aug 23 '22 at 11:58
  • Thank you Mauro for your excellent attention to my question! I knew that Prf(m, n) is p.r., but the issue is to show that it is rudimentary. Also, I understand why Prf(m,n) is Σ1-type (what Boolos et al. call generalized ∃-rudimentary), but again, my question is how to show that it is rudiementary (a.k.a. a Delta-0 formula). – nontology Aug 24 '22 at 09:04
  • I corresponded with Burgess, and he noted that what he calls a "proof predicate" is NOT a predicate which intuitively means "n codes a proof of the formula coded by m." Rather, his sort of proof predicate intuitively means "n is a witness to the provability of the formula coded by m." If we read things that way, then I now understand why such a "proof predicate" must be rudimentary by the argument from Boolos et al. Moreover, it may be that the proof predicate in the normal sense cannot be shown rudimentary. – nontology Aug 24 '22 at 09:07
  • Peter Smith's book Theorem 20.7 The relation $\text {Prf} (m, n)$, which holds when m is the super g.n. of a $\mathsf {PA}$ proof of the sentence with g.n. n, is primitive recursive. (starting page 151). – Mauro ALLEGRANZA Aug 24 '22 at 09:08
  • It seems to me that in BBJ the result is only sketched in Ch.15 on Arithmetization of Syntax. – Mauro ALLEGRANZA Aug 24 '22 at 09:14

0 Answers0