We get back to proving the First Incompleteness Theorem next week. In this week’s five chapters, we are reading into the record some necessary arithmetical background.
Everything in today’s chapter will very probably be quite familiar; but we do need to say just a little in GWT (a very little) about ‘First-order Peano Arithmetic’, the benchmark formalized theory of arithmetic. The most interesting claims (for a student who has not met them before, unlikely for a reader of this blog!) are those in the final section about non-standard models — but that brisk section is optional!
[Link now removed]
On chapter 6:
p. 39: “and now suppose that x(n) is true. Then it follows that …”
but this suggest the first line of the proof follows from x(n), which it does not. It’s the second line where the induction hypothesis is used. This could be confusing to some readers (well, it confused me for a moment). Instead of ‘then it follows that…’ it could be ‘Assume x(n) is true. Then we can reason …’
p.40 ‘how are we going to implement this idea in a formal theorem of arithmetic?’ Did you mean ‘formal theory’?
p. 42 defn. 25 of PA “..whose axioms are those of Q plus *the all* instances …’ should be ‘plus all the instances…’
p. 43 The exclamation mark at end of ‘Let’s have three initial examples…’ seems out of place.
p. 45 first line at the top of page 45 is not a sentence. It could be ‘something else would have encouraged…’
A general comment: Is it worth pointing out the connection between non-standard models and incompleteness here? If you have a consistent theory with no finite models which is negation-incomplete then it will have non-isomorphic countable models. For if A is undecidable in T, there’s a model of T in which A holds and a model in which ~A holds. By the Lowenheim-Skolem theorem, we can assume both have countable domains. Since A holds in one model and ~A in the other, they cannot be isomorphic.
By Godel’s theorem (theorem 2) every consistent recursively axiomatised extension of Q is negation-incomplete and none of them have finite models. So all such extensions have non-isomorphic countable models, including PA.
The nice thing about the proof you give for non-standard models of PA, using compactness, is that it works even for first-order arithmetical theories that are negation complete; for example the theory sometimes called ‘Arithmetic’ which consists of all the formulas of L_A true in the standard model. It’s quite surprising that even that theory — the theory of all first-order truths of arithmetic — has countable non-standard models.
A good suggestion, thanks! — worth a footnote to the compactness argument.
This is one of the chapters I like best out of those so far. I also think it’s a definite improvement on the version in GWT2f.
p 39, “plodding detail” and p 43, “painful detail” —
I think it’s generally best not to talk down things the reader is being asked to read or do. If the detail is plodding, for example, why is the reader being subjected to it? And if it’s expected that some readers will appreciate such detail, why suggest, in effect, that they need to plod?
The BA and Q proofs in Ch 5 were if anything more plodding and painful, but they weren’t described that way. The BA proofs were even introduced as “brisk examples”!
I think it’s better to use a more neutral expression, “simple steps”, say, rather than “plodding detail”.
Some alternatives to “Spelling that out in painful detail”:
Spelling that out in detail
Spelling that out in the step-by-step detail needed in formal proofs
p 43 “by the identity laws” and “by Conditional Proof” — I think that is much friendlier than the “by LL” and “by RAA” used in Ch 5.
p 42 I’m wondering: does anything in later chapters rely on being able to do induction on formulas with additional free variables?
p 44, “whose intended interpretation is the obvious one.” — I think it’s better to say what the interpretation is, rather than say it’s obvious.
p 45: This seems a natural question at this point: why can’t PA minus multiplication define multiplication?
p 46, “If you don’t know about compactness arguments, don’t worry – just skip, as nothing in later chapter depends on you knowing this proof.” —
I think that’s too strong. It’s useful to say nothing in later chapters depends on it. But GWT has just talked of the Lowenheim-Skolem theorem without any “just skip” advice, and the compactness argument isn’t all that hard to follow. I don’t think there should be so much encouragement to skip it.
p 46, “But can you now describe one of these countable-but-weird models of PA?” —
I think this paragraph is a bit misleading. It is possible to describe some things about their structure in a fairly straightforward way (their order type, though it can be be described more informally), and going straight to “we can take its domain to be the numbers again” obscures that. The rationals are countable, for instance, but we don’t immediately say we can take them to be the natural numbers again.
*
Will there be a “further reading” section somewhere in GWT3? There were such sections in the old GWT, but they were mostly about sections of IGT, and I think there was too much of that. Anyway, if there is any “further reading”, this might be a useful paper to include:
Richard Kaye, Tennenbaum’s Theorem for Models of Arithmetic
http://web.mat.bham.ac.uk/R.W.Kaye/papers/tennenbaum/tennenbaum.pdf
Hello Prof. Smith,
Great content, as usual! I have a question about the Induction Schema which I couldn’t easily figure out myself as I was reading the notes. As I take it, instances of the Induction Schema help us, given some numerical property P (expressed by some L_a wff Phi(x)), to syntactically derive that *all* numbers have property P if it’s provable that: (i) zero has property P and (ii) for all numbers n, if n has P, then s(n) has P.
However, what should we do if we don’t want to show that *all* numbers have property P, but just a subset of those. For a quick example, take the prime numbers as our infinite subset: {p0, p1, p2,…}. And let’s take our property P to be, say, the numerical property of being an odd number.
Now suppose we want to deploy some instance of the induction schema to show that all primes (greater than 2) are odd. We know that we can express in the language of arithmetic the property of being odd through some open L_a wff Odd(x). (Similarly, because the property of being a prime is decidable, we also have Prime(x) at our disposal.)
We’d want our induction schema instance to be something like:
(Odd(p_1) and forall x (Odd(p_x) -> Odd(p_s(x))) -> forall x Odd(p_x).
(The first argument is p_1 because p_0 would be 2, an even number. This is also a point that needs adjustment somehow.)
However, the foregoing statement is clearly not an instance of the Induction Scheme (not even a L_a wff since p_i’s are not in the language). How can this be adjusted in our formal framework to capture our thoughts?
I’m not sure this is a great example, since we don’t need induction to prove that primes (greater than 2) are odd! It follows immediately from the definition of being prime that a prime greater than 2 is not divisible by 2!
But you are raising a general point of principle. For example, how could we use induction to e.g. that all odd numbers are F? Well we could do the induction on the complex open wff F(2x + 1), showing the x = 0 case F1, and then showing that for all x, if F(2x + 1) then F(2Sx + 1). Then by induction we can conclude that, for all x, F(2x + 1). Then we use the fact that each odd number has the form (2x + 1).
Hello Professor, thanks for the quick reply!
I understand what you’re saying, but I’m still a bit confused about one aspect. To be clear, I’m *not* asking how to do simple induction exercises informally on paper (I know how to do that), but how I would carry out the reasoning mechanistically *inside Peano Arithmetic*. In order to do PA-proofs with make use of induction, I need to instantiate the Induction Scheme with a suitable wff. You gave the example of showing that all the odd numbers have the (definable) numerical property F by considering an open wff Phi(X) defined as Psi(S(SS0 x X)), where Psi(x) expresses F. In this case, we instantiate the Induction Schema with Phi(X) and I am perfectly ok with that.
But what if, coming back to the primes instead of the odds, we want to *reason inside PA* that all primes are F. We need to instantiate the Induction Schema somehow. But how do we restrict the universal quantifier to quantify only over the extension of Prime(x) and, more importantly I guess, to adjust the successor function to give out the next prime instead of the ordinary successor? So instead of s(x), to spit out p_{x+1}. In the case of showing that F holds for odd numbers, I understand the ‘S(SS0 x X)’ (i.e. 2x+1) trick you used. But this strategy doesn’t seem to work when it’s more chaotic to spell out what the next targeted element is, as it happens in the case of primes.
The induction formula would have to look something like this:
[F applies to 2 and for all x (if x is prime and x is F, then *the prime following x* is also an F)] implies that for all x (if x is prime, then x is F).
I have an idea of how to formalize that with the aid of the less-than-or-equal relation etc, but the resulting formalized version seems to be far from the syntactic shape required of the Induction Schema instances. The syntactic mismatch makes it impossible to use the formalization of the above in the course of mathematical reasoning *inside PA*, or at least it seems to me that way…
Sorry if I really get this wrong and thanks again for your time!