Definition:Tableau Proof (Propositional Tableaux)

This page is about Tableau Proof in the context of propositional tableaux. For other uses, see Tableau Proof.

Definition

Let $\mathbf H$ be a set of WFFs of propositional logic.

Let $\mathbf A$ be a WFF.

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

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

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

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

$\mathbf H \vdash_{\mathrm{PT} } \mathbf A$

Specifically, the notation:

$\vdash_{\mathrm{PT} } \mathbf A$

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

Proof System

Tableau proofs form a proof system $\mathrm{PT}$ for the language of propositional logic $\LL_0$.

It consists solely of axioms, in the following way:

A WFF $\mathbf A$ is a $\mathrm{PT}$-axiom if and only if there exists a tableau proof of $\mathbf A$.

Likewise, we can define the notion of provable consequence for $\mathrm{PT}$:

A WFF $\mathbf A$ is a $\mathrm{PT}$-provable consequence of a collection of WFFs $\mathbf H$ if there exists a tableau proof of $\mathbf A$ from $\mathbf H$.

Although formally $\mathrm{PT}$ has no rules of inference, the rules for the definition of propositional tableaux can informally be regarded as such.

Linguistic Note

The word tableau originates from the French language, where it means array, display, or table (in the sense of data presentation).

Hence the plural form of tableau is tableaux, although the US generally uses tableaus.

Tableaux is the preferred form on $\mathsf{Pr} \infty \mathsf{fWiki}$.

Sources

• 1996: H. Jerome Keisler and Joel Robbin: Mathematical Logic and Computability ... (previous) ... (next): $\S 1.7$: Tableaus: Definition $1.7.4$