Category:Propositional Tableaus
This category contains results about Propositional Tableaus.
Definitions specific to this category can be found in Definitions/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.
Subcategories
This category has only the following subcategory.
Pages in category "Propositional Tableaus"
The following 25 pages are in this category, out of 25 total.