Modus Ponendo Ponens for Semantic Consequence in Predicate Logic

From ProofWiki
Jump to navigation Jump to search


Let $\mathrm{PL}$ be the formal semantics of structures for predicate logic.

Denote with $\models_{\mathrm{PL}}$ $\mathrm{PL}$-semantic consequence.

Let $\mathbf A$ and $\mathbf B$ be sentences.

Let $\FF$ be a set of sentences.

Suppose that:

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


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

establishing Modus Ponendo Ponens in $\mathrm{PL}$.


To establish $\FF \models_{\mathrm{PL}} \mathbf B$, we need to show that for all structures $\AA$:

$\AA \models_{\mathrm{PL}} \FF$ implies $\AA \models_{\mathrm{PL}} \mathbf B$

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

Then since $\AA \models_{\mathrm{PL}} \FF$, it follows that:

$\AA \models_{\mathrm{PL}} \mathbf A$
$\AA \models_{\mathrm{PL}} \mathbf A \implies \mathbf B$

By definition then, the latter means:

$\map {f^\to} { \map {\operatorname{val}_\AA} {\mathbf A}, \map {\operatorname{val}_\AA} {\mathbf B} } = T$

where $f^\to$ is the truth function of $\implies$ and $\map {\operatorname{val}_\AA} {\mathbf A}$ is the value of $\mathbf A$ in $\AA$.

Since $\map {\operatorname{val}_\AA} {\mathbf A} = T$, it then follows from the definition of $f^\to$ that necessarily:

$\map {\operatorname{val}_\AA} {\mathbf B} = T$

which is to say:

$\AA \models_{\mathrm{PL}} \mathbf B$

Since $\AA$ was arbitrary such that $\AA \models_{\mathrm{PL}} \FF$, it follows that:

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