Definition:Tableau Proof (Formal Systems)

From ProofWiki
Jump to navigation Jump to search

This page is about tableau proofs as a presentation technique for proofs in the context of formal systems. For other uses, see Definition:Tableau Proof.

Definition

A tableau proof for a proof system is a technique for presenting a logical argument 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.


At the end of the proof, use the {{EndTableau}} template:

{{EndTableau}}


Sources