On Tue, Sep 3, 2013 at 2:05 PM, James Propp <jamespropp@gmail.com> wrote:
Are there (positive) integers m,n definable in PA whose existence is provable in PA such that m \geq n and n \geq m are undecidable in PA? (I think that's the right way to ask the question I have in mind, but if my wording evinces misunderstanding of foundational issues, please enlighten me!)
I'm not sure exactly what you mean by "defineable". I'm assuming what you mean is that there is a formula P(x) with one free variable, such that ExP(x) ^ ((AxAy P(x) ^ P(y)) -> x=y) is a theorem of PA,then the number x such that P(x) is defineable in PA. Using that definition of defineable, I think the answer to your question is yes. Here's a proof sketch (note that this involves no paradox, since this is not a proof in PA; it's a proof in some more powerful system, like ZFC, in which consis(PA) is a theorem). Let G be a Goedel sentence for PA, that is, a statement G that says "not-G is provable". G is undecideable in PA (if G is provable, so is not-G, and PA is inconsistent, and if not-G is provable, then G is true, so again PA is inconsistent; since PA is consistent (this is provable in ZF), neither G nor not-G is proveable in ZF) G is false in the standard model of PA; that is, none of 1, 1+1, 1+1+1, 1+1+1+1, ... is the Goedel number of a proof of not-G. So in the model in which those are all the numbers there are, the statement "Ex(x is a proof of G) is false. B ut there are models where there are bigger numbers than all of those, in which there is a number x such that "x is the goedel number of a proof of G" is true. Now let P(x) be "x is the smallest number that is the Goedel number of a proof of G, if such a number exists, or 4 if there is no number that is the Goedel number of a proof of G". let Q(x) be "x is the second smallest number that is the Goedel number of a proof of G, if two such numbers exists, or 3 if there are 0 or 1 numbers that are the Goedel numbers of a proof of G". Then "ExEy(P(x)^Q(y))" is a theorem of PA, but "ExEy(P(x)^Q(y) ^ x < y)" and "ExEy(P(x)^Q(y) ^ y < x)" are undecideable. In the standard model, the first is false and the second is true,
What if we replace PA by a stronger theory?
I think a similar argument works in any stronger omega-consistent theory F, where the proof is in the still stronger theory F + Consis(F).
The underlying intuition is that if there are incomprehensibly big numbers, at some point even comparative notions of bigness should start to fail us, so that, in a certain sense, the well-ordering of the natural numbers should become problematical.
Nonstandard models of PA have numbers that are bigger than all of 1, 1+1, 1+1+1, etc, but I'm not sure they correspond well to your intuitions of "unimaginably big numbers". The axiom schema of induction does its best to assert that no such numbers exist, but it only provides induction on countably many properties, and if you're sufficiently devious, you can (non-constructively) find a model where there are these extra numbers, but the axiom of induction "just happens to work" for each of these countably many properties. Andy