User:Lord Farin/Tableau Proof Rules
From ProofWiki
Contents |
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$ | $\textrm A$ | (None) |
Wiki code
|- | align="right" | $i$ || | align="right" | $i$ | $p$ | [[Axiom:Rule of Assumption|$\textrm A$]] | (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$ | $\land \mathcal I$ | $i,j$ | ||
| $l$ | $I,J$ | $q \land p$ | $\land \mathcal I$ | $i,j$ |
Wiki code
|- | align="right" | $k$ || | align="right" | $I,J$ | $p \land q$ | [[Axiom:Rule of Conjunction|$\land \mathcal I$]] | $i,j$ |- | align="right" | $l$ || | align="right" | $I,J$ | $q \land p$ | [[Axiom:Rule of Conjunction|$\land \mathcal I$]] | $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$ | $\land \mathcal E_1$ | $i$ | ||
| $k$ | $I$ | $q$ | $\land \mathcal E_2$ | $i$ |
Wiki code
|- | align="right" | $j$ || | align="right" | $I$ | $p$ | [[Axiom:Rule of Simplification|$\land \mathcal E_1$]] | $i$ |- | align="right" | $k$ || | align="right" | $I$ | $q$ | [[Axiom: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$ | [[Axiom:Rule of Addition|$\lor \mathcal I_1$]] | $i$ |- | align="right" | $k$ || | align="right" | $I$ | $q \lor p$ | [[Axiom: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$ | $\textrm A$ | ? | ||
| $i+1 .. i'-1$ | ? | ? | ? | ? | Let these lines prove $r$ from assuming $p$ | |
| $i'$ | $I$ | $r$ | ? | only from $i .. i'-1$ | ||
| $j$ | $j$ | $q$ | $\textrm A$ | ? | ||
| $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$ | $\lor \mathcal E$ | $i .. i', j .. j', k$ |
Wiki code
|- | align="right" | $l$ || | align="right" | $I,J,K,$ but excluding $i,j$ | $r$ | [[Axiom:Rule of Or-Elimination|$\lor \mathcal E$]] | $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$ | $\implies \mathcal E$ | $i,j$ |
Wiki code
|- | align="right" | $k$ || | align="right" | $I,J$ | $q$ | [[Axiom: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$ | $\textrm A$ | ? | ||
| $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$ | $\implies \mathcal I$ | $i .. i'$ |
Wiki code
|- | align="right" | $j$ || | align="right" | $I,$ but NOT $i$ | $p \implies q$ | [[Axiom: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$ | $\neg \mathcal E$ | $i,j$ |
Wiki code
|- | align="right" | $k$ || | align="right" | $I,J$ | $\bot$ | [[Axiom:Rule of Not-Elimination|$\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$ | $\neg \mathcal I$ | $i..i'$ |
Wiki code
|- | align="right" | $j$ || | align="right" | $I,$ but NOT $i$ | $\neg p$ | [[Axiom:Proof by Contradiction|$\neg \mathcal I$]] | $i..i'$
Bottom-Elimination
Given $\bot$, we have any $p$.
| Line | Pool | Formula | Rule | Depends upon | Notes | |
|---|---|---|---|---|---|---|
| $i$ | $I$ | $\bot$ | ? | ? | ||
| $j$ | $I$ | $p$ | $\bot \mathcal E$ | $i$ |
Wiki code
|- | align="right" | $j$ || | align="right" | $I$ | $p$ | [[Axiom:Rule of Bottom-Elimination|$\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$ | $\textrm {LEM}$ | (None) |
Wiki code
|-
| align="right" | $i$ ||
| align="right" | (None)
| $p \lor \neg p$
| [[Axiom:Law of Excluded Middle|$\textrm {LEM}$]]
| (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: $\mathrm {AL}$;
[[Absorption Laws|$\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.
