17
$\begingroup$

The entry on Gödel's incompletenss theorem in Wikipedia says:

Any effectively generated theory capable of expressing elementary arithmetic cannot be both consistent and complete. In particular, for any consistent, effectively generated formal theory that proves certain basic arithmetic truths, there is an arithmetical statement that is true,[1] but not provable in the theory (Kleene 1967, p. 250).

My understanding of Gödel's theorem derived from the proof sketch in the article above is that it is completely formal (axioms+logical axioms+inference rules) and does not rely on any model-theoretic notion where truth is established (a formal sentence being true iff every interpretation of it in every model is true).

But is this correct, that is are there proofs that use the apparatus of logic but do not not use any model theory at all? One piece of evidence that they must is that the quote above says that a statement is true but not proveable, and truth is a model-theoretic notion, unless of course there is a notion of truth different from model-theoretic truth?

EDIT

There is a very similar question here.

From the answer there one notices that 'true' is taken in the standard model of the integers. This is not the same as the model-theoretic notion of true taken above.

So, the question is refined to can we dispense with this restricted notion of truth and make the proof completely formal?

$\endgroup$
4
  • $\begingroup$ One just omits the "basic arithmetical truths" part, and shows that any consistent r.e. extension of say PA, (or something far weaker) is incomplete. $\endgroup$
    – André Nicolas
    Jun 14, 2013 at 21:23
  • 4
    $\begingroup$ After all one shows that there is some $\Phi$ such that $\Phi(\lceil n\rceil)$ is provable for all $n$, but $\forall n:\Phi(n)$ is not provable. This does not need models, only considering proofs syntactically. $\endgroup$
    – Hagen von Eitzen
    Jun 14, 2013 at 21:28
  • $\begingroup$ Aside: the informal usage of "true" squashes together a number of different concepts that one often doesn't care to distinguish. But in a context like this, doing that means we misunderstand all of the subtleties of the issue! In my opinion, the word "true" and its derivatives should be avoided entirely, except in the special case where the top element of a boolean algebra actually appears in a mathematical equation and needs to be named. $\endgroup$
    – user14972
    Dec 20, 2017 at 21:55
  • $\begingroup$ For future readers, note that the mistake in this question is the failure to properly distinguish between the meta-system MS and the formal system being studied within MS. MS itself can be formalized, so the incompleteness theorems can be completely formalized. This has nothing to do with truth. At the same time, those theorems as stated and proven in MS of course talk about arithmetical truths, which are sentences that hold in some particular model of PA that MS proves or assumes to exist. But naturals cannot be absolutely pinned down. $\endgroup$
    – user21820
    Dec 12, 2018 at 13:26

2 Answers 2

Reset to default
15
$\begingroup$

  • "A formal sentence being true iff every interpretation of it in every model is true". Not so. A sentence of formal arithmetic may be true on the intended, standard, interpretation while not a logical truth, not true on every interpretation.

  • "Gödel's theorem is completely formal." Not so. The theorem is a bit of ordinary informal mathematics. Its subject-matter is formal proofs in certain kinds of formal theories. But Gödel's theorem is a meta-result about those formal theories, and the usual proofs involve ordinary mathematical reasoning. [I say "ordinary" proofs because there have been projects to produce formal computer verifications of Gödel's theorem: but the theorem pre-dated the formal verifications by decades. And it is a nice question what we learn from having a formal proof in Coq, for example, all 37906 lines of it.]

  • "Gödel's theorem does not rely on any model-theoretic notion." Actually as perhaps Mostowski was the first to make really clear in his exposition, sixty years ago, there are two different versions of the first theorem, one that presupposes that we are dealing with a sound theory, another that assumes only that we are dealing with an [omega]-consistent theory. These are often referred to as the semantic vs the syntactic versions of the theorem. The semantic version, unsurprisingly, does rely on semantic notions.

  • "Are there proofs that use the apparatus of logic but do not not use any model theory at all?" Yes, some results, including the syntactic version of Gödel's first theorem, are purely proof-theoretic, i.e. about syntax. But again note that a theorem's being about syntax doesn't itself make it "completely formal". (For another example, proofs about the normalizability of formal natural deduction proofs in first-order logic are themselves bits of informal mathematics.)

