Definition:Propositional Tableau/Construction/Infinite

From ProofWiki
Jump to navigation Jump to search

Definition

An infinite labeled tree $\left({T, \mathbf H, \Phi}\right)$ is a propositional tableau if and only if:

There exists an exhausting sequence of sets $\left({T_n}\right)_{n \in \N}$ of $T$ such that for all $n \in \N$:
$\left({T_n, \mathbf H, \Phi \restriction_{T_n}}\right)$
is a finite propositional tableau, where $\Phi \restriction_{T_n}$ denotes the restriction of $\Phi$ to $T_n$.


Sources