# Definition:Tableau Proof (Formal Systems)

*This page is about tableau proofs in the context of proof systems. For other uses, see Tableau Proof.*

## Definition

A **tableau proof** for a proof system is a technique for presenting a logical argument in the form of a formal proof in a straightforward, standard form.

On $\mathsf{Pr} \infty \mathsf{fWiki}$, the proof system is usually natural deduction.

A **tableau proof** is a sequence of lines specifying the order of premises, assumptions, inferences and conclusion in support of an argument.

Each line of a **tableau proof** has a particular format. It consists of the following parts:

**Line:**The line number of the proof. This is a simple numbering from 1 upwards.**Pool:**The list of all the lines containing the pool of assumptions for the formula introduced on this line.**Formula:**The propositional formula introduced on this line.**Rule:**The justification for introducing this line. This should be the rule of inference being used to derive this line.**Depends on:**The lines (if any) upon which this line*directly*depends. For premises and assumptions, this field will be empty.

Optionally, a comment may be added to explicitly point out possible intricacies.

If any assumptions are discharged on a certain line, for the sake of clarity it is preferred that such be mentioned explicitly in a comment.

At the end of a tableau proof, the only lines upon which the proof depends may be those which contain the premises.

### Length

The **length** of a tableau proof is the number of lines it has.

## Technical Note

When constructing a **tableau proof**, use the `{{BeginTableau}}`

template to start it:

`{{BeginTableau|statement|proof system}}`

where:

`statement`

is the statement of logic that is to be proved,**without**the`$ ... $`

delimiters`proof system`

is a link (optional) to page containing the specific proof system in which this proof is valid.

Then, lines can be added to the proof by using the `{{TableauLine}}`

template, or specific variants of it as listed on Category:Tableau Proof Templates.

At the end of the proof, use the `{{EndTableau}}`

template:

`{{EndTableau}}`

## Sources

- 1959: A.H. Basson and D.J. O'Connor:
*Introduction to Symbolic Logic*(3rd ed.) ... (previous) ... (next): $\S 4.3$: Derivable Formulae - 1965: E.J. Lemmon:
*Beginning Logic*... (previous) ... (next): Chapter $1$: The Propositional Calculus $1$: $2$ Conditionals and Negation - 2000: Michael R.A. Huth and Mark D. Ryan:
*Logic in Computer Science: Modelling and reasoning about systems*... (previous) ... (next): $\S 1.2.1$: Rules for natural deduction - 2009: Kenneth Kunen:
*The Foundations of Mathematics*... (previous) ... (next): $\text{II}.10$ Formal Proofs: Definition $\text{II}.10.3$ - 2012: M. Ben-Ari:
*Mathematical Logic for Computer Science*(3rd ed.) ... (previous) ... (next): $\S 3.2$