User:Lord Farin/Tableau Proof Rules
Jump to navigation
Jump to search
General form of Tableau proof
The tableau proofs work with tables and general lines like this:
| Line | Pool | Formula | Rule | Depends upon | Notes | |
|---|---|---|---|---|---|---|
| <line number> | <line numbers> | $\ldots{}$ | link to ProofWiki entry | <line numbers> |
Wiki code
{| border="1"
|-
! Line !!
! Pool
! Formula
! Rule
! Depends upon
! Notes
|-
| align="right" | <line number> ||
| align="right" | <line numbers>
| $\ldots{}$
| [[link to ProofWiki entry]]
| <line numbers>
|}
Axioms
Throughout, $i, j \ldots$ denote arbitrary line numbers in a tableau proof.
Capital letters $I, J \ldots$ denote arbitrary sets of line numbers.
Assumption
Introduces an additional assumption $p$.
| Line | Pool | Formula | Rule | Depends upon | Notes | |
|---|---|---|---|---|---|---|
| $i$ | $i$ | $p$ | Rule of Assumption | (None) |
Wiki code
|- | align="right" | $i$ || | align="right" | $i$ | $p$ | [[Rule of Assumption]] | (None)
Conjunction
Given statements $p$ and $q$, we have also $p \land q$ and $q \land p$.
| Line | Pool | Formula | Rule | Depends upon | Notes | |
|---|---|---|---|---|---|---|
| $i$ | $I$ | $p$ | ? | ? | ||
| $j$ | $J$ | $q$ | ? | ? | ||
| $k$ | $I,J$ | $p \land q$ | Rule of Conjunction | $i,j$ | ||
| $l$ | $I,J$ | $q \land p$ | Rule of Conjunction | $i,j$ |
Wiki code
|- | align="right" | $k$ || | align="right" | $I,J$ | $p \land q$ | [[Rule of Conjunction]] | $i,j$ |- | align="right" | $l$ || | align="right" | $I,J$ | $q \land p$ | [[Rule of Conjunction]] | $i,j$
Simplification
Given $p \land q$, we have also $p$ and $q$.
| Line | Pool | Formula | Rule | Depends upon | Notes | |
|---|---|---|---|---|---|---|
| $i$ | $I$ | $p \land q$ | ? | ? | ||
| $j$ | $I$ | $p$ | Rule of Simplification: $\land \mathcal E_1$ | $i$ | ||
| $k$ | $I$ | $q$ | Rule of Simplification: $\land \mathcal E_2$ | $i$ |
Wiki code
|- | align="right" | $j$ || | align="right" | $I$ | $p$ | [[Rule of Simplification|Rule of Simplification: $\land \mathcal E_1$]] | $i$ |- | align="right" | $k$ || | align="right" | $I$ | $q$ | [[Rule of Simplification|Rule of Simplification: $\land \mathcal E_2$]] | $i$
Addition
Given statement $p$, we have also $p \lor q$ and $q \lor p$.
| Line | Pool | Formula | Rule | Depends upon | Notes | |
|---|---|---|---|---|---|---|
| $i$ | $I$ | $p$ | ? | ? | ||
| $j$ | $I$ | $p \lor q$ | $\lor \mathcal I_1$ | $i$ | ||
| $k$ | $I$ | $q \lor p$ | $\lor \mathcal I_2$ | $i$ |
Wiki code
|- | align="right" | $j$ || | align="right" | $I$ | $p \lor q$ | [[Rule of Addition|$\lor \mathcal I_1$]] | $i$ |- | align="right" | $k$ || | align="right" | $I$ | $q \lor p$ | [[Rule of Addition|$\lor \mathcal I_2$]] | $i$
Or-Elimination
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$
Modus Ponens
Given statements $p$ and $p \implies q$, we also have $q$.
| Line | Pool | Formula | Rule | Depends upon | Notes | |
|---|---|---|---|---|---|---|
| $i$ | $I$ | $p$ | ? | ? | ||
| $j$ | $J$ | $p \implies q$ | ? | ? | ||
| $k$ | $I,J$ | $q$ | Modus Ponendo Ponens: $\implies \mathcal E$ | $i,j$ |
Wiki code
|- | align="right" | $k$ || | align="right" | $I,J$ | $q$ | [[Modus Ponendo Ponens|Modus Ponendo Ponens: $\implies \mathcal E$]] | $i,j$
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'$
Not-Elimination
Given $p, \neg q$, we have contradiction ($\bot$).
| Line | Pool | Formula | Rule | Depends upon | Notes | |
|---|---|---|---|---|---|---|
| $i$ | $I$ | $p$ | ? | ? | ||
| $j$ | $J$ | $\neg p$ | ? | ? | ||
| $k$ | $I,J$ | $\bot$ | Principle of Non-Contradiction: $\neg \mathcal E$ | $i,j$ |
Wiki code
|- | align="right" | $k$ || | align="right" | $I,J$ | $\bot$ | [[Principle of Non-Contradiction|Principle of Non-Contradiction: $\neg \mathcal E$]] | $i,j$
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'$
Bottom-Elimination
Given $\bot$, we have any $p$.
| Line | Pool | Formula | Rule | Depends upon | Notes | |
|---|---|---|---|---|---|---|
| $i$ | $I$ | $\bot$ | ? | ? | ||
| $j$ | $I$ | $p$ | Rule of Explosion: $\bot \mathcal E$ | $i$ |
Wiki code
|- | align="right" | $j$ || | align="right" | $I$ | $p$ | [[Rule of Explosion|Rule of Explosion: $\bot \mathcal E$]] | $i$
Excluded Middle
This axiom is denied by the intuitionistic school.
We have $p \lor \neg p$ for any $p$.
| Line | Pool | Formula | Rule | Depends upon | Notes | |
|---|---|---|---|---|---|---|
| $i$ | (None) | $p \lor \neg p$ | Law of Excluded Middle | (None) |
Wiki code
|- | align="right" | $i$ || | align="right" | (None) | $p \lor \neg p$ | [[Law of Excluded Middle]] | (None)
Abbreviations for Derived results
Many results are too common to derive every time, and therefore have been assigned an abbreviation for use in tableau proofs.
A listing is below; here is a template for a tableau proof row:
{| border="1"
|-
! Line !!
! Pool
! Formula
! Rule
! Depends upon
! Notes
|-
| align="right" | <line number> ||
| align="right" | <line numbers>
| $\ldots{}$
| [[link to ProofWiki entry]]
| <line numbers>
|}
It is understood that all abbreviation links below are to be put in the fourth column of such a row.
Abbreviations and links
- Absorption Laws (Logic): $\mathrm {AL}$; [[Absorption Laws (Logic)|$\mathrm {AL}$]]
- Constructive Dilemma: $\mathrm {CD}$; [[Constructive Dilemma|$\mathrm {CD}$]]
- De Morgan's Laws (Logic): $\mathrm {DM}$; [[De Morgan's Laws (Logic)|$\mathrm {DM}$]]
- Destructive Dilemma: $\mathrm {DD}$; [[Destructive Dilemma|$\mathrm {DD}$]]
- Double Negation Elimination: $\neg \neg \mathcal E$; [[Double Negation Elimination|$\neg \neg \mathcal E$]]
- Double Negation Introduction: $\neg \neg \mathcal I$; [[Double Negation Introduction|$\neg \neg \mathcal I$]]
- Hypothetical Syllogism: $\mathrm {HS}$; [[Hypothetical Syllogism|$\mathrm {HS}$]]
- Modus Ponendo Tollens: $\mathrm {MPT}$; [[Modus Ponendo Tollens|$\mathrm {MPT}$]]
- Modus Tollendo Ponens: $\mathrm {MTP}$; [[Modus Tollendo Ponens|$\mathrm {MTP}$]]
- Modus Tollendo Tollens: $\mathrm {MTT}$; [[Modus Tollendo Tollens|$\mathrm {MTT}$]]
- Praeclarum Theorema: $\mathrm {PT}$; [[Praeclarum Theorema|$\mathrm {PT}$]]
- Proof by Cases: $\mathrm {PBC}$; [[Proof by Cases|$\mathrm {PBC}$]]
- Reductio ad Absurdum: $\mathrm {RAA}$; [[Reductio ad Absurdum|$\mathrm {RAA}$]]
- Rule of Association: $\mathrm {Assoc}$; [[Rule of Association|$\mathrm {Assoc}$]]
- Rule of Commutation: $\mathrm {Comm}$; [[Rule of Commutation|$\mathrm {Comm}$]]
- Rule of Distribution: $\mathrm {Dist}$; [[Rule of Distribution|$\mathrm {Dist}$]]
- Rule of Idempotence: $\mathrm {Idemp}$; [[Rule of Idempotence|$\mathrm {Idemp}$]]
- Rule of Transposition: $\mathrm {TP}$; [[Rule of Transposition|$\mathrm {TP}$]]
For any other theorem to be cited, use:
- Rule of Theorem Introduction: $\mathrm {TI}$; [[Rule of Theorem Introduction|$\mathrm {TI}$]]
It is required to give a reference to the origin of your result (in the optional sixth Notes column). If it is not on ProofWiki, make a page for it, even if you don't know the proof.