Construir una prueba formal de ciertos argumentos lógicos

Question

Dados los siguientes argumentos:

$ \tag A (R \to \neg S) \land (T \to \neg U)$

$ \tag B (V\to \neg W) \land (X \to \neg Y)$

$ \tag C (T \to W) \land (U \to S)$

$ \tag D V \lor R $

$$ \therefore \neg T \lor \neg U $$

cómo demostrarlo utilizando la norma reglas de inferencia ?

Answer 1

Es de esperar que esto se derive más o menos directamente de $(A)$ porque $p\to q\iff \neg p \lor q$ . Sin embargo, no hay tertium no datur . Hay que encontrar la lucha a partir de (D) mediante el análisis de casos:

Por simplificación de (A): $$\tag{1}R\to\neg S$$ y $$\tag2 T\to\neg U$$ Por simplificación de (C): $$\tag{3}T\to W$$ y $$\tag4 U\to S$$ Por modus ponens de (1): $$\tag 5R\vdash \neg S$$ Por modus tollens de (4) y (5): $$\tag 6 R\vdash \neg U$$ Por adición de (6) $$\tag 7 R\vdash \neg T \lor \neg U$$ Por teorema de la decucción de (6): $$\tag 8 R\to (\neg T \lor \neg U)$$ Por simplificación de (B): $$\tag 9 V\to\neg W$$ Por modus ponens de (9): $$\tag{10} V\vdash \neg W$$ Por modus tollens de (10) y (3): $$\tag{11}V\vdash \neg T$$ Por adición de (11): $$\tag{12}V\vdash \neg T\lor\neg U$$ Por teorema de la deducción de (12) $$\tag{13}V\to( \neg T\lor\neg U)$$ Por análisis de casos de (D), (13) y (8): $$\neg T \lor \neg U_\blacksquare$$

Answer 2

Aquí hay una prueba utilizando un Comprobador de pruebas estilo Fitch :

Las cuatro primeras líneas exponen las premisas. Luego intento considerar los dos casos de la premisa 4 asumiendo cada uno en una subprueba y derivando el objetivo deseado. Una vez hecho esto, puedo utilizar eliminación de la disyunción o análisis de casos (vE) en la línea 17 para completar la prueba.

Dentro de las subpruebas he utilizado eliminación o simplificación de conjuntos (∧E), eliminación condicional o modus ponens (→E), introducción o adición de la disyunción (vI) y modus tollens (MT).

Todas las reglas se encuentran en la lista de la OP reglas de inferencia .

---

Editor y comprobador de pruebas de deducción natural al estilo de JavaScript/PHP de Kevin Klement http://proofs.openlogicproject.org/