Proof of induction from higher starting point

Question

I'd like to request to verify this proof that for a arbitrary natural $n_0$ this holds:
$[C(n_0+1) $ and $\forall n>n_0 : C (n) \implies C (n+1)] \implies \forall n> n_0 : C (n) $
($C (n)$ means a condition)

At first it seemed easy but I haven't yet proved that there aren't any naturals between n and n+1 etc nor any other properties of naturals, which makes me unsure of the correctness of my proof. All I can use is peano axioms and addition. So here it is:

Assume $C (n_0+1) $ and $\forall n > n_0 : C (n) \implies C (n+1)$

Let D (n) be a condition: $D (n) \iff (n>n_0 \implies C (n))$

i) $D (0)$ is obviously true since 0 cannot be bigger than $n_0$ therefore the implication is true.

ii) Assuming $D (n) $we have to prove $D (n+1)$

$n>n_0 \implies C (n) $ (ind. hypothesis)

$\forall n>0 : C (n) \implies C (n+1)$

The previous 2 lines thus give: $n>n_0 \implies C (n+1) $

Since $n+1>n $ we get finally

$(n+1>n_0 \implies C (n+1)) $

Is this correct ? Is there a better aproach?

Answer 1

The easiest approach is to define a new variable $m=n-n_0$ and a new predicate $E(p)$ such that $E(p)\equiv C(p+n_0)$. Then you have $E(0)$ and $E(m)\implies E(m+1)$ and can use the induction axiom as usual.

Answer 2

We wish to show that the condition $C(n)$ holds for each $n \in \mathbb{N}$ such that $n > n_0$ given that $C(n_0 + 1)$ holds and $\forall n > n_0: C(n) \implies C(n + 1)$.

Consider the set $T = \{n \in \mathbb{N} \mid n > n_0 \wedge C(n)~\text{does not hold}\}$. We must show that $T = \emptyset$.

Suppose $T \neq \emptyset$. Since $T \subseteq \mathbb{N}$, then $T$ must have a least element by the Well-ordering principle. Call it $t$. Since $C(n_0 + 1)$ holds, $t \neq n_0 + 1$, so $t > n_0 + 1$. Hence, $t - 1 > n_0$. Since $t$ is the smallest element of $T$, $C(t - 1)$ holds. Since $t - 1 > n_0$, $C(t - 1) \implies C(t)$, contradicting our assumption that $t \in T$. Hence, $T = \emptyset$.