Definition:Semantic Consequence

From ProofWiki
Jump to navigation Jump to search

Definition

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

Let $\mathcal F$ be a collection of WFFs of $\mathcal L$.


Let $\map {\mathscr M} {\mathcal F}$ be the formal semantics obtained from $\mathscr M$ by retaining only the structures of $\mathscr M$ that are models of $\mathcal F$.

Let $\phi$ be a tautology for $\map {\mathscr M} {\mathcal F}$.


Then $\phi$ is called a semantic consequence of $\mathcal F$, and this is denoted as:

$\mathcal F \models_{\mathscr M} \phi$


That is to say, $\phi$ is a semantic consequence of $\mathcal F$ if and only if, for each $\mathscr M$-structure $\mathcal M$:

$\mathcal M \models_{\mathscr M} \mathcal F$ implies $\mathcal M \models_{\mathscr M} \phi$

where $\models_{\mathscr M}$ is the models relation.


Note in particular that for $\mathcal F = \O$, the notation agrees with the notation for a $\mathscr M$-tautology:

$\models_{\mathscr M} \phi$


The concept naturally generalises to sets of formulas $\mathcal G$ on the right hand side:

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

if and only if $\mathcal F \models_{\mathscr M} \phi$ for every $\phi \in \mathcal G$.


Let $\mathcal F$ be a collection of WFFs of propositional logic.


Then a WFF $\mathbf A$ is a semantic consequence of $\mathcal F$ iff:

$v \models_{\mathrm{BI}} \mathcal F$ implies $v \models_{\mathrm{BI}} \mathbf A$

where $\models_{\mathrm{BI}}$ is the models relation.

Let $\mathcal F$ be a collection of WFFs of predicate logic.


Then a WFF $\mathbf A$ is a semantic consequence of $\mathcal F$ if and only if:

$\mathcal A \models_{\mathrm{PL}} \mathcal F$ implies $\mathcal A \models_{\mathrm{PL}} \mathbf A$

for all structures $\mathcal A$, where $\models_{\mathrm{PL}}$ is the models relation.


Also known as

One also says that $\mathcal F$ semantically entails $\phi$, in particular if $\mathcal F$ 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