Lógica: Segundo Parcial 2010 Ej-1

Buenas, para definir el PIP en FORM hay que definirlo también para TERM o no es necesario en este ejercicio? esto fue lo que hice del ejercicio pero nose si está bien el PIP o hay que agregar de alguna forma a TERM, nose si nombra la parte de TERM por formalismo o es necesario usar esa parte. También creo que tengo algo mal en el paso inductivo del para todo pero no logro darme cuenta donde, si alguien tiene idea le agradezco.

Re: Segundo Parcial 2010 Ej-1

de Romina Romero - InCo - jueves, 30 de junio de 2016, 01:13

Hola.

PIP de FORM

"para definir el PIP en FORM hay que definirlo también para TERM o no es necesario en este ejercicio?"

No, no es necesario nunca. El enunciado del PIP es siempre mecánico, es un algoritmo, grosso modo, de la siguiente forma:

Enunciar el PIP

Entrada:

conjunto: Nombre del conjunto
defInductConjunto: Definición de conjunto inductivo en cuestión

Salida: Enunciado del PIP para el conjunto en cuestión

Procedimiento:

var enunciado : String

enunciado = "H) Sea P una propiedad de los elementos de conjunto que cumple:"

para cada elemento base en defInductConjunto: // elementos que no se forman a partir de otros del conjunto

enunciado += "P(elemento)"

para cada elemento inductivo en defInductConjunto:

enunciado += "Si P(antecesor de elemento), entonces P(elemento)"

enunciado += "T) Se cumple P para todos los elementos de conjunto"

return enunciado

Si la entrada es FORM, la salida va a tener un rengloncito para cada elemento en la definición de FORM, nada de elementos que no están en la definición de FORM.

Lo que sí puede pasar es que para probar una propiedad en FORM, necesites probar una propiedad auxiliar en TERM. Eso no tienen nada que ver con el PIP en FORM, simplemente en la prueba que estás haciendo precisás un lema auxiliar que te ayude a probar algo que precisás probar.

Tu enunciado del PIP está casi bien. Le sobra el renglón de $\bot$ . $\bot$ , además de una fórmula, es un conectivo. Y no está en la lista de conectivos de $\mathcal{L}$ , así que no pertenece a ese lenguaje.

Propiedad a probar

Hay que corregir la propiedad a probar (no está bueno poner el "sean x, y ∈ TERM" adentro de la propiedad, además tenemos que exigir que estén en VAR, porque queremos que sean variables, no términos cualesquiera).

Empecemos por formalizar lo que hay que probar:

$(\bar{\forall} \varphi \in FORM_\mathcal{L})(\bar{\forall} x,y \in VAR)(x \not\in V(\varphi) \Rightarrow (\varphi[x/y])[y/x] = \varphi )$

Reordenando los para todos (es válido porque $(\forall x)(\forall y) \alpha$ eq $(\forall y)(\forall x) \alpha$ ):

$(\bar{\forall} x,y \in VAR)(\bar{\forall} \varphi \in FORM_\mathcal{L})(x \not\in V(\varphi) \Rightarrow (\varphi[x/y])[y/x] = \varphi )$

Acá es cuando decimos:

Sean x,y ∈ VAR. Ahora nos queda probar que:

$(\bar{\forall} \varphi \in FORM_\mathcal{L})(x \not\in V(\varphi) \Rightarrow (\varphi[x/y])[y/x] = \varphi )$

y esto último lo vamos aprobar por PIP en FORM.

$\mathcal{P}(\varphi) := x \not\in V(\varphi) \Rightarrow (\varphi[x/y])[y/x] = \varphi$ .

Demostración
Respecto a los PB, falta demostrar formalmente que si x no ocurre en t entonces t[x/y][y/x] = t, sin importar quién sea t. O sea, acá es donde ya entramos en el terreno de TERM, y se precisa otra inducción. En la demostración simplemente podemos poner "por lema se cumple", pero luego, como cosa aparte, fuera del PIP de FORM, hay que demostrar ese lema:

