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