I sottomodelli generati preservano la verità nel punto.

DEF: Chiusura riflessiva e transitiva di $R$

$$ wR^*v \ \text{sse} \ \exists n(wR^n v) $$

DEF: sottomodello generato

Sia $M= \langle W, R, I \rangle$

$M^w := \langle W^w, R^w, I^w \rangle$

$W^w := \{v: wR^*v \}$

$R^w := R \cap \{W^w \times W^w \}$

$I^w(p) := I(p) \cap W^w$

Lemma: $\forall M \forall w \in W^v$: $\vDash_w^M A$ sse $\vDash_w^{M^v} A$.

Ovvero un punto del modello si comporta come lo stesso punto nel sottomodello generato.

Dimostrazione

Sia $v$ il mondo che usiamo per fare il sottomodello generato e sia $w$ un generico mondo all’interno di quest’ultimo

Per induzione sulla struttura di $A$:

• $A \equiv \bot$

  $\not \vDash_w^M \bot \iff \not\vDash_w^{M^v} \bot$

• $A \equiv p$

  $\vDash_w^M p \ \ \ \ \iff \ \ \ \ \vDash_w^{M^v} p$

    $\\Updownarrow$                             $\\Updownarrow$
  

  $w \in I(p)$ $w\in I^v(p)$

               $\\Updownarrow$              $\\Updownarrow$
  
            $w \\in I(p) \\cap W^v$
  

• $A \equiv B \land C$

  IH: $\forall M\forall w \in W^v$ $\vDash_w^M B \iff \vDash_w^{M^v}B$ e $\forall M\forall w \in W^v$ $\vDash_w^M C \iff \vDash_w^{M^v}C$

  Dobbiamo dimostrare che $\vDash_w^M B \land C \iff \vDash_w^{M^v}B \land C$

  $\vDash_w^M B \land C$ vale se valgono $\vDash_w^M B$ e $\vDash_w^M C$.

  Per IH valgono sse rispettivamente $\vDash_w^{M^v} B$ e $\vDash_w^{M^v} C$ ovvero $\vDash_w^{M^v} B \land C$

• simile per $A \equiv B \lor C$ e $A \equiv B \rightarrow C$.

• $A \equiv \square B$

  Per IH vale $\forall M\forall w \in W^v$ $\vDash_w^M B \iff \vDash_w^{M^v} B$.

  $\vDash_w^M \square B \iff \vDash_w^{M^v} \square B$.

  • verso $\Rightarrow$: assumo $\vDash_w^M \square B$ e dimostro $\vDash_w^{M^v} \square B$.

    So $\vDash_w^M \square B$ ovvero $\forall u \in W . wRu \Rightarrow \ \vDash_u^M B$.

    Devo dimostrare che $\forall z \in W^v.wR^vz \Rightarrow \ \vDash_z^{M^v} B$.

    Fisso $z \in W^v$ fresca e assumo $wR^vz$.

    Dato che $R^v \sube R$, so che $wRz$.

    Da $\vDash_w^M \square B$ ottengo $\vDash_z^M B$ e per IH ottengo $\vDash_z^{M^v}B$.

  • verso $\Leftarrow$: assumo $\vDash_w^{M^v} \square B$ e dimostro $\vDash_w^M \square B$

    So $\vDash_w^{M^v} \square B$ ovvero $\forall u \in W^v . wR^vu \Rightarrow \ \vDash_u^{M^v} B$.

    Devo dimostrare che $\forall z \in W. wRz \Rightarrow \ \vDash_z^M B$.

    Fisso $z$ fresca e assumo $wRz$ e dimostro $\vDash_z^M B$.

    Siccome $wRz$ allora $z \in W^v$ quindi vale $wR^vz$.

    Da $\vDash_w^{M^v} \square B$ e $wR^vz$ vale $\vDash_z^{M^v}B$ e per IH vale $\vDash_z^MB$.

    Quindi $\vDash_z^M\square B$.