DEF: sia $M=\langle W,R,I \rangle$. Una $M$-realizzazione è $\sigma:\Sigma \rightarrow W$, dove $\Sigma$ è l’insieme delle etichette.
DEF: una formula $E$ del linguaggio etichettato è vera in $M$ rispetto a $\sigma$ ($M$-realizzazione),
$\sigma \vDash E$, se:
$$ \sigma \vDash wRv \ \ \ \ \ \text{sse} \ \ \sigma(w)R\sigma(v) \\ \sigma \vDash w{:}A \ \ \ \ \ \ \text{sse} \ \vDash_{\sigma(w)}^M A \ \ \ \ \ \ $$
DEF: $\Gamma \Rightarrow \Delta$ è verificata da $\sigma$ (in notazione $\sigma \vDash \Gamma \Rightarrow \Delta$) sse se $\sigma \vDash E$ per ogni $E \in \Gamma$, allora $\sigma \vDash F$ per qualche $F \in \Delta$.
DEF: $\Gamma \Rightarrow \Delta$ è $\mathcal{L}$-valido (in notazione $C^{\mathcal{L}} \vDash \Gamma \Rightarrow \Delta$) sse per ogni modello $M$ basato sulla logica $\mathcal{L}$ e per ogni realizzazione $\sigma$ abbiamo che $\sigma \vDash \Gamma \Rightarrow \Delta$.
Se $\Gamma \Rightarrow \Delta$ è $\text{G3.}\mathcal{L}$ derivabile allora è $\mathcal{L}$-valido.
$$ \text{G3.}\mathcal{L} \vdash \Gamma \Rightarrow \Delta \ \ \ \ \ \ \ \ \ \ \text{implica} \ \ \ \ \ \ \ \ \ C^\mathcal{L} \vDash \Gamma \Rightarrow \Delta $$
Se $\mathcal{C}^L \vDash \Gamma \Rightarrow \Delta$ allora $\text{G3.L} \vdash \Gamma \Rightarrow \Delta$.
Se $\mathcal{C}^L \vDash A$ allora $\text{G3.L} \vdash \Rightarrow w{:}A$
Se $\text{G3.L} \not \vdash \Rightarrow w{:}A$ allora $\mathcal{C}^L \not \vDash A$