1
$\begingroup$

Before I begin the question, it is meant to generalize to other theories, but I will focus on the natural numbers theory, with the following peano axioms: peano axiom list

The question is, could the induction schema be proved instead of being an axiom schema by doing appropiate modifications to the logic and to the axiom list? I think that, intuitively, if one knows that all natural numbers are of the form $S...SS(0)$ and that $\varphi(0) \wedge \forall x(\varphi(x)\implies\varphi (Sx))$ then one should be able to deduce $\forall x \varphi(x)$. However, you can't prove that all natural numbers are of the form $S...SS(0)$ with axioms 1 to 6, so you could add that as an schema, where $n$ is a natural number: $$\text{No-cycles schema: } \lnot \exists x_1 \lnot \exists x_2 ... \lnot\exists x_n[S(x_1)=x_2 \wedge S(x_2)=x_3 \wedge ...\wedge S(x_n)=x_1]$$

If this schema is sufficient to capture the intuition of all natural numbers being of the form $S...S(0)$ (which I am not sure of), what could be added to the logical axioms/deduction rules/natural deduction system (without allowing for infinitely long proofs) to prove the induction schema?

Edit:

Thanks to helpful comments, I've realized that my question is twofold:

  1. Can we create a theory where it's model doesn't have any deviant element? (it's fine if they have deviant properties). The closest formalization I can think of is that for every model of this theory has an order isomorphism ($x<y \iff S(x)=y$) with the standard model (under the same order).

  2. If such a theory could be created and if we had it, would it imply induction? If not, what changes to the logical systems (avoiding infinite proofs) could be made to be able to prove induction?

$\endgroup$
  • 2
    $\begingroup$ No, the Induction axiom cannot be derived from Axioms 1 through 6. See: math.stackexchange.com/questions/2817147/… $\endgroup$ – Bram28 Nov 30 '18 at 21:16
  • 3
    $\begingroup$ You cannot prove that all natural numbers have the form $S\dots S(0)$ with the Induction Schema either. $\endgroup$ – Asaf Karagila Nov 30 '18 at 21:23
  • $\begingroup$ What do you mean by a deviant element? $\endgroup$ – spaceisdarkgreen Dec 1 '18 at 1:28
  • 1
    $\begingroup$ If you mean an element not of the form $S^n(0),$ then perhaps I should expand on Asaf's point here: You cannot prove every natural has this form using induction schema, or for that matter, using any set of first order axioms whatsoever. Pretty much any first order theory has nonstandard models (Lowenheim-Skolem). There is no so thing as 'its model'... there are always many. $\endgroup$ – spaceisdarkgreen Dec 1 '18 at 1:35
  • $\begingroup$ This answers completely point 1. Thanks. By deviant element I meant an element that did not pertain to the standard model, though I admit it's not a really formal definition at all. $\endgroup$ – Shiranai Dec 1 '18 at 1:52
3
$\begingroup$

Your "No-cycles schema" idea isn't going to work for various reasons:

First, you can't use ellipsis ('...') in a logic formula; so you'd effectively have to add a formula that there cannot be a cycle of length $n$ for every $n$, i.e. infinitely many.

Second, they would have to be of the form: $$\text{No-cycles schema: } \lnot \exists x_1 \exists x_2 ... \exists x_n[S(x_1)=x_2 \wedge S(x_2)=x_3 \wedge ...\wedge S(x_n)=x_1]$$ (you have too many $\neg$'s; you just need one).

Third, you can have non-standard models in which you have two infinite 'successor sequences', so your No-cycles schema would hold, but Induction may still not work.

That is, in a domain with two sets of objects:

$0,S0,SS0,SSS0,...$ ($0$ is the object denoted by the constant $\mathsf{0}$, $S0$ the object denoted by $\mathsf{S(0)}$, etc.)

$0',S0',SS0',SSSS',...$

you can make all of Axioms 1 through 6 hold, and your 'No-Cycles scheme' holds as well, but the truth of $\varphi(0) \land \forall x (\varphi(x) \rightarrow \varphi(S(x))$ would only mean that the first set of objects have the property as expressed by $\varphi$, and so the second group of objects may not have that property, in which case $\forall x \ \varphi(x)$ would not be true. As such, it is fairly simple to create a concrete example where the Induction Axiom does not hold, showing that it cannot be derived from Axioms 1 through 6.

$\endgroup$
  • $\begingroup$ Thanks, this is very helpful. Just some additional questions, why can't the no-cycles schema be incorporated? I understand $"..."$ is not a valid logical symbol, it was just a shorthand, but the schema could be the set of all those formulas, could it not? Additionally, (assuming the no-cycles can be implemented), would it be enough to add $\forall x \exists y [x \not = 0 \implies S(y)=x] to rule out deviant successor sequences? By denying the existence of deviant zeroes plus the no-cycles, would we have an only sequence where induction is kinda implied? $\endgroup$ – Shiranai Dec 1 '18 at 0:56
  • $\begingroup$ I understand that by the Gödel incompleteness theorem I can't get the model exactly right, but my intuition is that as long as I get the number of elements right (as in there are no deviant elements), even if I can't prove all their properties the logic behind should be able to prove induction. I'll edit my question to consider this two steps. $\endgroup$ – Shiranai Dec 1 '18 at 0:59

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.