Semantic Consequence is Transitive

From ProofWiki
Jump to navigation Jump to search

Theorem

Let $\mathcal L$ be a logical language.

Let $\mathscr M$ be a formal semantics for $\mathcal L$.

Let $\mathcal F, \mathcal G$ and $\mathcal H$ be sets of $\mathcal L$-formulas.

Suppose that:

$\mathcal F \models_{\mathscr M} \mathcal G$
$\mathcal G \models_{\mathscr M} \mathcal H$


Then $\mathcal F \models_{\mathscr M} \mathcal H$.


Proof

Let $\mathcal M$ be an $\mathscr M$-structure.

By assumption, if $\mathcal M$ is a model of $\mathcal F$, it is one of $\mathcal G$ as well.

But any model of $\mathcal G$ is also a model of $\mathcal H$.


In conclusion, any model of $\mathcal F$ is also a model of $\mathcal H$.

Hence the result, by definition of semantic consequence.

$\blacksquare$