Sintaxis de la lógica de primer orden

Buenas noches, quisiera saber si el siguiente razonamiento es correcto para la resolución del ejercicio 8 parte a.

Sean $\varphi \in FORM, x \in Var, t \in TERM$, se pide probar si la afirmación $x$ es libre para $x$ en $\varphi$ es verdadera o falsa, justificando en cualquier caso.

Pensé hacer inducción en $FORM$, la cual quedó (medio resumida, obviando algunos pasos) de la siguiente manera:

Se quiere probar la propiedad $(\forall \varphi \in FORM)$($x$ esta libre para $x$ en $\varphi$)

PB: $\varphi$ es atómica (o bien $\varphi = \perp$, o bien $\varphi = P_{j}(t_{1},...,t_{rj})$, o bien $\varphi = t_{1} =' t_{2}$).

Dem: Aplicando def de término libre para variable en una fórmula, como $\varphi$ es atómica, entonces se cumple.

PI_1:

HI_1: $x$ esta libre para $x$ en $\varphi_{1}$ y $x$ esta libre para $x$ en $\varphi_{2}$

TI_1: $x$ esta libre para $x$ en $(\varphi_{1} \Box \varphi_{2})$

Dem: Por def de termino libre para una variable en una formula, $x$ esta libre para $x$ en $(\varphi_{1} \Box \varphi_{2})$ si $x$ esta libre para $x$ en $\varphi_{1}$ y $x$ esta libre para $x$ en $\varphi_{2}$, lo cual es cierto por HI_1.

PI_2:

HI_2: $x$ esta libre para $x$ en $\varphi_{1}$

TI_2: $x$ esta libre para $x$ en $(\neg \varphi_{1})$

Dem: Por def de termino libre para una variable en una formula, $x$ esta libre para $x$ en $(\neg \varphi_{1})$ si $x$ esta libre para $x$ en $\varphi_{1}$, lo cual es cierto por HI_2.

PI_3: $\varphi = (\forall x') \varphi_{1}$

HI_3: $x$ esta libre para $x$ en $\varphi_{1}$

TI_3: $x$ esta libre para $x$ en $(\forall x') \varphi_{1}$

Dem: 

Si $x = x'$, entonces $x \notin FV(\varphi)$, por lo tanto es libre para $x$ en $\varphi$ por definición de.

Si $x \neq x'$, entonces $x' \notin FV(x)$ y $x$ esta libre para $x'$ en $\varphi_{1}$ por HI_3.

Análogo para el caso $\varphi = (\exists x') \varphi_{1}$

Aplicando el PIP en $FORM$, concluyo que $x$ es libre para $x$ en $\varphi$ para toda $\varphi \in FORM$.

Saludos!