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$ ... $
delimitersproof 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$