Ejercicio 8 a

Ejercicio 8 a

de Alejandro Jose Rojas Quartino -
Número de respuestas: 0

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!