\begin{definition}[Definition:Semantic Consequence]
Let $\mathscr M$ be a formal semantics for a formal language $\LL$.
Let $\FF$ be a collection of WFFs of $\LL$.
Let $\map {\mathscr M} \FF$ be the formal semantics obtained from $\mathscr M$ by retaining only the structures of $\mathscr M$ that are models of $\FF$.
Let $\phi$ be a tautology for $\map {\mathscr M} \FF$.
Then $\phi$ is called a '''semantic consequence of $\FF$''', and this is denoted as:
:$\FF \models_{\mathscr M} \phi$
That is to say, $\phi$ is a '''semantic consequence of $\FF$''' {{iff}}, for each $\mathscr M$-structure $\MM$:
:$\MM \models_{\mathscr M} \FF$ implies $\MM \models_{\mathscr M} \phi$
where $\models_{\mathscr M}$ is the models relation.
Note in particular that for $\FF = \O$, the notation agrees with the notation for a $\mathscr M$-tautology:
:$\models_{\mathscr M} \phi$
The concept naturally generalises to sets of formulas $\GG$ on the {{RHS}}:
:$\FF \models_{\mathscr M} \GG$
{{iff}} $\FF \models_{\mathscr M} \phi$ for every $\phi \in \GG$.
{{transclude:Definition:Semantic Consequence/Boolean Interpretations
  |section = tc
  |title = Semantic Consequence for Boolean Interpretations
  |header = 3
  |increase = 1
  |link = true
  |foldable = true
}}
{{transclude:Definition:Semantic Consequence/Predicate Logic
  |section = tc
  |title = Semantic Consequence for Predicate Logic
  |header = 3
  |increase = 1
  |link = true
  |foldable = true
}}
\end{definition}