< is defined in terms of plus by saying x<y iff there exists a such that y=z+x. + is supposed to be provided as a primitive operation as part of the data consisting of a model of PA. It’s not actually possible to give a concrete description of what + looks like in general for non-standard models because of Tenenbaums’s Theorem, but at least when one of x or y (say x) is a standard number it’s exactly what you’d expect: x+y is what you get by starting at y and going x steps to the right.
To see that x<y whenever x is a standard number and y isn’t, you need to be a little tricky. You actually prove an infinite family of statements. The first one is “for all x, either x=0 or else x>0”. The second is “for all x, either x=0 or x=1 or x>1″, and in general it’s “for all x, either x=0,1,..., or n, or else x>n”. Each of these can be proven by induction, and the entire infinite family together implies that a non-standard number is bigger than every standard number.
I suppose you can’t prove a statement like “No matter how many times you expand this infinite family of axioms, you’ll never encounter a non-standard number” in first-order logic? Should I not think of numbers and non-standard numbers as having different types? Or should I think of > as accepting differently typed things? (where I’m using the definition of “type” from computer science, e.g. “strongly-typed language”)
Sorry I didn’t answer this before; I didn’t see it. To the extent that the analogy applies, you should think of non-standard numbers and standard numbers as having the same type. Specifically, the type of things that are being quantified over in whatever first order logic you are using. And you’re right that you can’t prove that statement in first order logic; Worse, you can’t even say it in first order logic (see the next post, on Godel’s theorems and Compactness/Lowenheim Skolem for why).
Thanks. Hm. I think I see why that can’t be said in first order logic.
...my brain is shouting “if I start at 0 and count up I’ll never reach a nonstandard number, therefore they don’t exist” at me so loudly that it’s very difficult to restrict my thoughts to only first-order ones.
This is largely a matter of keeping track of the distinction between “first order logic: the mathematical construct” and “first order logic: the form of reasoning I sometimes use when thinking about math”. The former is an idealized model of the latter, but they are distinct and belong in distinct mental buckets.
It may help to write a proof checker for first order logic. Or alternatively, if you are able to read higher math, study some mathematical logic/model theory.
< is defined in terms of plus by saying x<y iff there exists a such that y=z+x. + is supposed to be provided as a primitive operation as part of the data consisting of a model of PA. It’s not actually possible to give a concrete description of what + looks like in general for non-standard models because of Tenenbaums’s Theorem, but at least when one of x or y (say x) is a standard number it’s exactly what you’d expect: x+y is what you get by starting at y and going x steps to the right.
To see that x<y whenever x is a standard number and y isn’t, you need to be a little tricky. You actually prove an infinite family of statements. The first one is “for all x, either x=0 or else x>0”. The second is “for all x, either x=0 or x=1 or x>1″, and in general it’s “for all x, either x=0,1,..., or n, or else x>n”. Each of these can be proven by induction, and the entire infinite family together implies that a non-standard number is bigger than every standard number.
Thanks!
I suppose you can’t prove a statement like “No matter how many times you expand this infinite family of axioms, you’ll never encounter a non-standard number” in first-order logic? Should I not think of numbers and non-standard numbers as having different types? Or should I think of > as accepting differently typed things? (where I’m using the definition of “type” from computer science, e.g. “strongly-typed language”)
Sorry I didn’t answer this before; I didn’t see it. To the extent that the analogy applies, you should think of non-standard numbers and standard numbers as having the same type. Specifically, the type of things that are being quantified over in whatever first order logic you are using. And you’re right that you can’t prove that statement in first order logic; Worse, you can’t even say it in first order logic (see the next post, on Godel’s theorems and Compactness/Lowenheim Skolem for why).
Thanks. Hm. I think I see why that can’t be said in first order logic.
...my brain is shouting “if I start at 0 and count up I’ll never reach a nonstandard number, therefore they don’t exist” at me so loudly that it’s very difficult to restrict my thoughts to only first-order ones.
This is largely a matter of keeping track of the distinction between “first order logic: the mathematical construct” and “first order logic: the form of reasoning I sometimes use when thinking about math”. The former is an idealized model of the latter, but they are distinct and belong in distinct mental buckets.
It may help to write a proof checker for first order logic. Or alternatively, if you are able to read higher math, study some mathematical logic/model theory.