definiciones contradictorias de libre

definiciones contradictorias de libre

de Martín Fossatti Valetti -
Número de respuestas: 1

Buenas, estoy teniendo problemas comprendiendo cuando es aplicable una sustitución debido a que la definición de cuando un termino es libre para una variable en una formula es contradictoria.aquí es donde encuentro la contradicción, la primera definición es de las diapositivas del curso (def 2.3.11) y la segunda del libro (def 3.3.12), están diciendo lo opuesto respecto a la pertenencia de x en FV(phi), debo estar malinterpretando el uso de la notación, agradezco aclaren el porque de la diferencia.


note el problema al revisar la introducción al practico, en el siguiente ejercicio yo había comprendido que no se podía utilizar la sustitución, siguiendo la definición de las diapositivas, puesto que x3 pertenece a FV(((Ex2)x3='x1)) = {x3,x1} y x2 pertenece a FV(f1(x1,x2)) = {x1,x2}. Sin embargo en el video dicen que debido a que x3 no esta alcanzado por un cuantificador aplicado a x3, debe considerarse como libre y por tanto se puede sustituir. Agradecería me aclararan como aplicar la definición de que un termino es libre para sustituir.

desde ya muchas gracias, Martin.

En respuesta a Martín Fossatti Valetti

Re: definiciones contradictorias de libre

de Juan Diego Campo -
Hola Martín,

efectivamente hay una diferencia entre lo que está definido en las
diapositivas y el libro.

Las diapos dicen (simplificando un poco):

φ=((∀x)φ₁) y (x∉FV(φ) o (y∉FV(t) y t libre para x en φ₁))

El libro dice:

φ=((∀x)φ₁) y (si x∈FV(φ), entonces (y∉FV(t) y t libre para x en φ₁))


Estas dos definiciones son equivalentes. La primera tiene esta forma:

A ∧ (¬B ∨ (C ∧ D))

y la segunda:

A ∧ (B → (C∧D))

La diferencia se debe a que nos parece que la forma en que está
expresada la definición en las diapos es más clara que la del libro.
Pero ambas dicen lo mismo.



Respecto a la condición de "libre para" al aplicar las sustituciones, es
como vos decís:

el término f₁(x₁,x₂) NO está libre para x₃ en ((∃x₂)x₃='x₁)

Si bien no se cumple la condición, consideramos que la sustitución está
definida igual y me da:

((∃x₂)x₃='x₁)[f₁(x₁,x₂)/x₃] = ((∃x₂)f₁(x₁,x₂)='x₁)

Cuando veamos semántica, vamos a ver que estas sustituciones dan
problemas. Por eso no las queremos. A partir de la semana que viene,
siempre que aparezca una sustitución vamos a chequear que el término
esté libre para la variable en la fórmula.

Pero la función de sustitución está definida en este caso y sustituye el
término por la variable porque la x₃ está libre, como dice el video de
práctico.


Vale la pena aclarar que esta convención (la sustitución se aplica
igual, pero el resultado es problemático) la tomamos después de que se
grabaron las clases de teórico y que si bien las diapos de teórico se
actualizaron, el video en openfing quedó con la versión vieja (la
sustitución ni siquiera se aplicaba si el término no está libre para la
variable en la fórmula).

En cualquier caso, la diferencia es un tecnicismo que sólo complica esta
semana. Como te digo, a partir de la semana que viene, siempre que
aparezca una sustitución vamos a estar verificando que cumpla la
condición del libre para.


Saludos,

--
Juan Diego Campo
Instituto de Computación
Facultad de Ingeniería - UdelaR