Open Branch (Tableaux)

logic tableaux

Definition

Open Branch

A branch in a semantic tableau is open when it is complete, meaning no further rules can be applied, and it contains no pair $t:A$ and $f:A$ for the same formula $A$.

An open branch certifies that the initial formula is satisfiable.

Extracting a Model

Model Construction

An open, complete branch provides a model for the initial formula. Construct the model by assigning truth values to atoms based on their signs:

• Assign $\top$ to every atom $p$ where $t:p$ appears on the branch
• Assign $\perp$ to every atom $p$ where $f:p$ appears on the branch

This interpretation satisfies all signed formulas on the branch, and therefore satisfies the initial formula.

Relation to Validity

Satisfiability Witness

The presence of an open branch means the negation of the initial formula is satisfiable. To check whether a formula $A$ is valid, start with $t:\neg A$ and verify that all branches close. If any branch remains open, $A$ is not valid.