Definition:Tableau Proof (Formal Systems)

From ProofWiki
Jump to navigation Jump to search

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