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

Question

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

Answer 1

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.

Answer 2

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.