Definition:Finished
Jump to navigation
Jump to search
Definition
Finished Set of WFFs of Propositional Logic
Let $\Delta$ be a set of WFFs of propositional logic.
Then $\Delta$ is finished if and only if:
- $\Delta$ is not contradictory
- For each WFF $\mathbf C \in \Delta$, either $\mathbf C$ is basic or one of the following is true:
- $\mathbf C$ has the form $\neg \neg \mathbf A$ where $\mathbf A \in \Delta$
- $\mathbf C$ has the form $\paren {\mathbf A \land \mathbf B}$ where both $\mathbf A \in \Delta$ and $\mathbf B \in \Delta$
- $\mathbf C$ has the form $\neg \paren {\mathbf A \land \mathbf B}$ where either $\neg \mathbf A \in \Delta$ or $\neg \mathbf B \in \Delta$
- $\mathbf C$ has the form $\paren {\mathbf A \lor \mathbf B}$ where either $\mathbf A \in \Delta$ or $\mathbf B \in \Delta$
- $\mathbf C$ has the form $\neg \paren {\mathbf A \lor \mathbf B}$ where both $\neg \mathbf A \in \Delta$ and $\neg \mathbf B \in \Delta$
- $\mathbf C$ has the form $\paren {\mathbf A \implies \mathbf B}$ where either $\neg \mathbf A \in \Delta$ or $\mathbf B \in \Delta$
- $\mathbf C$ has the form $\neg \paren {\mathbf A \implies \mathbf B}$ where both $\mathbf A \in \Delta$ and $\neg \mathbf B \in \Delta$
- $\mathbf C$ has the form $\paren {\mathbf A \iff \mathbf B}$ where either:
- both $\mathbf A \in \Delta$ and $\mathbf B \in \Delta$, or:
- both $\neg \mathbf A \in \Delta$ and $\neg \mathbf B \in \Delta$;
- $\mathbf C$ has the form $\neg \paren {\mathbf A \iff \mathbf B}$ where either:
- both $\mathbf A \in \Delta$ and $\neg \mathbf B \in \Delta$
- or:
- both $\neg \mathbf A \in \Delta$ and $\mathbf B \in \Delta$.
Finished Branch of Propositional Tableau
Let $T$ be a propositional tableau.
Let $\Gamma$ be a branch of $T$.
Then $\Gamma$ is finished if and only if:
- $(1): \quad \Gamma$ is not contradictory
- $(2): \quad$ Every non-basic WFF on $\Gamma$ is used at some node of $\Gamma$.
That is, $\Gamma$ is finished if and only if the set $\Delta$ of WFFs of propositional logic which occur along $\Gamma$ is a finished set.
Finished Propositional Tableau
Let $T$ be a propositional tableau.
Then $T$ is finished if and only if every branch of $T$ is either finished or contradictory.