Lema:

$(\bar{\forall} t \in TERM)(x \not\in V(t) \Rightarrow t[x/y][y/x] = t )$
Ejercicio: demostrar por inducción en TERM

En el PI del ∀, en el caso 1, no me cierra el remate, faltan cosas.

$((\forall y)\varphi)[x/y][y/x] = (((\forall y)\varphi)[x/y])[y/x] = ((\forall y)\varphi)[y/x]$ hasta ahí vamos bien.

$x \not\in V(\varphi) \Rightarrow x \not\in V((\forall y) \varphi) \Rightarrow x \not\in FV((\forall y) \varphi) \Rightarrow y \text{ libre para } x \text{ en } (\forall y) \varphi$
Faltaría mostrar efectivamente la sustitución:

$((\forall y)\varphi)[y/x] = ((\forall y)\varphi[y/x]) = (\forall y)\varphi$ (justificando estas igualdades).

(En el caso 2 también habría que justificar que x está libre para y en la fórmula, en la primera sustitución).

No te olvides de la clausura de la demostración "Entonces por PIP

$(\bar{\forall} \varphi \in FORM_\mathcal{L}) \mathcal{P}(\varphi)$ ".

Saludos

Re: Segundo Parcial 2010 Ej-1

de Ignacio Rafael Ferreira Urrutia - viernes, 1 de julio de 2016, 20:36

Sí nose porque puse de TERM, es verdad que sino podría ser cualquier elemento de TERM por más que le llame x,y en vez de t.

Hice el lema pero nose si alcanza esa justificación para las variables xi, que como no hay cuantificadores siempre se puede realizar la justificación, si me olvide del final del PIP.

Tendría que haber puesto primero el lema, PIP del lema, la parte de FORM, PIP en FORM pero me quedo en ese orden.

Creo que ahora quedó mejor la parte del para todo:

Re: Segundo Parcial 2010 Ej-1

de Romina Romero - InCo - domingo, 3 de julio de 2016, 20:04

Hola.

En el enunciado del PIP te falta la tesis (penúltima línea del algoritmo que escribí antes). Solo escribiste las hipótesis.

"Hice el lema pero nose si alcanza esa justificación para las variables xi, que como no hay cuantificadores siempre se puede realizar la justificación" El lema está bien. En la sustitución en TERM no hay restricciones, siempre se puede sustituir. La restricción de que el término tiene que estar libre para variable en la fórmula, es solo para sustituciones en FORM.

"Tendría que haber puesto primero el lema, PIP del lema, la parte de FORM, PIP en FORM pero me quedo en ese orden" el lema puede estar después de la demostración por inducción en FORM, eso no es problema. Además es más natural que te des cuenta que precisás el lema una vez que estás metido en la demostración. Lo que sí, yo pondría la conclusión de FORM "como P cumple con el PIP de FORM...." justo después del último paso inductivo en FORM. Y luego el lema. Supongo que a eso te referías con

"si me olvide del final del PIP".

La demostración en general se ve bien.

Saludos

Re: Segundo Parcial 2010 Ej-1

de Ignacio Rafael Ferreira Urrutia - domingo, 3 de julio de 2016, 20:36

Es verdad, que como cumple para esos elementos entonces cumple para todo elemento del conjunto.

Con lo del final del PIP me refería a la primera versión, con "Tendría que haber puesto primero el lema, PIP del lema, la parte de FORM, PIP en FORM pero me quedo en ese orden" me refería a que quería escribirlo de la forma (demostración LEMA - clausura del PIP (TERM)) (demostración FORM - clausura del PIP (FORM)) pero tenía que borrar mucha cosa para que me quedara ordenado.

Ta entonces es mejor que el lema quede después así si lo preciso en la primera inducción ahí me doy cuenta.

Genial, gracias por tomarte el tiempo de leerlo y perdón por el tema de la prolijidad al escribir.

Saludos