2
$\begingroup$

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 ?

$\endgroup$
2
$\begingroup$

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.

$\endgroup$
  • $\begingroup$ Can this way of stating consistency be generalised to any formal system of axioms ? $\endgroup$ – Юрій Ярош Apr 7 '18 at 19:58
  • $\begingroup$ @ЮрійЯрош Well, it takes effort to make that question precise. The short version: any simply describable set of axioms can be handled this way. Specifically, take $f$ to be Godel's original numbering translation. Then we can express the consistency of $T$ in the above way as long as $T$ is a theory which is arithmetically definable via $f$ - that is, such that the set $\{f(\varphi): \varphi\in T\}$ is definable. Since $f$ is so natural and intuitively computable, we often just say that $T$ is arithmetically definable. (cont'd) $\endgroup$ – Noah Schweber Apr 7 '18 at 20:02
  • $\begingroup$ A particularly important case is when $T$ is computably axiomatizable - that is, when the set $\{f(\varphi): \varphi\in T\}$ is computably enumerable. The key improvement of "computably axiomatizable" over "arithmetically definable" is that PA can prove more (translated) facts about theories of the former type than the latter. One key word here is "representability." As a concrete difference, the second incompleteness theorem only applies to computably axiomatizable theories. $\endgroup$ – Noah Schweber Apr 7 '18 at 20:05
  • $\begingroup$ Honestly enough, your answer gotten me curios, but to the mathematical logic. Because my knowledge in it, is not enough for fully understanding your answer. But still, thanks for the answer. $\endgroup$ – Юрій Ярош Apr 7 '18 at 20:13

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.