User:Lord Farin/Tableau Proof Rules/Proof by Contradiction
Jump to navigation
Jump to search
Proof by Contradiction
Given $p \vdash \bot$, we have $\neg p$ (without assuming $p$).
Line | Pool | Formula | Rule | Depends upon | Notes | |
---|---|---|---|---|---|---|
$i$ | $i$ | $p$ | ? | ? | ||
$i+1..i'-1$ | ? | ? | ? | ? | Let these lines prove $\bot$ from $p$ | |
$i'$ | $I$ | $\bot$ | ? | only on $i .. i'-1$ | ||
$j$ | $I,$ but NOT $i$ | $\neg p$ | Proof by Contradiction | $i..i'$ |
Wiki code
|- | align="right" | $j$ || | align="right" | $I,$ but NOT $i$ | $\neg p$ | [[Proof by Contradiction]] | $i..i'$