# 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{}$
| <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$

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$

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$
| $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{}$