Gödel without recursion

Question

I am reading books on logic, and I got an impression that the main Gödel's technical results necesary for his incompleteness theorems can be formulated (but apparently not proved, only formulated) without mentioning of recursive functions. In particular, in Takeuti's book Proposition 10.9 (which in my opinion is proved very vaguely) can be more or less easily proved with the help of the following two propositions (which I believe can be attributed to Gödel):

Theorem 1. Assuming consistency of PA, for each theory $\mathcal S$ with a given numeration $\ulcorner \cdot \urcorner$ of its Gentzen trees, there exists a formula in PA, that defines a predicate symbol $\operatorname{Prf}$ of arity 2 with the following two rpoperties:

(i) for each formula $\varphi$ in $\mathcal S$ and for each Gentzen tree ${\mathcal K}$ in $\mathcal S$ the formula $$ \operatorname{Prf}(\ulcorner {\mathcal K} \urcorner,\ulcorner \varphi \urcorner) $$ is deducible in PA if and only if the Gentzen tree ${\mathcal K}$ is a deduction of the formula $\varphi$ (or what is the same, of the sequent $\vdash\varphi$) in $\mathcal S$,

(ii) each Gentzen tree $\mathcal K$ (of metaformulas) in LK with the language of $\mathcal S$, that expresses deducibility of the metaformula $\psi$ from some metaformulas $\varphi_1$,...,$\varphi_n$ (i.e. a Gentzen tree with $n$ vetrtexes $\vdash\varphi_1$,...,$\vdash\varphi_n$, and perhaps with other vertexes which are axioms of the theory LK with this language, i.e. which have the form $\alpha\vdash\alpha$, and with the root $\vdash\psi$), $$ {\mathcal K}\ : \quad \frac{\frac{\vdash\varphi_1}{\dots}\quad ...\quad \frac{\vdash\varphi_n}{\dots}\quad ...}{\vdash\psi}, $$ generates a formula in PA, that defines an adjoined functional symbol $F_{\mathcal K}$ of arity $n$, such that for each values of the metavariables in $\varphi_1$,...,$\varphi_n$ and in $\psi$ the following sequent is deducible in PA: $$ \operatorname{Prf}(y_1,\ulcorner \varphi_1 \urcorner),...,\operatorname{Prf}(y_n,\ulcorner \varphi_n \urcorner) \vdash \operatorname{Prf}(F_{\mathcal K}(y_1,...,y_n),\ulcorner \psi \urcorner) $$ (in other words, if with the given values of metavariables in $\varphi_1$,...,$\varphi_n$ and in $\psi$ the objects $y_1,...,y_n$ are Gödel numbers of the deductions for the formulas $\varphi_1$,...,$\varphi_n$, then $F_{\mathcal K}(y_1,...,y_n)$ is the Gödel number of the deduction of the formula $\psi$).

And

Theorem 2. Suppose $\mathcal S$ is a theory with a given numeration $\ulcorner \cdot \urcorner$ of Gentzen trees, and at the same time $\mathcal S$ interprets the Peano arithmetics PA. Then there exists a formula in $\mathcal S$ that defines an adjoined functional symbol $\operatorname{Ded}$ of arity 1, such that in $\mathcal S$ the following sequent is deducible: $$ \operatorname{Prf}_{\mathcal S}(y,\ulcorner \varphi \urcorner)\vdash \operatorname{Prf}_{\mathcal S}(\operatorname{Ded}(y),\ulcorner \operatorname{Prf}_{\mathcal S}(y,\ulcorner \varphi \urcorner)\urcorner) $$ (in other words, if $y$ is the Gödel number of a deduction of the formula $\varphi$, then $\operatorname{Ded}(y)$ is the Gödel nuber of a deduction of the formula $\operatorname{Prf}_{\mathcal S}(y,\ulcorner \varphi \urcorner)$).

I hope, everything is more or less clear. By metavariables I mean the symbols of some new alphabet, which does not intersect with the alphabet of $\mathcal S$, and the metaformulas are defined as sequences of symboles composed from usual formulas in $\mathcal S$ and from metavariables, which are suposed to be places for new formulas (and can be replaced by usual formulas). Also $\operatorname{Prf}_{\mathcal S}(y,x)$ means the translation in $\mathcal S$ of the formula $\operatorname{Prf}(y,x)$ in PA.

My question is

if there exist a text which can be used as a reference for these two propositions?

As I wrote, I am interested in this because I think that there are simpler (than in Takeuti's book or in Mendelson's book) schemes of proving Gödel's incompleteness theorems. If we state these two theorems then the rest of the proof becomes more or less simple, that is why I believe that there must be texts on logic where these two propositions are mentioned (maybe in a different form, but anyway with this translation into the language of sequent calculus). I would be grateful if somebody could give such references (or maybe just some advises).

Answer 1

Two quick points.

1. "The main Gödel's technical results necesary for his incompleteness theorems can be formulated ... without mentioning of recursive functions." That's not accurate. To be sure we can state the incompleteness theorem for PA (or ZFC, or other particular theories) without mentioning recursive functions. But what we normally think of as Gödel incompleteness theorems are general claims (of the kind that Gödel himself made) along the lines of "Any recursively axiomatised theory which contains enough arithmetic is negation incomplete", and to state such general claims we need the notion of being recursively axiomatised (and hence the notion of a recursive function is there in setting up the very statement of the theorem).

2. But yes, for a particular case, like proving the incompleteness of PA, we don't need to invoke recursive functions. Instead of proving (a) that certain arithmetised syntactic relations are recursive, and (b) PA can represent all recursive functions, so (c) PA can represent arithmetised syntax, we can more directly show how PA can represent the syntactic relations we need. Leary and Kristiansen, for example, do this in their excellent (freely downloadable) A Friendly Introduction to Mathematical Logic. See my note on this book here: https://www.logicmatters.net/tyl/booknotes/leary/