# Gödel without recursion

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).

• I haven't gone over your wording in dense detail, but your propositions look like fairly standard components of a Gödel exposition. (They correspond roughly to the three Hilbert-Bernays derivability conditions, in a different order and modified for other rules of inference than modus ponens). Are you looking for an answer that contrasts them specifically to the development in the particular book you mention? Jul 10, 2021 at 18:28
• @Troposphere yes, these "Hilbert–Bernays provability conditions" look exactly like Takeuti's Proposition 10.9. I must confess that I don't understand how Takeuti proves this. Is this proved in P.Smith's book (mentioned in this Wikipedia article)? Jul 10, 2021 at 18:46
• Smith's book itself might not provide the level of detail you desire. There's a footnote referring a bit testily to "the very brief gestures towards proofs in e.g. Boolos (1993, p. 44) and Takeuti (1987, p. 86)", so apparently he shares your judgment of Takeuti. For the actual gory details the same footnote states: "Masochists who want to complete the story for themselves can start by looking at Grandy (1977, p. 75) for a few more details. See also Rautenberg (2006, Sec. 7.1)." [The book is free for download on Smith's website, so you can follow these references at your own leisure]. Jul 10, 2021 at 19:17
• @Troposphere excuse me, are you saying that Rautenberg's book is available at Smith's website? logicmatters.net/about Jul 11, 2021 at 6:31
• No, Smith' book is -- which I why I didn't bother to find and reproduce the bibliography entries whose references I quoted. Jul 11, 2021 at 11:29