Definition:Semantic Consequence/Predicate Logic

Definition

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.

Notation

That $\mathbf A$ is a semantic consequence of $\FF$ is denoted as:

$\FF \models_{\mathrm{PL} } \mathbf A$

Also see

• Semantic Consequence preserved in Supersignature, showing that this notion is indeed independent of the choice of signature which is left implicit above

Sources

• 2009: Kenneth Kunen: The Foundations of Mathematics ... (previous) ... (next): $\text{II}.7$ First-Order Logic Semantics: Definition $\text{II.7.12}$