Definition:Semantic Consequence/Predicate Logic

From ProofWiki
Jump to navigation Jump to search

Definition

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.


Notation

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

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


Also see


Sources