Rule of Distribution/Disjunction Distributes over Conjunction/Left Distributive/Formulation 2/Forward Implication/Proof 1

From ProofWiki
Jump to navigation Jump to search

Theorem

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


Proof


Using a tableau proof for instance 1 of a Gentzen proof system:


$\vdash \left({p \lor \left({q \land r}\right)}\right) \implies \left({\left({p \lor q}\right) \land \left({p \lor r}\right)}\right)$
Line Pool Formula Rule Depends upon Notes
1 $\neg p, p, q$ Axiom
2 $\neg p, p \lor q$ $\beta$-Rule: $\beta\lor$ 1
3 $\neg p, p, r$ Axiom
4 $\neg p, p \lor r$ $\beta$-Rule: $\beta\lor$ 3
5 $\neg p, \left({p \lor q}\right) \land \left({p \lor r}\right)$ $\alpha$-Rule: $\alpha\land$ 2, 4
6 $\neg q, \neg r, p, q$ Axiom
7 $\neg q, \neg r, p \lor q$ $\beta$-Rule: $\beta\lor$ 6
8 $\neg q, \neg r, p, r$ Axiom
9 $\neg q, \neg r, p \lor r$ $\beta$-Rule: $\beta\lor$ 8
10 $\neg q, \neg r, \left({p \lor q}\right) \land \left({p \lor r}\right)$ $\alpha$-Rule: $\alpha\land$ 7, 9
11 $\neg \left({q \land r}\right), \left({p \lor q}\right) \land \left({p \lor r}\right)$ $\beta$-Rule: $\beta\land$ 10
12 $\neg \left({p \lor \left({q \land r}\right)}\right), \left({p \lor q}\right) \land \left({p \lor r}\right)$ $\alpha$-Rule: $\alpha\lor$ 5, 11
13 $\left({p \lor \left({q \land r}\right)}\right) \implies \left({ \left({p \lor q}\right) \land \left({p \lor r}\right)}\right)$ $\beta$-Rule: $\beta\implies$ 12

$\blacksquare$


Sources