We can try to write that down as “For all x, there is an n such that x = S(S(...S(0)...)) repeated n times.”
The two problems that we run into here are: first, that repeating S n times isn’t something we know how to do in first-order logic: we have to say that there exists a sequence of repetitions, which requires quantifying over a set. Second, it’s not clear what sort of thing “n” is. It’s a number, obviously, but we haven’t pinned down what we think numbers are yet, and this statement becomes awkward if n is an element of some other chain that we’re trying to say doesn’t exist.
I’ve also seen addition defined recursively somehow, so each step it subtracted 1 from the second number and added 1 to the first number, until the second number was equal to zero. Something like this:
From this you could define subtraction in a similar way, and then state that all numbers subtracted from themselves, must equal 0. This would rule out nonstandard numbers.
From this you could define subtraction in a similar way, and then state that all numbers subtracted from themselves, must equal 0. This would rule out nonstandard numbers.
That will not rule out nonstandard models of the first-order Peano axioms. If a subtraction predicate is defined by:
∀x. sub(x,0,x)
∀x.∀y.∀z. sub(x,y,z) ⇒ sub(s(x),s(y),z)
then you don’t need to add that all numbers subtracted from themselves, must equal 0. ∀x.sub(x,x,0) is already a theorem, which can be proved almost immediately from those axioms and the first-order induction schema. Being a theorem, it is true in all models. Every nonstandard element of a nonstandard model, subtracted from itself, gives 0.
It may seem odd that a statement proved by induction is necessarily true even of those elements of a non-standard model that, in our mental picture of them, cannot be reached by counting upwards from zero, but the induction axiom scheme explicitly says just that: if P(0) and ∀x.(P(x) ⇒ P(s(x))) then ∀x.P(x). The conclusion is not limited to standard values of x, because the language cannot distinguish standard from non-standard values.
If you already have an axiom of induction then you’ve already ruled out nonstandard numbers and this isn’t an issue. I was trying to show that without the second order logic axiom of induction, you can rule out nonstandard numbers.
The recursive subtract predicate will never reach zero on a nonstandard number, therefore it can not be true that n-n=0.
If you already have an axiom of induction then you’ve already ruled out nonstandard numbers and this isn’t an issue. I was trying to show that without the second order logic axiom of induction, you can rule out nonstandard numbers.
Without second-order logic, you cannot rule out nonstandard numbers. As Epictetus mentioned, the Lowenheim-Skolem Theorem implies that if there is a model of first-order Peano arithmetic, there are models of all infinite cardinalities.
You have to distinguish the axioms from the meanings one intuitively attaches to them. We have an intuitive idea of the natural numbers, and the Peano axioms (including the induction schema) seem to be true of them. However, ZFC set theory (for example) provably contains models of those axioms other than the natural numbers of our intuition.
The induction schema seems to formalise our notion that every natural number is reachable by counting up from zero. But look more closely and you can intuitively read it like this: if you can prove that P is true of every number you can reach by counting, then P is true of every number (even those you can’t reach by counting, if there are any).
The predicate “is a standard number” would be a counterexample to that, but the induction schema is asserted only for formulas P expressible in the language of Peano arithmetic. Given the existence of non-standard models, the fact that “is a standard number” does not satisfy the induction schema demonstrates that it is not definable in the language.
The subtraction predicate provably satisfies ∀n. n-n = 0. Therefore every model of the Peano axioms satisfies that—it would not be a model if it did not.
(Technical remark: I should not have added “sub” as a new symbol, which creates a different language, an extension of Peano arithmetic. Instead, “sub(x,y,z) should be introduced as a metalinguistic abbreviation for y+z=x, which is a formula of Peano arithmetic. One can still prove ∀x. sub(x,x,0), and without even using induction. Expanding the abbreviation gives x+0 = x, which is one of the axioms, e.g. as listed here.)
Every (countable) first-order theory that has an infinite model, has a model of size k for every infinite cardinal k. You cannot use first-order logic to exclude non-standard numbers unless you want to abandon infinite models altogether.
Repeating S n times is not addition: addition is the thing defined by those axioms, no more, and no less. You can prove the statements:
∀x. plus(x, 1, S(x))
∀x. plus(x, 2, S(S(x)))
∀x. plus(x, 3, S(S(S(x))))
and so on, but you can’t write “∀x. plus(x, n, S(S(...n...S(x))))” because that doesn’t make any sense. Neither can you prove “For every x, x+n is reached from x by applying S to x some number of times” because we don’t have a way to say that formally.
From outside the Peano Axioms, where we have our own notion of “number”, we can say that “Adding N to x is the same as taking the successor of x N times”, where N is a real-honest-to-god-natural-number. But even from the outside of the Peano Axioms, we cannot convince the Peano Axioms that there is no number called “pi”. If pi happens to exist in our model, then all the values …, pi-2, pi-1, pi, pi+1, pi+2, … exist, and together they can be used to satisfy any theorem about the natural numbers you concoct. (For instance, sub(pi, pi, 0) is a true statement about subtraction, so the statement “∀x. sub(x, x, 0)” can be proven but does not rule out pi.)
“For every x, x+n is reached from x by applying S to x some number of times” because we don’t have a way to say that formally.
But that’s what I’m trying to say. To say n number of times, you start with n and subtract 1 each time until it equals zero. So for addition, 2+3 is equal to 3+2, is equal to 4+1, is equal to 5+0. For subtraction you do the opposite and subtract one from the left number too each time.
If no number of subtract 1′s cause it to equal 0, then it can’t be a number.
I know that’s what you’re trying to say because I would like to be able to say that, too. But here’s the problems we run into.
Try writing down “For all x, some number of subtract 1′s cause it to equal 0”. We can write the “∀x. ∃y. F(x,y) = 0″ but in place of F(x,y) we want “y iterations of subtract 1′s from x”. This is not something we could write down in first-order logic.
We could write down sub(x,y,0) (in your notation) in place of F(x,y)=0 on the grounds that it ought to mean the same thing as “y iterations of subtract 1′s from x cause it to equal 0”. Unfortunately, it doesn’t actually mean that because even in the model where pi is a number, the resulting axiom “∀x. ∃y. sub(x,y,0)” is true. If x=pi, we just set y=pi as well.
The best you can do is to add an infinitely long axiom “x=0 or x = S(0) or x = S(S(0)) or x = S(S(S(0))) or …”
I think I’m starting to get it. That there is no property that a natural number could be defined as having, that a infinite chain couldn’t also satisfy in theory.
That’s really disappointing. I took a course on logic and the most inspiring moment was when the professor wrote down the axioms of peano arithmitic. They are more or less formalizations of all the stuff we learned about numbers in grade school. It was cool that you could just write down what you are talking about formally and use pure logic to prove any theorem with them. It’s sad that it’s so limited you can’t even express numbers.
We can try to write that down as “For all x, there is an n such that x = S(S(...S(0)...)) repeated n times.”
The two problems that we run into here are: first, that repeating S n times isn’t something we know how to do in first-order logic: we have to say that there exists a sequence of repetitions, which requires quantifying over a set. Second, it’s not clear what sort of thing “n” is. It’s a number, obviously, but we haven’t pinned down what we think numbers are yet, and this statement becomes awkward if n is an element of some other chain that we’re trying to say doesn’t exist.
Why not? Repeating S n times is just addition, and addition is defined in the peano first order logic axioms. I just took these from my textbook:
∀y.plus(0,y,y)
∀x.∀y.∀z.(plus(x,y,z) ⇒ plus(s(x),y,s(z)))
∀x.∀y.∀z.∀w.(plus(x,y,z) ∧ ¬same(z,w) ⇒ ¬plus(x,y,w))
I’ve also seen addition defined recursively somehow, so each step it subtracted 1 from the second number and added 1 to the first number, until the second number was equal to zero. Something like this:
∀x.∀y.∀z.∀w.(plus(x,y,z) ⇒ plus(s(x),w,z) ∧ same(s(w),y))
From this you could define subtraction in a similar way, and then state that all numbers subtracted from themselves, must equal 0. This would rule out nonstandard numbers.
That will not rule out nonstandard models of the first-order Peano axioms. If a subtraction predicate is defined by:
∀x. sub(x,0,x)
∀x.∀y.∀z. sub(x,y,z) ⇒ sub(s(x),s(y),z)
then you don’t need to add that all numbers subtracted from themselves, must equal 0. ∀x.sub(x,x,0) is already a theorem, which can be proved almost immediately from those axioms and the first-order induction schema. Being a theorem, it is true in all models. Every nonstandard element of a nonstandard model, subtracted from itself, gives 0.
It may seem odd that a statement proved by induction is necessarily true even of those elements of a non-standard model that, in our mental picture of them, cannot be reached by counting upwards from zero, but the induction axiom scheme explicitly says just that: if P(0) and ∀x.(P(x) ⇒ P(s(x))) then ∀x.P(x). The conclusion is not limited to standard values of x, because the language cannot distinguish standard from non-standard values.
If you already have an axiom of induction then you’ve already ruled out nonstandard numbers and this isn’t an issue. I was trying to show that without the second order logic axiom of induction, you can rule out nonstandard numbers.
The recursive subtract predicate will never reach zero on a nonstandard number, therefore it can not be true that n-n=0.
Without second-order logic, you cannot rule out nonstandard numbers. As Epictetus mentioned, the Lowenheim-Skolem Theorem implies that if there is a model of first-order Peano arithmetic, there are models of all infinite cardinalities.
You have to distinguish the axioms from the meanings one intuitively attaches to them. We have an intuitive idea of the natural numbers, and the Peano axioms (including the induction schema) seem to be true of them. However, ZFC set theory (for example) provably contains models of those axioms other than the natural numbers of our intuition.
The induction schema seems to formalise our notion that every natural number is reachable by counting up from zero. But look more closely and you can intuitively read it like this: if you can prove that P is true of every number you can reach by counting, then P is true of every number (even those you can’t reach by counting, if there are any).
The predicate “is a standard number” would be a counterexample to that, but the induction schema is asserted only for formulas P expressible in the language of Peano arithmetic. Given the existence of non-standard models, the fact that “is a standard number” does not satisfy the induction schema demonstrates that it is not definable in the language.
The subtraction predicate provably satisfies ∀n. n-n = 0. Therefore every model of the Peano axioms satisfies that—it would not be a model if it did not.
(Technical remark: I should not have added “sub” as a new symbol, which creates a different language, an extension of Peano arithmetic. Instead, “sub(x,y,z) should be introduced as a metalinguistic abbreviation for y+z=x, which is a formula of Peano arithmetic. One can still prove ∀x. sub(x,x,0), and without even using induction. Expanding the abbreviation gives x+0 = x, which is one of the axioms, e.g. as listed here.)
I refer you to the Lowenheim-Skolem Theorem:
Every (countable) first-order theory that has an infinite model, has a model of size k for every infinite cardinal k. You cannot use first-order logic to exclude non-standard numbers unless you want to abandon infinite models altogether.
Repeating S n times is not addition: addition is the thing defined by those axioms, no more, and no less. You can prove the statements:
∀x. plus(x, 1, S(x))
∀x. plus(x, 2, S(S(x)))
∀x. plus(x, 3, S(S(S(x))))
and so on, but you can’t write “∀x. plus(x, n, S(S(...n...S(x))))” because that doesn’t make any sense. Neither can you prove “For every x, x+n is reached from x by applying S to x some number of times” because we don’t have a way to say that formally.
From outside the Peano Axioms, where we have our own notion of “number”, we can say that “Adding N to x is the same as taking the successor of x N times”, where N is a real-honest-to-god-natural-number. But even from the outside of the Peano Axioms, we cannot convince the Peano Axioms that there is no number called “pi”. If pi happens to exist in our model, then all the values …, pi-2, pi-1, pi, pi+1, pi+2, … exist, and together they can be used to satisfy any theorem about the natural numbers you concoct. (For instance, sub(pi, pi, 0) is a true statement about subtraction, so the statement “∀x. sub(x, x, 0)” can be proven but does not rule out pi.)
But that’s what I’m trying to say. To say n number of times, you start with n and subtract 1 each time until it equals zero. So for addition, 2+3 is equal to 3+2, is equal to 4+1, is equal to 5+0. For subtraction you do the opposite and subtract one from the left number too each time.
If no number of subtract 1′s cause it to equal 0, then it can’t be a number.
I know that’s what you’re trying to say because I would like to be able to say that, too. But here’s the problems we run into.
Try writing down “For all x, some number of subtract 1′s cause it to equal 0”. We can write the “∀x. ∃y. F(x,y) = 0″ but in place of F(x,y) we want “y iterations of subtract 1′s from x”. This is not something we could write down in first-order logic.
We could write down sub(x,y,0) (in your notation) in place of F(x,y)=0 on the grounds that it ought to mean the same thing as “y iterations of subtract 1′s from x cause it to equal 0”. Unfortunately, it doesn’t actually mean that because even in the model where pi is a number, the resulting axiom “∀x. ∃y. sub(x,y,0)” is true. If x=pi, we just set y=pi as well.
The best you can do is to add an infinitely long axiom “x=0 or x = S(0) or x = S(S(0)) or x = S(S(S(0))) or …”
I think I’m starting to get it. That there is no property that a natural number could be defined as having, that a infinite chain couldn’t also satisfy in theory.
That’s really disappointing. I took a course on logic and the most inspiring moment was when the professor wrote down the axioms of peano arithmitic. They are more or less formalizations of all the stuff we learned about numbers in grade school. It was cool that you could just write down what you are talking about formally and use pure logic to prove any theorem with them. It’s sad that it’s so limited you can’t even express numbers.