Rule of Commutation/Disjunction/Formulation 2/Forward Implication

From ProofWiki
Jump to navigation Jump to search


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


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

$\vdash \left({p \lor q}\right) \implies \left({q \lor p}\right)$
Line Pool Formula Rule Depends upon Notes
1 $\neg p, q, p$ Axiom
2 $\neg q, q, p$ Axiom
3 $\neg \left({p \lor q}\right), q, p$ $\alpha$-Rule: $\alpha\lor$ 1, 2
4 $\neg \left({p \lor q}\right), q \lor p$ $\beta$-Rule: $\beta\lor$ 3
5 $\left({p \lor q}\right) \implies \left({q \lor p}\right)$ $\beta$-Rule: $\beta\implies$ 4


Also see