4

I'm currently working through Peter Smith's 'Introduction to Godel's Theorems'.

I'm wondering how a formalization of first-order logic that allows us to prove the incompleteness theorems, etc. might look. Is it a first-order theory itself? It does appear to make some second-order statements. For instance, when discussing Peano Arithmetic, we want to talk about the set of 'actual' natural numbers, namely the successors of 0 and nothing else. Then again, set theory manages to say things with first order logic which feel more like higher-order logic.

In particular, I wonder if first-order logic can be shown to be consistent itself. If not, what kind of consistence results are there with respect to first order logic?

Thanks.

Alex
  • 73
  • what do you mean by first-order logic is consistent? – azarel Jan 03 '14 at 22:43
  • I mean it in the same sense as the consistence of any theory. I'll try to elaborate some. What we do when we prove Godel's Incompleteness, or compactness, or completeness appears to be mathematics like anything else (set theory, arithmetic, etc.). So, I would assume that all of this can be formalized somehow, perhaps even as a first order theory T. If so, can T be proven to be consistent? I would guess probably not. Perhaps another way of asking this is, "Can the metatheory itself be expressed as a theory?". – Alex Jan 03 '14 at 23:13
  • Wikipedia mentions in passing that formal proofs of Godel's Incompleteness Theorems have been developed. I just wonder what these look like. http://en.wikipedia.org/wiki/G%C3%B6del's_incompleteness_theorems#Formalized_proofs – Alex Jan 03 '14 at 23:31
  • I alerted Peter Smith to this question on Twitter. He often posts here. – MJD Jan 04 '14 at 02:10

1 Answers1

3

Take the second question first:

I wonder if first-order logic can be shown to be consistent itself.

It is a textbook result in any math logic text that a standard deductive system for first-order logic (pick your favourite, axiomatic Hilbert-style, natural deduction style, tableaux-style ...) is consistent. That is to say, you can't derive something of the form $C \land \neg C$ from no assumptions in the deductive system. (Aside: It is perhaps a bit worrying you ask this. I'd really suggest to anyone that they tackle an elementary math logic text which covers this sort of thing before trying to get their head round more advanced stuff like the incompleteness theorems ...)

I'm wondering how a formalisation ... that allows us to prove the incompleteness theorems, etc. might look.

To fix ideas, consider (half) the first theorem for first-order Peano Arithmetic, PA. That's the result (F) that if PA is consistent, then PA doesn't prove $\mathsf{G}_{PA}$. This is a result about expressions (wffs) and relations between them, so we need to formalize a theory about expressions. But expressions are finite objects and we can give code numbers for them (that's the trick we use in informally proving (F)). So, using the coding trick, we can in fact express (F) in the language of arithmetic itself. Let $\mathsf{Con}$ be the arithmetical expression that codes that PA is consistent. And the expression that $\mathsf{G}_{PA}$ is unprovable in PA is -- wait for it! -- $\mathsf{G}_{PA}$ itself. So we can express (F), via coding, in the language of arithmetic as $\mathsf{Con} \to \mathsf{G}_{PA}$.

OK, so what does it take to formally prove this sentence (i.e. to give a formalized proof of half the first incompleteness theorem for PA)? Well, the proof of the first theorem is quite elementary, so you'd expect it to be provable in elementary arithmetic so in PA itself. And it is! [Indeed, as we'd guess, a weak subsystem of PA suffices]. So, in response to your question

First-order PA is itself sufficient to prove (half) the first incompleteness theorem for PA.

Bonus result: Since PA can prove $\mathsf{Con} \to \mathsf{G}_{PA}$ and can't prove $\mathsf{G}_{PA}$, PA can't prove $\mathsf{Con}$. Which is, of course, the second incompleteness theorem.

All this is explained in my book, Ch. 24 in the first edition, Ch. 31 in the much better second edition.

(On a slightly different tack, if you want to know about a formal computer verification of the first incompleteness theorem, then look here: http://r6.ca/Goedel/goedel1.html )

Peter Smith
  • 54,743
  • Thank you very much for this. I didn't expect a response from Peter Smith himself! I took a basic logic course some time ago and I've been brushing up on the basics as I've been reading your book. Sorry if the first bit seemed a bit elementary. I'm a bit surprised by last part above. In particular, the proof of the first half of the incompleteness theorem for PA seems to rely on being able to fix the standard model of natural numbers and I wouldn't think PA could do this. Anyway, I'll take a closer look at Ch. 24. Thank you very much. – Alex Jan 04 '14 at 22:20