Semantic Consequence preserved in Supersignature

From ProofWiki
Jump to navigation Jump to search

Theorem

Let $\mathcal L, \mathcal L'$ be signatures for the language of predicate logic.

Let $\mathcal L'$ be a supersignature of $\mathcal L$.

Let $\mathbf A$ be an $\mathcal L$-sentence.

Let $\Sigma$ be a set of $\mathcal L$-sentences.


Then the following are equivalent:

$\mathcal A \models_{\mathrm{PL}} \mathbf A$ for all $\mathcal L$-structure $\mathcal A$ for which $\mathcal A \models_{\mathrm{PL}} \Sigma$
$\mathcal A' \models_{\mathrm{PL}} \mathbf A$ for all $\mathcal L'$-structure $\mathcal A'$ for which $\mathcal A' \models_{\mathrm{PL}} \Sigma$

where $\models_{\mathrm{PL}}$ denotes the models relation.


That is to say, the notion of semantic consequence is preserved in passing to a supersignature.


Proof


Sources