Proof by Contradiction/Variant 3/Formulation 2/Proof 2

Theorem

$\vdash \paren {p \implies \neg p} \implies \neg p$

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 \implies \neg p} \implies \neg p$

Line		Pool	Formula	Rule	Depends upon	Notes
1			$\paren {p \lor p} \implies p$	Axiom $\text A 1$
2			$\paren {\neg p \lor \neg p} \implies \neg p$	Rule $\text {RST} 1$	1	$\neg p \, / \, p$
3			$\paren {p \implies \neg p} \implies \neg p$	Rule $\text {RST} 2 \, (2)$	2

$\blacksquare$

Sources

• 1959: A.H. Basson and D.J. O'Connor: Introduction to Symbolic Logic (3rd ed.) ... (previous) ... (next): $\S 4.3$: Derivable Formulae: Example $1$