User:Lord Farin/Tableau Proof Rules/Proof by Contradiction

From ProofWiki
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'$