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