Definition:Tableau Proof (Propositional Tableaus)

From ProofWiki
Jump to navigation Jump to search

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 = \varnothing$.

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 $\mathcal L_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