Semantic Consequence of Superset

From ProofWiki
Jump to navigation Jump to search


Let $\LL$ be a logical language.

Let $\mathscr M$ be a formal semantics for $\LL$.

Let $\FF$ be a set of logical formulas from $\LL$.

Let $\phi$ be an $\mathscr M$-semantic consequence of $\FF$.

Let $\FF'$ be another set of logical formulas.


$\FF \cup \FF' \models_{\mathscr M} \phi$

that is, $\phi$ is also a semantic consequence of $\FF \cup \FF'$.


Any model of $\FF \cup \FF'$ is a fortiori also a model of $\FF$.

By definition of semantic consequence all models of $\FF$ are models of $\phi$.

Therefore all models of $\FF \cup \FF'$ are also models of $\phi$.


$\FF \cup \FF' \models_{\mathscr M} \phi$

as desired.