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

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

This proof is derived in the context of the following proof system: Instance 2 of the Hilbert-style systems.

By the tableau method:

$\vdash \paren{ p \lor \paren{ q \land r } } \implies \paren{ \paren{ p \lor q } \land \paren{ p \lor r } }$
Line Pool Formula Rule Depends upon Notes
1 $\paren{ q \land r } \implies q$ Rule of Simplification $q / p, r / q$
2 $\paren{ \paren{ q \land r } \implies q } \implies \paren{ \paren{ p \lor \paren{ q \land r } } \implies \paren{ p \lor q } }$ Axiom $A4$ $\paren{ q \land r } \,/\, q, q \,/\, r$
3 $\paren{ p \lor \paren{ q \land r } } \implies \paren{ p \lor q }$ Rule $RST \, 3$ 1,2
4 $\paren{ q \land r } \implies \paren{ r \land q }$ Rule of Commutation $q / p, r / q$
5 $\paren{ r \land q } \implies r$ Rule of Simplification $r / p$
6 $\paren{ q \land r } \implies r$ Hypothetical Syllogism 4,5
7 $\paren{ \paren{ q \land r } \implies r } \implies \paren{ \paren{ p \lor \paren{ q \land r } } \implies \paren{ p \lor r } }$ Axiom $A4$ $\paren{ q \land r } \,/\, q$
8 $\paren{ p \lor \paren{ q \land r } } \implies \paren{ p \lor r }$ Rule $RST \, 3$ 6,7
9 $\paren{ p \lor q } \implies \paren{ \paren{ p \lor r } \implies \paren{ \paren{ p \lor q } \land \paren{ p \lor r } } }$ Rule of Conjunction $\paren{ p \lor q } \,/\, p, \paren{ p \lor r } \,/\, q$
10 $\paren{ p \lor \paren{ q \land r } } \implies \paren{ \paren{ p \lor r } \implies \paren{ \paren{ p \lor q } \land \paren{ p \lor r } } }$ Hypothetical Syllogism 3,9
11 $\paren{ \paren{ p \lor \paren{ q \land r } } \implies \paren{ \paren{ p \lor r } \implies \paren{ p \lor q } \land \paren{ p \lor r } } } \\ \implies \paren{ \paren{ p \lor r } \implies \paren{ \paren{ p \lor \paren{ q \land r } } \implies \paren{ p \lor q } \land \paren{ p \lor r } } }$ Principle of Commutation $\paren{ p \lor \paren{ q \land r } } \,/\, p, \paren{ p \lor r } \,/\, q, \paren{ \paren{ p \lor q } \land \paren{ p \lor r } } \,/\, r$
12 $\paren{ p \lor r } \implies \paren{ \paren{ p \lor \paren{ q \land r } } \implies \paren{ p \lor q } \land \paren{ p \lor r } }$ Rule $RST \, 3$ 10,11
13 $\paren{ p \lor \paren{ q \land r } } \implies \paren{ \paren{ p \lor \paren{ q \land r } } \implies \paren{ p \lor q } \land \paren{ p \lor r } }$ Hypothetical Syllogism 8,12
14 $\paren{ p \lor \paren{ q \land r } } \implies \paren{ p \lor q } \land \paren{ p \lor r }$

$\blacksquare$


Sources