How can a system state its own consistency within its own language?

Question

Gödel's incompleteness theorem says that formal arithmetic can't prove its own consistency, but how can formal system even state its own consistency with its own language/semantics ?

Answer 1

There is no easy answer to this question; indeed, the answer is the bulk of Godel's proof, and the whole key idea. That said, below I'll try to shed some light on the issue.

---

In my opinion a useful analogy here is: "How can a computer talk about the physical world?" On the one hand, "obviously" $0$s and $1$s can't rise to the level of referring to the actual real world; on the other hand, video games. Bridging this paradox is pragmatism - the realization that at the end of the day, we don't need to dive too much into what "talk about" means, but just focus on the concrete issues we care about.

A more directly self-referential example would be to talk about computers simulating computers, but I think that has less "oomph" than the above example.

---

OK, on to the actual question! Suppose I have a function $f$ from the set of sentences in the language of arithmetic to $\mathbb{N}$. Any set $S$ of sentences yields a set $f(S)$ of natural numbers. Here's the key idea:

We want a function $f$ from the set of sentences in the language of arithmetic to $\mathbb{N}$ such that for "lots" of sets of sentences $S$, the set $f(S)$ is definable in the language of arithmetic.

We'll actually want more than that:

We'll want to be able to prove in PA the arithmetic statements corresponding, via $f$, to basic facts about how various natural sets of sentences interact.

For example, let $S$ be the set of PA-theorems. Then:

• We want $f(S)$ to be a definable subset of $\mathbb{N}$ - in fact, we want a specific formula $\varphi$ defining it. Note that now "Con(PA)" is just an abbreviation for "$\neg\varphi(\underline{f(0=1)})$"

(Here "$\underline{n}$," for $n$ a natural number, denotes the numeral corresponding to $n$; e.g. $\underline{2}$ is the expression "$S(S(0))$." The point is that $2$ itself is not a symbol in the language of arithmetic, so technically "$\varphi(2)$" isn't meaningful.)

• We want PA to prove - for all sentences $\psi_0,\psi_1$ in the language of arithmetic - the sentence $$\varphi(\underline{f(\psi_0)})\wedge \varphi (\underline{f(\psi_0\implies\psi_1)})\implies \varphi(\underline{f(\psi_1)}).$$ This just reflects "If PA proves $\psi_0$, and PA proves $\psi_0\implies \psi_1$, then PA proves $\psi_1$."

This is of course just one instance of what we're trying to do. The point is that a good choice$^*$ of $f$ tells us how to express various claims about sentences as statements of arithmetic and to prove some of them in PA; we can then juggle between the arithmetic level and the meta level via this translation. The details are complicated and you should read a good exposition of the theorem to see exactly what happens - e.g. Peter Smith's book - but this is the basic idea.

---

$^*$Godel's argument begins by picking one specific map, the Godel numbering scheme. Of course there's no claim that it's the only choice of $f$ that works, but it's a good one.

Meanwhile, the question of distinguishing "good" interpretations from "bad" interpretations more generally is a big one in mathematical logic, and there's a lot of work on this. This old question mentions one particular issue, and you may also be interested in this paper of Halbach and Visser.