I am looking at an altered condition in the standard natural number induction principle (see reminder below). Specifically, the schema $$\forall n. \Big(\big(n=0\lor \exists p. ((Sp=n)\land \phi(p))\big)\to \phi(n)\Big)\ \to\ \forall m. \phi(m)$$ This variant seems to be just weak induction with the antecedent in brackets being expressed by a predicate that's shifted down by one compared with any given $\phi$. It looks like it would, when taken as axiom, imply the standard induction formulas. The ingrained predecessor expression seems mild, but then again I think we usually must use induction to prove all numbers have one. Not being allowed to go in circles and use lemmas proved from induction, I fails to see how to show this implication.
For starters, I fail to formally fuse the two quantifiers to one. I can turn $A\land B$ into $\neg(A\to \neg B)$ and thus get a negation to play around, but that doesn't seem to resolve the gap. There might be some natural deduction style bookkeeping to move between those forms. Maybe it's just that I don't need the predecessor for all numbers (at once) and that's why rewriting without the $\exists$ is legal. Then a short discussion would be helpful of why Robinson arithmetic needs the axiom but and can't be gotten from universally generalization there. Or maybe a formal way of rewriting the outer universal quantifier of the overall antecedent in the sense of applying $\forall n.P(n)\to \forall n.P(S(n))$, which trivializes $n=0$ and $\exists p. Sp=n$ using arithmetic. Maybe instead of a rewriting one wants to show that the assumption in this altered induction rules out a counter-example and then use $(\neg\exists n.\neg P(n))\to(\forall n.\neg\neg P(n))$. If the latter is the approach to take, I wonder if double-negation elimination is required to prove the equivalence. If it's equivalent, do I need to use other arithmetic properties regarding predecessors to get rid of the $\exists$, or is this already equivalent using logical principles? If not, what's a structure distinguishing them?
Recall the "strong and weak" forms of the induction schemas
$\forall n. \Big(\big(\forall(k< n). \phi(k)\big)\to \phi(n))\Big)\ \to\ \forall m. \phi(m)$
$\Big(\phi(0)\land \forall n. (\phi(n) \to \phi(Sn))\Big)\ \to\ \forall m. \phi(m)$
The latter weak one can also be written, a bit more convoluted, as
$\Big((\top\to \phi(0))\land \forall n. (\phi(n) \to \phi(Sn))\Big)\ \to\ \forall m. \phi(m)$.
The former strong one also captures the requirement to prove the zero case as $\forall (k<0).P(n)=\top$. Also I write them down here as schemas, but in the end we may move between equivalents just in terms of some given proposition.
In Peano arithmetic, induction can be used to prove that every non-zero number $n$ has a computable predecessor $p$ with $n=p+1$.
Elaboration on some of the tactics I mention:
- For any given numeral $t$, plugging in $n=St$ into the expressing in the antecedent of the alternative induction principle gives $$\big(St=0\lor \exists p. ((Sp=St)\land \phi(p))\big)\to \phi(St)$$ Since $St=0$ is always false and $p=t$ is a witness, this reduces to $\phi(t)\to \phi(St)$, which is the same as in weak induction. Going in the other direction would be the outer-quantifier rewriting approach.
- For the indirect counter-example approach. Succeeding only this non-constructive way would beg for models that distinguish the principles: Consider any $\phi$ for which there is a given numeral $t$ such that the truth value changes, $\phi(t)\leftrightarrow\neg\phi(St)$. Using the above, the $\to$-direction of this breaks the $\forall n$-antecedent (of weak induction as well as of my principle). Similarly, for a $\phi$ which is just always false, also both antecedents break. In such case, as $\bot\to\top$, the principles overall are value. Now if $\neg\forall m. \phi(m)$ then classically $\exists m. \neg\phi(m)$ and we may reason that either of the two scenarios apply.