Take the 2-minute tour ×
Mathematics Stack Exchange is a question and answer site for people studying math at any level and professionals in related fields. It's 100% free, no registration required.

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?

share|improve this question
    
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. –  André Nicolas Jun 14 '13 at 21:23
3  
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. –  Hagen von Eitzen Jun 14 '13 at 21:28

2 Answers 2

up vote 11 down vote accepted
  • "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.

  • "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.)

share|improve this answer
    
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. –  Mozibur Ullah Jun 14 '13 at 21:55
    
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. –  Carl Mummert Jun 14 '13 at 23:10
    
"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. –  dfeuer Jun 14 '13 at 23:17
1  
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? –  NikolajK Jun 14 '13 at 23:40
1  
@NickKidman I'd prefer to say that Gödel's theorem is formalizable. –  Peter Smith Jun 15 '13 at 8:37

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$.

share|improve this answer
    
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. –  Carl Mummert Jun 14 '13 at 23:13
    
'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? –  Mozibur Ullah Jun 14 '13 at 23:14
    
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. –  Carl Mummert Jun 14 '13 at 23:15
2  
No, the theorem can be proved entirely syntactically, as I keep saying. –  Carl Mummert Jun 14 '13 at 23:37
1  
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? –  Mozibur Ullah Jun 14 '13 at 23:53

Your Answer

 
discard

By posting your answer, you agree to the privacy policy and terms of service.

Not the answer you're looking for? Browse other questions tagged or ask your own question.