I have the following definition:
$\quad p(x) \iff (x=0 \vee$
$\quad\quad\quad\quad\quad\quad\exists y\ (x=y+2\ \&\ p(y)) \vee$
$\quad\quad\quad\quad\quad\quad(x=1\ \&\ \forall y\ p(y*2)))$
Assume I have first order logic with the first order induction principle for natural numbers. Plus definitions for $+2$ and $*2$ bootstrapped from successor.
Can I prove $\forall x\ p(x)$? And if yes, can I do it with a single induction?
Is this formal enough?
You have $p(0)$. Denoting the successor by $'$ we have $y'*2=(y*2)+2$. Therefore from $p(x)\Rightarrow p(x+2)$ we can conclude that $\forall y:\ p(y*2)$. This implies $p(1)$ by your third clause, and using $p(x)\Rightarrow p(x+2)$ again we get $p(x)$ for all odd $x$.