What does the expression "contains arithmetic" in the second Gödel incompletenetss theorem mean exactly?

The second Gödel incompletenetss theorem is often formulated as follows:

Assume F is a consistent formalized system which contains elementary arithmetic. Then F ⊬ Cons(F).

Can anybody enlighten me, what is meant by the word "contains" here? I think that in the case when $F$ is a variant of an axiomatic set theory the "containing" means that the Peano arithmetic has a model in $F$. Apparently, in the general case people have in mind a similar construction, but I don't know the exact formulations. Could you, please, clarify this (and give me a reference)?

The key is that the theory in question should be able to talk in some way about natural numbers; this amounts essentially to representing every primitive recursive function, and to being able to prove enough about the version of the natural numbers talked about by the theory.

One approach is via interpretations in the model-theoretic sense, although the version of "interpretation" I use is slightly different. For simplicity, assume all languages have relation symbols only; we can "relationize" a non-relational theory by replacing every function with its graph, so this is a benign assumption. If $T, S$ are theories in languages $\Sigma_0,\Sigma_1$, we say that $T$ interprets $S$ if there are formulas $\varphi, \psi_\sigma (\sigma\in\Sigma_1)$ with the following properties:

• $\varphi$ has a single free variable; the idea is that $\{x: \varphi(x)\}$ should correspond to the elements of a model of $S$.

• $\psi_\sigma$ has a number of free variables corresponding to the arity of $\sigma$: e.g. if $\sigma$ is a $3$-ary relation symbol, $\psi_\sigma$ should have three variables.

