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