Definition:Semantic Consequence
This page is about semantic consequence in the context of formal semantics. For other uses, see consequence.
Definition
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$ if and only if, 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 right hand side:
- $\FF \models_{\mathscr M} \GG$
if and only if $\FF \models_{\mathscr M} \phi$ for every $\phi \in \GG$.
Let $\FF$ be a collection of WFFs of propositional logic.
Then a WFF $\mathbf A$ is a semantic consequence of $\FF$ if and only if:
- $v \models_{\mathrm{BI}} \FF$ implies $v \models_{\mathrm{BI}} \mathbf A$
where $\models_{\mathrm{BI}}$ is the models relation.
Let $\FF$ be a collection of WFFs of predicate logic.
Then a WFF $\mathbf A$ is a semantic consequence of $\FF$ if and only if:
- $\AA \models_{\mathrm{PL} } \FF$ implies $\AA \models_{\mathrm{PL} } \mathbf A$
for all structures $\AA$, where $\models_{\mathrm{PL} }$ is the models relation.
Also known as
One also says that $\FF$ semantically entails $\phi$, in particular if $\FF$ comprises just one WFF.
Another common term used is logical consequence (and, correspondingly, logical entailment).
However, the adjective "logical" is heavily used and prone to ambiguity, so these terms should not be used on $\mathsf{Pr} \infty \mathsf{fWiki}$.
Also see
Sources
- 1996: H. Jerome Keisler and Joel Robbin: Mathematical Logic and Computability ... (previous) ... (next): $\S 1.7$: Tableaus
- 1998: David Nelson: The Penguin Dictionary of Mathematics (2nd ed.) ... (previous) ... (next): consequence: 2. (formal consequence)