Definition:Tableau Proof

From ProofWiki

Jump to: navigation, search

Definition

There are two kinds of tableau proof in the study of propositional logic.

A tableau proof by natural deduction is a technique for presenting a logical argument in a straightforward, standard form.

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 five 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 formula or statement form introduced on this line.
Rule: The justification for introducing this line. This should be the appropriate abbreviation of the proof rule being used to derive this line, for example:

Depends on: The lines (if any) upon which this line directly depends. For premises and assumptions, this field will be empty.

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

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

Let $\mathbf H$ be a set of premises in the form of WFFs of propositional calculus.

A tableau proof of $\mathbf A$ from $\mathbf H$ is a tableau confutation of $\mathbf H \cup \left\{{\neg \mathbf A}\right\}$.

This definition also applies when $\mathbf H = \varnothing$.

Then a tableau proof of $\mathbf A$ is a tableau confutation of $\left\{{\neg \mathbf A}\right\}$.

If there exists a tableau proof of $\mathbf A$ from $\mathbf H$, we can write:

$\mathbf H \vdash \mathbf A$

using the same symbology (and meaning) as logical implication.

Similarly, the notation:

$\vdash \mathbf A$

means that

there exists a tableau proof of $\mathbf A$.

Since, by definition, a tableau confutation is a finite propositional tableau, it follows that all tableau proofs have a finite number of nodes.