Definition:Labeled Tree for Propositional Logic
Definition
A labeled tree for propositional logic is a system containing:
- A rooted tree $T$;
- A countable set $\mathbf H$ of WFFs of propositional logic;
- A WFF $\Phi \left({t}\right)$ attached to each non-root node $t$ of $T$.
Such a structure can be denoted $\left({T, \mathbf H, \Phi}\right)$.
Hypothesis Set
The countable set $\mathbf H$ of WFFs of propositional logic is called the hypothesis set.
The elements of $\mathbf H$ are known as hypothesis WFFs.
The hypothesis set $\mathbf H$ is considered to be attached to the root node of $T$.
Attached
Let $t$ be a non-root node of $T$.
Let $\mathbf A$ be a WFF.
Then $\mathbf A$ is attached to $t$ if and only if $\mathbf A = \Phi \left({t}\right)$.
Child WFF
A WFF that is attached to a child of a node $t$ is called a child WFF of $t$.
Ancestor WFF
A WFF that is attached to an ancestor node of a node $t$ is called an ancestor WFF of $t$.
Along a Branch
Let $\Gamma$ be a branch of $T$.
Let $\mathbf A$ be a WFF that is attached to a node $t \in \Gamma$.
Then $\mathbf A$ occurs along $\Gamma$.
This includes the case where $\mathbf A \in \mathbf H$, that is, $\mathbf A$ is attached to the root node.
Also denoted as
For ease of notation, one often writes $T$ in place of the more cumbersome $\left({T, \mathbf H, \Phi}\right)$ when this does not give rise to ambiguity.
Also see
Sources
- 1996: H. Jerome Keisler and Joel Robbin: Mathematical Logic and Computability ... (previous) ... (next): $\S 1.7$: Tableaus