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.
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.