Definition:Tableau Proof (Propositional Tableaus)

From ProofWiki
Jump to navigation Jump to search

This page is about tableau proofs in the context of propositional tableaus. For other uses, see Definition: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 \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$, 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 $\mathcal L_0$.

It consists solely of axioms, in the following way:

A WFF $\mathbf A$ is a $\mathrm{PT}$-axiom iff 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