Definition:Labeled Tree for Propositional Logic

From ProofWiki
Jump to navigation Jump to search


A labeled tree for propositional logic is a system containing:

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


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