Semantic Consequence of Set minus Tautology

From ProofWiki
Jump to: navigation, search


Let $\mathcal L$ be a logical language.

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

Let $\mathcal F$ be a set of logical formulas from $\mathcal L$.

Let $\phi$ be an $\mathscr M$-semantic consequence of $\mathcal F$.

Let $\psi \in \mathcal F$ be a tautology.


$\mathcal F \setminus \left\{{\psi}\right\} \models_{\mathscr M} \phi$

that is, $\phi$ is also a semantic consequence of $\mathcal F \setminus \left\{{\psi}\right\}$.


Let $\mathcal M$ be a model of $\mathcal F \setminus \left\{{\psi}\right\}$.

Since $\psi$ is a tautology, it follows that:

$\mathcal M \models_{\mathscr M} \psi$


$\mathcal M \models \mathcal F$

which, by hypothesis, entails:

$\mathcal M \models \phi$

Since $\mathcal M$ was arbitrary, it follows by definition of semantic consequence that:

$\mathcal F \setminus \left\{{\psi}\right\} \models_{\mathscr M} \phi$