Definition:Tableau Proof (Propositional Tableaus)
This page is about Tableau Proof in the context of Propositional Tableau. 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 tableaus can informally be regarded as such.
Sources
- 1996: H. Jerome Keisler and Joel Robbin: Mathematical Logic and Computability ... (previous) ... (next): $\S 1.7$: Tableaus: Definition $1.7.4$