A differenza di LK tutte le regole sono invertibili.

Sequenti iniziali:

$$ p, \Gamma \Rightarrow \Delta, p $$

dove $p$ è una variabile enunciativa.

Nota: $\Gamma$ e $\Delta$ dei sequenti iniziali permette di avere ipotesi non necessarie o indebolimenti della conseguenza che in LK veniva aggiunti con $L\land_1$, $L\land_2$, $R\lor_1$ e $R\lor_2$.

Regole:

Nota: non ha senso avere $R\bot$ perché non c’è ragione di aggiungere $\bot$ a destra.

Nota: $L\bot$ può anche essere messo come sequente iniziale. Allo stesso modo, i sequenti iniziali potevano essere messi come regole a zero premesse.

Nota: come nel calcolo LK, il fatto che $A \Rightarrow B$ sia equivalente a $\Rightarrow A \to B$ non è un metaconcetto (come lo era nel caso della deduzione logica; in particolare, il Teorema di deduzione semantica diceva che se $A \Vdash B$ allora $\Vdash A \to B$), ma una regola vera e propria.