# Constructing a formal proof of certain logical arguments

Given the following arguments:

$\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$$

how to prove this using the standard rules of inference?

-

One expects this to follow more or less directly from $(A)$ because $p\to q\iff \neg p \lor q$. However, there is no tertium no datur. One has to find ones luch starting from (D) by case analysis:
By simplification from (A): $$\tag{1}R\to\neg S$$ and $$\tag2 T\to\neg U$$ By simplification from (C): $$\tag{3}T\to W$$ and $$\tag4 U\to S$$ By modus ponens from (1): $$\tag 5R\vdash \neg S$$ By modus tollens from (4) and (5): $$\tag 6 R\vdash \neg U$$ By addition from (6) $$\tag 7 R\vdash \neg T \lor \neg U$$ By decuction theorem from (6): $$\tag 8 R\to (\neg T \lor \neg U)$$ By simplification from (B): $$\tag 9 V\to\neg W$$ By modus ponens from (9): $$\tag{10} V\vdash \neg W$$ By modus tollens from (10) and (3): $$\tag{11}V\vdash \neg T$$ By addition from (11): $$\tag{12}V\vdash \neg T\lor\neg U$$ By deduction theorem from (12) $$\tag{13}V\to( \neg T\lor\neg U)$$ By case analysis from (D), (13) and (8): $$\neg T \lor \neg U_\blacksquare$$