Characterization of provably recursive functions in PA

101 Views Asked by At

This concerns Takeuti's Proof Theory: the book contains a lot of wonderful material, but the presentation is sometimes lacking (and so many typos!). At least that has been my experience so far, unfortunately. Well, the question concerns the proof of corollary 12.16:

Suppose $R$ is a primitive recursive predicate and there is a proof of $\to \exists x R(a, x)$ in $\text{PA}_k$ with ordinal $< \omega_k(l)$ for some numbers $k$ and $1$ (as defined just above Definition 12.6). Then the number-theoretic function $f$ defined by $$f(m) = \text{the least $n$ > such that } R(m, n)$$

is $<\!\cdot$-primitive recursive, where $<\!\cdot$ is the initial segment of the standard ordering of $\epsilon_0$ of order type $\omega_k(l)$.

In the proof Takeuti claims

We (temporarily) call a proof reducible if it is a proof in $\text{PA}_k$, with ordinal $\omega_k(l)$ containing an essential cut or ind, and with end-sequent satisfying [property] P [of Problem 12.11]. If $P$ [a proof] is reducible, then by applying repeatedly the reduction procedure of Lemma 12.8 (modified for $\text{PA}_k$, as in Remark 12.14), we obtain a proof in $\text{PA}_k$, of the same sequent, without an essential cut or ind.

First of all very confusing that the symbol P is overloaded for an arbitrary proof and the property described in Problem 12.11. This is problem 12.11:

Problem 12.11

I highlighted two aspects of this problem that are confusing to me:

  1. In my Dover edition the $\exists$ underlined in red is a $\forall$ (the screenshot is of the original first edition). What should it be?
  2. Is the section highlighted with blue still part of the problem? Very confusing since Takeuti doesn't separate proofs, problems, and discussions very well.

Now the main question: Lemma 12.8 refers to the reduction part of Gentzen's (second) proof for the consistency of PA (if there is a proof of $\to$ then there is one with a smaller ordinal). But that doesn't in itself at all yield a proof of $\to \exists x R(a, x)$ that is without essential cuts and ind (induction). So presumably Takeuti intends to use Problem 12.11 (although he doesn't really say that), but I have no idea how that is proved... is my analysis of the situation correct? Did I understand Takeuti correct? Can you please show how to solve 12.11?

(Takeuti is so confusing sometimes... yes, I'm a little frustrated lol)