# 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.