$\endgroup$
6
  • $\begingroup$ Does the semantic version of the theory use logical truth or just in the standard model? I assume this means that the model isn't categorial so we're using higher order logic. $\endgroup$
    – Mozibur Ullah
    Jun 14, 2013 at 21:55
  • $\begingroup$ The main benefit I see of the proof in Coq, although it is quite long, is that it helps reduce any worries about the second incompleteness theorem, of which part of the proof is famously "left as an exercise" in textbooks. However, the fact that the incompleteness theorems can be formalized in PRA is more important, because it shows that the incompleteness theorems are finitistically provable. $\endgroup$
    – Carl Mummert
    Jun 14, 2013 at 23:10
  • $\begingroup$ "Beware of bugs in the above code; I have only proved it correct, not tried it." — Donald Knuth Humans are not as good at spotting small errors as computers are. $\endgroup$
    – dfeuer
    Jun 14, 2013 at 23:17
  • 1
    $\begingroup$ Your formulation of the second point is interesting: Don't you consider the computer version, which came decades later, to be extensionally :) equivalent to Gödels theorem? Once it's formalized in some way, wouldn't you say Gödels theorem is fully formal as such? $\endgroup$
    – Nikolaj-K
    Jun 14, 2013 at 23:40
  • 1
    $\begingroup$ @NickKidman I'd prefer to say that Gödel's theorem is formalizable. $\endgroup$
    – Peter Smith
    Jun 15, 2013 at 8:37
10
$\begingroup$

Although it is not usually presented this way, the usual proof of the incompleteness theorem shows the following:

For any sufficiently strong effective theory $T$ of arithmetic, with Gödel-Rosser sentence $G$, there is an algorithm that will take any proof of $G$ within $T$ and turn it into a proof of $0=1$ within $T$, and there is an algorithm that will take a proof of the negation of $G$ within $T$ and turn it into a proof of $0=1$ within $T$.

This has the immediate corollary:

For any sufficiently strong effective theory $T$ of arithmetic, with Gödel-Rosser sentence $G$, if $T$ does not prove $0=1$ then $T$ does not prove $G$ and $T$ does not prove the negation of $G$.

Neither of these statements, nor their proofs, requires any model theory.

However, these syntactic statements leave open the question of whether $G$ is actually true. It's one thing to know that there is some sentence that is neither provable nor disprovable, but either $G$ or its negation has to be true as a statement about natural numbers, and it would be nice to know which one it is. The answer is that $G$ is true, rather than the negation of $G$.

$\endgroup$
13
  • $\begingroup$ The first indented statement may seem somewhat weak, because we could just search for the proof of $0=1$ if it exists. But, if we add the fact that the proof of the incompleteness theorem establishes that the algorithm is given by a primitive recursive function, that removes any vacuousness. $\endgroup$
    – Carl Mummert
    Jun 14, 2013 at 23:13
  • $\begingroup$ 'neither of these statements or their proofs don't require model theory' - does this include interpretation in the standard model of the integers N? To tally with Peter Smiths answer (that there are two proofs - sound & syntactic) is the proof you're considering use omega-consistency? $\endgroup$
    – Mozibur Ullah
    Jun 14, 2013 at 23:14
  • $\begingroup$ No, no model theory at all is required for that, and there is no need to mention the standard model. The proof shows that there is a fixed algorithm that, solely by syntactic manipulation of formulas and proofs, will take a proof of $G$ and turn it into a proof of $0=1$. But the cost of this is that you lose part of the conclusion. $\endgroup$
    – Carl Mummert
    Jun 14, 2013 at 23:15
  • 2
    $\begingroup$ No, the theorem can be proved entirely syntactically, as I keep saying. $\endgroup$
    – Carl Mummert
    Jun 14, 2013 at 23:37
  • 1
    $\begingroup$ I'm trying to understand what you mean by saying 'these syntactic statements leave open the question of whether G is actually true' which implies that truth isn't something that is captured purely syntactically, and your explanation showed 'there is some sentence that is neither provable nor disprovable'. But you finally assert that 'The answer is that G is true'. Now when truth is mentioned I usually think of model interpretation. Obviously after your comments that can't be correct. So what notion of truth are you using in your last statement? $\endgroup$
    – Mozibur Ullah
    Jun 14, 2013 at 23:53

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .