Conseguenza semantica

Sia $C$ una classe di strutture, $A$ una formula e $X$ un insieme di formule: dirò che $A$ è conseguenza semantica di $X$ rispetto a $C$ (ovvero $X \vDash_C A$) sse

$$ \forall F \in C , \forall F\text{-modello } M, \forall w \in M \ (\text{se} \ \forall B \in X . \vDash_wB \ \text{allora} \ \vDash_w A) $$

Regole che preservano la validità

Modus Ponens

Necessitazione

Deduzione locale e globale

$$ B \vDash^l A \text{ sse } \vDash^l B \to A $$

$A \vDash^l B$ vuol dire $\forall w (\vDash_w A \text{ allora } \vDash_w B)$.

Teorema di deduzione globale (Non vale)

Dimostriamo che non vale il Teorema di deduzione globale:

$$ B \vDash^\gamma A \text{ sse } \vDash^\gamma B \to A \text{ \; \; \; \; \;NO!} $$

$A \vDash^\gamma B$ vuol dire $\forall w (\vDash_w A) \text{ allora } \forall w (\vDash_w B)$.

Se vale il Teorema di deduzione globale, vale anche $A \to \square A$. Dimostrazione:

Tuttavia $A \to \square A$ non è valida. Per esempio, consideriamo due mondi $w$, $v$ t.c. $wRv$ e nient’altro. Supponiamo che $\vDash_w A$ e $\not \vDash_v A$. $\not \vDash_w A \to \square A$, quindi $A \to \square A$ non è valida

Teorema di deduzione semantica per conseguenza locale