A consequence relation $⊢$ that is taken to reflect the notion of logical consequence corresponding to proof. Generally, $⊢$ is taken to be a relation holding between a set of formulae $\text{Γ}$ in some language and a formula $\phi$ in that language (although variations exist, such as multiple-conclusion logic). In this case, where $\text{L}$ is a deductive system, that $\text{Γ}⊢\phi$ is interpreted as:

• • There exists a proof $\phi$ in a proof theory for $\text{L}$ with premisses $\text{Γ}$.

In different proof theories, this may be given subtly different interpretations. In, e.g., tableau methods, this is interpreted as:

• • Every branch closes in every tableau in which each $\psi \in \text{Γ}$ and $\neg \phi$ appear in the root.

In sequent calculi, this is equivalent to the assertion that the sequent $\text{Γ}\Rightarrow \left\{\phi \right\}$ is derivable.