Definizioni preliminari

• Insieme $\text{G3.L}$ per denotare il calcolo etichettato per la logica modale $L$.
• La lunghezza di una formula etichettata $E$, $l(E)$ è così definita:
  • se $E=wRv$ allora $l(E)=0$
  • se $E = w{:}A$ allora $l(E)=l(A)$
• La profondità di una $\text{G3.L}$ derivazione $D$, $h(D)$ è uguale al massimo dei numeri di nodi dei rami di $D$.
• $\text{G3.L} \vdash^{(n)} \Gamma \Rightarrow \Delta$ per dire che $\Gamma \Rightarrow \Delta$ è $\text{G3.L}$-derivabile (con profondità al più $n$).
• Una regola $R$ è ammissibile in $\text{G3.L}$ se la sua conclusione è $\text{G3.L}$-derivabile qualora lo siano le sue premesse.
• $R$ è derivabile se si può estendere una derivazione delle sue premesse in una derivazione della sua conclusione
• Una regola $R$ è ammissibile preservando la profondità (pp-ammissibile) se la sua conclusione è derivabile con profondità al più $n$ qualora tutte le sue premesse siano derivabili con profondità al più $n$.

LEMMA: Il sequente $w{:}A, \Gamma \Rightarrow \Delta, w{:}A$ con $A \ \text{fbf}$ arbitraria è $\text{G3.L}$-derivabile

DIM: per induzione sulla struttura di $w{:}A$

Sostituzione di etichette

La formula $E[v/u]$ è così definita:

$$ (w{:}A)[v/u] \equiv w[v/u]{:}A \equiv \begin{cases} v{:}A & w \equiv u \\ w{:}A & \text{altrimenti} \end{cases} $$

La sostituzione è applicabile a un multinsieme applicandola a ciascun elemento.

Lemma di sostituzione

La seguente regola di sostituzione:

è pp-ammissibile in G3.L.

Dimostrazione