• Formule di $\mathcal{L}^\Phi$ Logica modale
• Un insieme $E$ enumerabile di etichette, denotate da $w$, $v,$ $u$, ... Nota: il concetto di etichetta è diverso da quello di mondo, un’etichetta è un oggetto sintattico mentre i mondi sono oggetti semantici.
• Il predicato binario $R$ (nota che qui è un simbolo sintattico, è diverso dalla relazione semantica tra mondi). Nota: stessa differenza delle etichette con la relazione tra mondi.

Descrizione formale di $\mathcal{L}^E$:

• Se $A \in \mathcal{L}^\phi$ allora $w{:}A \in \mathcal{L}^E$
• $wRv \in \mathcal{L}^E$ per ogni $w, v \in E$
• Nient’altro appartiene a $\mathcal{L}^E$

Il peso di $A \in \mathcal{L}^E$, $w(A)$ è:

$$ w(wRv) = 0 \\ w(w{:}A) = w(A) $$

dove $w(A)$ è definito come nel linguaggio modale, ovvero è il numero di connettivi.

Sequente

Un sequente è una coppia di multinsiemi $\Gamma \Rightarrow \Delta$ dove $\Gamma$, detto antecedente, è composto da atomi relazionali e formule etichettate e $\Delta$, detto succedente, è composto da formule etichettate (ma non atomi relazionali).

Derivazione

Una derivazione è definita come in Calcolo G3.

Calcolo di sequenti G3K

Sequenti iniziali: $w {:} p, \Gamma \Rightarrow \Delta, w {:} p$.

Le regole legate alla logica proposizionale sono uguali a quelle del Calcolo G3, ma vanno applicate alla stessa etichetta. Per esempio:

Inoltre abbiamo le seguenti regole: