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


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

  • 1
    $\begingroup$ 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? $\endgroup$ Jul 10, 2021 at 18:28
  • $\begingroup$ @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)? $\endgroup$ Jul 10, 2021 at 18:46
  • 1
    $\begingroup$ 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]. $\endgroup$ Jul 10, 2021 at 19:17
  • $\begingroup$ @Troposphere excuse me, are you saying that Rautenberg's book is available at Smith's website? logicmatters.net/about $\endgroup$ Jul 11, 2021 at 6:31
  • 1
    $\begingroup$ No, Smith' book is -- which I why I didn't bother to find and reproduce the bibliography entries whose references I quoted. $\endgroup$ Jul 11, 2021 at 11:29

1 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/

  • $\begingroup$ Peter, thank you for the answer. I did not write this in the question, but my idea was that we can restrict ourselves to the theories with finite set of axioms and finite set of schemes of axioms. All the "theories for the working mathematician" that I know are like this. So actually there is no need to pronounce the words "recursive" or "recursively axiomatized" before proving the two propositions that I stated. $\endgroup$ Jul 11, 2021 at 20:09

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.