Sequente

Un sequente $\Gamma \Rightarrow \Delta$ è una coppia di multinsiemi (insiemi con ripetizioni) finiti di formule t.c.

$$ \vdash_{LK} \Gamma \Rightarrow \Delta \text{ sse } \vdash_{PC} \wedge \Gamma \to\vee \Delta $$

Dove $PC$ è il calcolo proposizionale.

Calcolo LK

Non è invertibile.

Sequenti iniziali:

• $A \Rightarrow A$
• $\bot \Rightarrow A$

Regole:

Nota: non invertibile.

Nota: non invertibile.

Nota: Il $\Delta$ deve essere per forza uguale, altrimenti la regola non vale!