Inducción, ¿con qué frecuencia?

Question

Tengo la siguiente definición:

$\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)))$

Supongamos que tengo una lógica de primer orden con el principio de inducción de primer orden para los naturales. Más definiciones para $+2$ y $*2$ con el arranque de del sucesor.

¿Puedo probar $\forall x\ p(x)$ ? Y si es así, ¿puedo hacerlo con una sola inducción?

Answer 1

¿Es lo suficientemente formal?

Usted tiene $p(0)$ . Denotando al sucesor por $'$ tenemos $y'*2=(y*2)+2$ . Por lo tanto, desde $p(x)\Rightarrow p(x+2)$ podemos concluir que $\forall y:\ p(y*2)$ . Esto implica $p(1)$ por su tercera cláusula, y utilizando $p(x)\Rightarrow p(x+2)$ de nuevo obtenemos $p(x)$ para todos los impar $x$ .