• $T$ proves $\forall x_1, ..., x_n[\psi_\sigma(x_1, ..., x_n)\implies \varphi(x_1)\wedge ...\wedge \varphi(x_n)$. This is a benign requirement: we could always replace $\psi_\sigma(x_1, ..., x_n)$ with $\psi_\sigma'(x_1, ..., x_n)\equiv [\varphi(x_1)\wedge ... \wedge\varphi(x_n)\wedge\psi_\sigma(x_1, ..., x_n)]$.

• For each sentence $\theta$ in the language $\Sigma_1$, if $S\vdash\theta$ then $T\vdash Translate(\theta)$, where $Translate(\theta)$ is the translation of $\theta$ into the language $\Sigma_0$ via the $\psi_\sigma$s; we relativize everything to $\varphi$ and replace each $\Sigma_1$-symbol with its corresponding $\psi$. E.g. $$"\forall x, y(R(x, y)\implies R(y, x))"$$ would become $$"\forall x, y(\varphi(x)\wedge \varphi(y)\implies(\psi_R(x, y)\implies \psi_R(y, x)))."$$

Note that we might have $T$ prove things which $S$ doesn't; we just require that $T$ prove at least the things $S$ proves. We'll say an interpretation is effective if:

• (i) The languages $\Sigma_0,\Sigma_1$ are recursive.

• (ii) The set $\{\varphi\}\cup\{\psi_\sigma: \sigma\in\Sigma_1\}$ is recursive.

• (iii) The theories $T$ and $S$ are each recursive.

Now the key point is: if we have an effective interpretation, then $$T\cap \{Translate(\theta): \theta\in Sentence(\Sigma_1)\}$$ is a computable subset of $T$, but from it we can extract a computable extension $S'$ of $S$. If $T$ is complete, then $S'$ would be complete as well.

So now we can state the following generalized version of Goedel's first incompleteness theorem:

Suppose $T$ is a consistent theory which effectively interprets the relational version of Robinson's Q. Then $T$ is incomplete.

(Remember that "effectively interprets" means that $T$ is recursively axiomatized - clause (iii)!) I've used Robinson's Q here since it's basically the weakest thing we can use here; the driving fact about it is that it is essentially undecidable, meaning that any consistent extension of it is undecidable (and in particular it has no recursively axiomatizable completions).

The shift to relational languages makes defining "$Translate(\theta)$" easier; it also means that the above can be applied to theories without "enough terms," like ZFC. I make no claim that the version above is optimal (indeed, it's easy to show that it isn't), but it is true, gives a meaning to "contains enough arithmetic," and is strong enough for every practical purpose I'm aware of.

• Noah, I believe that there is a simpler explanation. What you say is an analysis of the proof, but for formulating this theorem it is desirable to hide the proof behind the curtain, leaving for the audience the formulation in its simplest (but of course, rigorous) form. I am sure it is possible to explain this without recursive functions. For example, as far as I understand, for formulating this theorem for ZFC there is no need to refer to recursive functions, it is sufficient to construct a model of PA in ZFC, is that right? Jun 3, 2017 at 20:04
• @SergeiAkbarov Yes, but that's a huge thing! Note that theories of arithmetic don't contain models of even much weaker theories of arithmetic - a model of such a theory is an infinite set (with some properties), and theories of arithmetic can't get at these in any but the most roundabout ways. It is of course sufficient to construct a model of arithmetic inside you, but that's massive overkill. (cont'd) Jun 3, 2017 at 20:07
• You asked "Can anybody enlighten me, what is meant by the word "contains" here?" I stand by my answer - while we may colloquially use it to mean "has a model of PA" when talking about certain specific theories, the general meaning is that PA (or enough of arithmetic) can be "embedded" into the theory in a precise way; and that way basically amounts to what I've written. Jun 3, 2017 at 20:10
• @Sergei Not quite. The key is the ability to code in the theory meta-theoretic notions and recursive operations between these objects. Even the most "semantic" presentations of the theorem do this. (The issue is subtle. The point is that, for instance, it is different to claim that there is a model from saying that a theory proves that there is a model. The former is semantics, the latter is syntactic and requires more careful coding of notions than just model-theoretic ones.) Jun 3, 2017 at 20:14
• Noah, I would indeed prefer the word "interpretation" (or "embedding"). What does it mean here exactly, and which reference can I put into my text? Jun 3, 2017 at 20:14

The important property is that it must be possible to express primitive recursive arithmetic in the theory. A possible way of formalizing this is to require that

• For each natural number $n$ there is a formula $\psi_n(x)$ such that $T$ proves $\exists x.\psi_n(x)$. (Intuitively $\psi_n(x)$ represents "$x$ is the number $n$").
• For natural numbers $n\ne m$, $T$ proves $\neg(\psi_n(x)\land \psi_m(x))$.
• $\psi_n$ can be constructed mechanically given $n$ (that is, the Gödel number of $\psi_n(x)$ must be a primitive recursive function of $n$).
• For every primitive recursive function $f(x_1,\ldots,x_k)$ there must be a formula $\varphi_f(x_1,\ldots,x_k,y)$ such that for every $n_1,\ldots,n_k$, $T$ proves $$\psi_{n_1}(x_1)\land\cdots\land \psi_{n_k}(x_k) \to \bigr[\varphi_f(x_1,\ldots,x_k,y) \leftrightarrow \psi_{f(n_1,\ldots,n_k)}(y)\bigr]$$

These conditions will in particular be satisfied if there is a way to translate formulas of arithmetic into the language of $T$, such that $T$ proves the translations of the axioms of Peano Arithmetic -- or even just the axioms of Robinson's Q (which don't include induction).

This assumes that $T$ is a theory in standard first-order logic. We can make it even more abstract by just requiring that the formal system can express (in a systematic way) enough logical connectives and deductions to make the constructions in the proof go through -- but I don't have a ready list of which ones that is.

Whoops, that was not completely correct. The above is enough to prove the first incompleteness theorem. For the second one you also need some amount of induction. Induction on existentially quantified formulas of primitive recursive arithmetic should be enough, though.

• Hm... This looks too complicated for me. I would expect that this can be formulated with the help of a proper generalization of the notion of "model" (or "interpretation"). Jun 3, 2017 at 14:17