User:Lord Farin/Tableau Proof Rules/Or-Elimination
Jump to navigation
Jump to search
Proof by Cases
Given $p \lor q$, $p \vdash r$ and $q \vdash r$, we have also $r$.
| Line | Pool | Formula | Rule | Depends upon | Notes | |
|---|---|---|---|---|---|---|
| $i$ | $i$ | $p$ | Rule of Assumption | ? | ||
| $i+1 .. i'-1$ | ? | ? | ? | ? | Let these lines prove $r$ from assuming $p$ | |
| $i'$ | $I$ | $r$ | ? | only from $i .. i'-1$ | ||
| $j$ | $j$ | $q$ | Rule of Assumption | ? | ||
| $j+1 .. j'-1$ | ? | ? | ? | ? | Let these lines prove $r$ from assuming $q$ | |
| $j'$ | $J$ | $r$ | ? | only from $j .. j'-1$ | ||
| $k$ | $K$ | $p \lor q$ | ? | ? | ||
| $l$ | $I,J,K,$ but NOT $i,j$ | $r$ | Proof by Cases: $\text{PBC}$ | $i .. i', j .. j', k$ |
Wiki code
|-
| align="right" | $l$ ||
| align="right" | $I,J,K,$ but excluding $i,j$
| $r$
| [[Proof by Cases|Proof by Cases: $\text{PBC}$]]
| $i .. i', j .. j', k$