Definition:Labeled Tree for Propositional Logic/Ancestor WFF

From ProofWiki
Jump to: navigation, search


Let $\left({T, \mathbf H, \Phi}\right)$ be a labeled tree for propositional logic.

A WFF that is attached to an ancestor node of a node $t$ is called an ancestor WFF of $t$.

So a hypothesis WFF is an ancestor WFF of every node of $T$.

Also known as

An ancestor WFF of $t$ is also referred as just an ancestor of $t$.

When using the term ancestor in this way, take care to avoid confusion with the concept of ancestor node.