Rule of Addition/Sequent Form/Formulation 2/Form 1

From ProofWiki
Jump to navigation Jump to search

Theorem

$\vdash p \implies \paren {p \lor q}$


Proof 1

By the tableau method of natural deduction:

$p \implies \paren {p \lor q} $
Line Pool Formula Rule Depends upon Notes
1 1 $p$ Premise (None)
2 1 $p \lor q$ Rule of Addition: $\lor \II_1$ 1
3 $p \implies \paren {p \lor q}$ Rule of Implication: $\implies \mathcal I$ 1 – 3 Assumption 1 has been discharged

$\blacksquare$


Proof 2

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

By the tableau method:

$p \implies \paren {p \lor q}$
Line Pool Formula Rule Depends upon Notes
1 $q \implies \paren {p \lor q}$ Axiom $\text A 2$
2 $p \implies \paren {q \lor p}$ Rule $\text {RST} 1$ 1 $p \,/\, q, q \,/\, p$
3 $\paren {p \lor q} \implies \paren {q \lor p}$ Axiom $\text A 3$
4 $\paren {q \lor p} \implies \paren {p \lor q}$ Rule $\text {RST} 1$ 3 $p \,/\, q, q \,/\, p$
5 $p \implies \paren {p \lor q}$ Hypothetical Syllogism 2, 4

$\blacksquare$


Sources