Category:Definitions/Propositional Tableaus

From ProofWiki
Jump to navigation Jump to search

This category contains definitions related to Propositional Tableaus.
Related results can be found in Category:Propositional Tableaus.


The finite propositional tableaus are precisely those labeled trees singled out by the following bottom-up grammar:

$\boxed{\mathrm{Root}}$ A labeled tree whose only node is its root node is a finite propositional tableau.
For the following clauses, let $t$ be a leaf node of a finite propositional tableau $T$.
$\boxed{\neg \neg}$ If $\neg \neg \mathbf A$ is an ancestor WFF of $t$, the labeled tree obtained from $T$ by adding:
a child $s$ to $t$, with $\Phi \left({s}\right) = \mathbf A$

is a finite propositional tableau.

$\boxed \land$ If $\mathbf A \land \mathbf B$ is an ancestor WFF of $t$, the labeled tree obtained from $T$ by adding:
a child $s$ to $t$, with $\Phi \left({s}\right) = \mathbf A$
a child $r$ to $s$, with $\Phi \left({r}\right) = \mathbf B$

is a finite propositional tableau.

$\boxed{\neg \land}$ If $\neg \left({\mathbf A \land \mathbf B}\right)$ is an ancestor WFF of $t$, the labeled tree obtained from $T$ by adding:
a child $s$ to $t$, with $\Phi \left({s}\right) = \neg\mathbf A$
another child $s'$ to $t$, with $\Phi \left({s'}\right) = \neg\mathbf B$

is a finite propositional tableau.

$\boxed \lor$ If $\mathbf A \lor \mathbf B$ is an ancestor WFF of $t$, the labeled tree obtained from $T$ by adding:
a child $s$ to $t$, with $\Phi \left({s}\right) = \mathbf A$
another child $s'$ to $t$, with $\Phi \left({s'}\right) = \mathbf B$

is a finite propositional tableau.

$\boxed{\neg\lor}$ If $\neg \left({\mathbf A \lor \mathbf B}\right)$ is an ancestor WFF of $t$, the labeled tree obtained from $T$ by adding:
a child $s$ to $t$, with $\Phi \left({s}\right) = \neg\mathbf A$
a child $r$ to $s$, with $\Phi \left({r}\right) = \neg \mathbf B$

is a finite propositional tableau.

$\boxed \implies$ If $\mathbf A \implies \mathbf B$ is an ancestor WFF of $t$, the labeled tree obtained from $T$ by adding:
a child $s$ to $t$, with $\Phi \left({s}\right) = \neg\mathbf A$
another child $s'$ to $t$, with $\Phi \left({s'}\right) = \mathbf B$

is a finite propositional tableau.

$\boxed{\neg\implies}$ If $\neg \left({\mathbf A \implies \mathbf B}\right)$ is an ancestor WFF of $t$, the labeled tree obtained from $T$ by adding:
a child $s$ to $t$, with $\Phi \left({s}\right) = \mathbf A$
a child $r$ to $s$, with $\Phi \left({r}\right) = \neg \mathbf B$

is a finite propositional tableau.

$\boxed \iff$ If $\mathbf A \iff \mathbf B$ is an ancestor WFF of $t$, the labeled tree obtained from $T$ by adding:
a child $s$ to $t$, with $\Phi \left({s}\right) = \mathbf A \land \mathbf B$
another child $s'$ to $t$, with $\Phi \left({s'}\right) = \neg \mathbf A \land \neg\mathbf B$

is a finite propositional tableau.

$\boxed{\neg\iff}$ If $\neg \left({\mathbf A \iff \mathbf B}\right)$ is an ancestor WFF of $t$, the labeled tree obtained from $T$ by adding:
a child $s$ to $t$, with $\Phi \left({s}\right) = \mathbf A \land \neg \mathbf B$
another child $s'$ to $t$, with $\Phi \left({s'}\right) = \neg \mathbf A \land \mathbf B$

is a finite propositional tableau.

Note how the boxes give an indication of the ancestor WFF mentioned in the clause.

These clauses together are called the tableau extension rules.

Pages in category "Definitions/Propositional Tableaus"

The following 32 pages are in this category, out of 32 total.