Conjunction of Disjunctions Consequence

From ProofWiki
Jump to navigation Jump to search

Theorem

$\left({p \lor q}\right) \land \left({r \lor s}\right) \vdash p \lor r \lor \left({q \land s}\right)$


Proof

By the tableau method of natural deduction:

$\left({p \lor q}\right) \land \left({r \lor s}\right) \vdash \left({p \lor r}\right) \lor \left({q \land s}\right)$
Line Pool Formula Rule Depends upon Notes
1 1 $\left({p \lor q}\right) \land \left({r \lor s}\right)$ Premise (None)
2 1 $\left({p \land \left({r \lor s}\right)}\right) \lor \left({q \land \left({r \lor s}\right)}\right)$ Sequent Introduction 1 Conjunction Distributes over Disjunction
3 $p \land \left({r \lor s}\right) \implies p$ Theorem Introduction (None) Simplification
4 $q \land \left({r \lor s}\right) \implies \left({q \land r}\right) \lor \left({q \land s}\right)$ Theorem Introduction (None) Conjunction Distributes over Disjunction
5 $q \land r \implies r$ Theorem Introduction (None) Simplification
6 $q \land s \implies q \land s$ Theorem Introduction (None) Law of Identity/Formulation 2
7 $\left({q \land r}\right) \lor \left({q \land s}\right) \implies r \lor \left({q \land s}\right)$ Sequent Introduction 5,6 Constructive Dilemma
8 $q \land \left({r \lor s}\right) \implies r \lor \left({q \land s}\right)$ Sequent Introduction 4,7 Hypothetical Syllogism
9 $\left({p \lor q}\right) \land \left({r \lor s}\right) \implies p \lor \left({r \lor \left({q \land s}\right)}\right)$ Sequent Introduction 3,8 Constructive Dilemma
10 1 $p \lor \left({r \lor \left({q \land s}\right)}\right)$ Modus Ponendo Ponens: $\implies \mathcal E$ 9, 1
11 1 $\left({p \lor r}\right) \lor \left({q \land s}\right)$ Sequent Introduction 10 Rule of Association

$\blacksquare$