Analytical Tableaux

A Calculus ${\mathcal{T}}_0$ with two Inference Rules per connective:

Theorem / Derivability

$A$ is a ${\mathcal{T}}_0$ theorem iff there is a closed tableau with $A^F$ at the root (this also shows that $A$ is valid). A set of formulas $\Phi$ (assumptions) can be used to derive $A$ iff there is a closed tableau starting with $A^F$ and this set of assumptions. If we have the second case with only one branch, then this is called initial for $\Phi {⊢}_{{\mathcal{T}}_0}\mathrm{A}.$