Logic

Notation: Q : formal system (logical & nonlogical axioms, etc.) of Robinson's arithmetic; wff : well formed formula; |- : proves. G1IT is always stated in the form: If Q is consistent then exists wff x: ¬(Q |- x) & ¬(Q |- ¬x) but we cannot prove it within Q (simply because there is no deduction rule to say "Q doesn't prove" (there is only modus ponens and generalization)), so it's incomplete statement, I don't see WHERE (in which formal system) IS IT STATED. (Math logic is a formal system too.) In my opinion, some correct answer is to state the theorem within a copy of Q: Q |- Con(O) |- exists x ((x is wff of O) & ¬(O |- x) & ¬(O |- ¬x)) where O is a copy of Q inside Q, e.g. ¬(O |- x) is an arithmetic formula of Q, Con(O) means contradiction isn't provable...such formulas can be constructed (see Godel's proof). But I'm confused because I haven't found such statement (or explanation) anywhere. Thank You Very Much

Comments

Gödel's first incompleteness theorem applied to the arithmetic Q tells us that there is a corresponding Gödel sentence GQ such that, if Q is consistent, it can't prove GQ, and if Q satisfies a rather stronger condition (so-called omega-consistency) then Q can't prove not-GQ either.

How do we establish the incompleteness theorem? There is a number of different arguments. But Gödel's original one depends on the very ingenious trick of using numbers to code facts about proofs. And he shows us how to construct an the arithmetical sentence GQ which -- read in the light of that coding -- "says" that GQ is not provable in Q. (So of course we don't want Q to prove GQ or it would prove a falsehood!)

Now, Gödel's original proof of the incompleteness theorem, and all the textbook variants, are presented as nearly all mathematics is presented -- i.e. in informal mathematicians' German or English or whatever, with as much detail filled in as is needed to convince. And what's wrong with that? Why should it be stated "in a formal system"? Mathematics is almost never so stated -- and it is none the worse for that!

But still, let's note that, assuming a suitable coding system, there will be an arithmetical sentence Con(Q) which "says" that Q is consistent. And we've just noted that GQ "says" that GQ is not provable in Q. So e.g. the claim that if Q is consistent, it can't prove GQ (i.e. one half of the Gödelian result for Q) can itself be represented as an arithmetic sentence, Con(Q) --> GQ. And we might ask: can this arithmetic sentence be proved in Q? To which the answer is no! Proving that sentence in fact requires using a smidgin of induction, and the very weak arithmetic Q lacks induction. However, Con(Q) --> GQ can be proved in richer formal arithmetics which allow enough induction. (And we don't need to talk about "copies" of Q inside Q or inside any other theory -- the idea we need is coding, not copying.)

However, I'm afraid that is probably all going to be a bit telegraphic for nearly every reader, and maybe for the questioner too! But you will find a pretty accessible version of the whole story in my Introduction to Gödel's Theorems (if I'm allowed some shameless advertising!). And even if you don't want all the technical bells and whistles, the first chapter -- which can be freely downloaded -- should help round out what I've said here.

One thing the questioner seems to want to know is in what kinds of theories the first incompleteness theorem can itself be proved. As Peter says, the proof of the theorem is fine given informally, as almost all actual mathematical results are. But still, one might want to know: Where is this theorem provable?

The answer is: Not in Q, but in fairly weak theories. It can certainly be proven in PA---full Peano arithmetic---though that hardly counts as a "weak" theory. I am fairly certain, though, that it can be proven in the theory known as "I-Sigma-1"---though I'd have to check that before betting my life on it. Part of the reason I'm sure about this, though, is that I-Sigma-1 is susceptible to the second incompleteness theorem. What you get in such cases is (e.g.) that PA |- Con(PA) --> GPA; but then, if PA |- Con(PA), then PA |- GPA, and PA is inconsistent, by the first incompleteness theorem, and this works for any theory T that extends Q and is capable of proving: Con(T) --> GT.

So---I think, but someone check me on this---PA itself proves: If PA proves Con(PA), then ~Con(PA). But (this is where it gets really weird!), it's still consistent that PA proves that PA proves that Con(PA). If so, then of course PA proves ~Con(PA), but that too is consistent.

Read another response by Peter Smith, Richard Heck

Read another response about Logic