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