3 votos

¿Cómo puedo eliminar dos subfórmulas conflictivas en dos premisas en una prueba formal?

Problema: Demostrar que $P \lor S$ se desprende de las premisas: $P \lor (Q \land R)$ y $(\lnot Q \lor \lnot R) \lor S$

Hasta ahora he podido demostrar que $(\lnot Q \lor \lnot R)$ equivale a $\lnot (Q \land R)$ usando el teorema de De Morgan y quiero demostrar que esto cancela $(Q \land R)$ pero tengo problemas para llevarlo más allá. Esto es lo que tengo hasta ahora: Formal Proof in FOL

3voto

Bram28 Puntos 18

@lemontree da una buena prueba... pero quiero dar un comentario/consejo general sobre su prueba:

Siempre que iniciar subprueba, debe siempre indique lo que desea en el Finalizar de cada subprueba, antes de entrar en los detalles de la subprueba. Esto es lo que da estructura a la prueba .... y sin ella, te vas a perder, ¡créeme!

Por lo que tienes, puedo decir inmediatamente que no estás haciendo esto ... y por lo tanto se pierden. De hecho, ya que el objetivo que tiene es $P \lor S$ debes intentar que sea la última línea de cada subprueba. Así que, para tu primera subprueba, donde asumes $S$ la última línea que buscas es $P \lor S$ . Por supuesto, esto es una simple $\lor I$ ...pero el hecho de que no lo hayas hecho dice mucho. De hecho, para la segunda subprueba, aunque has probado a DeMorgan, una vez más no has indicado qué es lo que quieres al final de la subprueba ... que una vez más debería ser $P \lor S$ .

Por lo tanto, su configuración inicial debe ser:

enter image description here

Con lo que se puede hacer un seguimiento:

enter image description here

Y a partir de ahí... ¿ves cómo funciona? En primer lugar se hace el montaje/organización/plan/esqueleto de la prueba .. y entonces se resuelven los detalles

1voto

lemontree Puntos 61

No tienes que dar el rodeo de probar la ley DeMorgan $\neg Q \lor \neg R \leftrightarrow \neg(Q \land R)$ y luego derivar una contradicción a $Q \land R$ , en cambio se puede mostrar la contradicción directamente, donde la principal operación que se realiza es una elminación de la disyunción en la premisa $\neg Q \lor \neg R$ . Es decir, tienes dos subpruebas, una que comienza con la suposición $\neg Q$ y uno que comienza con $\neg R$ y cada uno de estos supuestos conducirá a una contradicción. Una suposición contradice $Q$ y una $R$ , de los cuales podemos salirnos $Q \land R$ . Y entonces, como sabes que al menos uno de $\neg Q$ o $\neg R$ y cualquiera de ellas conduce a una contradicción, se puede concluir que la fórmula $\neg Q \lor \neg R$ lleva a una contradicción. Ya estabas en el camino correcto al hacer la eliminación de la disyunción en $\neg Q \lor \neg R$ y el inicio de dos subprofos con $\neg Q$ y $\neg R$ respectivamente, es que no se necesita la fórmula $\neg(\neg Q \lor \neg R)$ en cualquier parte de tu prueba, puedes simplemente derivar la contradicción entre $\neg Q \lor \neg R$ y $Q \land R$ directamente:

enter image description here

(También se podría derivar ahora una dirección de una de las leyes de De Morgan en dos pasos más haciendo $\neg$ Introducir en uno de los locales (ya sea $Q \land R \vdash \neg(\neg Q \lor \neg R)$ o $\neg Q \lor\neg R \vdash \neg(Q \land R)$ pero esto no es necesario, porque ya tenemos la contradicción deseada).

De esta contradicción podemos entonces, aplicando ex falso quodlibet, concluir cualquier fórmula que nos convenga. Aquí nos interesa la fórmula $P \lor S$ . Por cierto, esta debería ser también la fórmula que se deduce de la hipótesis $S$ más arriba, ya que $P \lor S$ es la fórmula que necesitamos mostrar eventualmente, y queremos derivarla haciendo $\lor$ eliminación en la premisa $(\neg Q \lor \neg R) \lor S$ , por lo que necesitamos $P \lor S$ para ser la conclusión de las dos subpruebas que comienzan con $S$ y con $\neg Q \lor \neg P$ .

Sin embargo, es más fácil hacer el anidamiento de las subpruebas al revés de lo que se empezó y en su lugar tener el $\lor$ eliminación en $P \lor (Q \land R)$ sea la operación más externa y el $ \lor$ eliminación en $(\neg Q \lor R) \lor S$ en su interior, así que este es el aspecto de la prueba final:

enter image description here

1voto

user11300 Puntos 116

Creo que es más sencillo utilizar la resolución.

  1. (P V Q) por clausura
  2. (P V R) por clausura
  3. ((¬Q∨¬R)∨S) premisa
  4. ((P V $\lnot$ R) $\lor$ S) 1, 3 resolución
  5. (P $\lor$ S) 2, 4 resolución

i-Ciencias.com

I-Ciencias es una comunidad de estudiantes y amantes de la ciencia en la que puedes resolver tus problemas y dudas.
Puedes consultar las preguntas de otros usuarios, hacer tus propias preguntas o resolver las de los demás.

Powered by:

X