Constructive Dilemma/Formulation 2

From ProofWiki
Jump to navigation Jump to search

Theorem

$\vdash \paren {\paren {p \lor r} \land \paren {p \implies q} \land \paren {r \implies s} } \implies \paren {q \lor s}$


Proof

By the tableau method of natural deduction:

$\vdash \paren {\paren {p \lor r} \land \paren {p \implies q} \land \paren {r \implies s} } \implies \paren {q \lor s} $
Line Pool Formula Rule Depends upon Notes
1 1 $\paren {\paren {p \lor r} \land \paren {p \implies q} \land \paren {r \implies s} }$ Assumption (None)
2 1 $\paren {p \implies q} \land \paren {r \implies s}$ Rule of Simplification: $\land \mathcal E_2$ 1 Cutting corners: should use Associativity first
3 1 $\paren {p \lor r} \implies \paren {q \lor s}$ Sequent Introduction 2 Constructive Dilemma: Formulation 1
4 1 $p \lor r$ Rule of Simplification: $\land \mathcal E_1$ 1
5 1 $q \lor s$ Modus Ponendo Ponens: $\implies \mathcal E$ 3, 4
6 $\paren {\paren {p \lor r} \land \paren {p \implies q} \land \paren {r \implies s} } \implies \paren {q \lor s}$ Rule of Implication: $\implies \mathcal I$ 1 – 5 Assumption 1 has been discharged

$\blacksquare$


Sources