Definition:Semantic Consequence

From ProofWiki
Jump to navigation Jump to search

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

For semantic consequence, one also says that $\FF$ semantically entails $\phi$, in particular if $\FF$ comprises just one WFF.

The term formal consequence is also sometimes encountered.


Another common term used is logical consequence, but this is mainly used more generally in the context of logical implication.

Correspondingly, the term logical entailment can also be found.

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

  • Results about semantic consequences can be found here.


Sources