LARA

Semantic Argument Method

Suppose we want to prove the validity of a propositional logic formula $F$. Several methods to do this exists, one of which is called the semantic argument method.

We start the proof by assuming that a falsifying interpretation exists:

\begin{equation*} I \not\models F \end{equation*}

and try to show that this leads to a contradiction by applying semantic definitions of the logical connectives.

Thus, we obtain a set of proof rules:

\begin{equation*} \frac{I \models \neg F}{I \not\models F} \text{ and } \frac{I \not\models \neg F}{I \models F} \end{equation*}

\begin{equation*} \frac{I \models F \wedge G}{\parbox{2cm}{$I \models F$ \\ $I \models G$}} \text{ and } \frac{I \not\models F \wedge G}{I \not\models F \mid I \not\models G}} \end{equation*}

\begin{equation*} \frac{I \models F \vee G}{I \models F \mid I \models G}} \text{ and } \frac{I \not\models F \vee G}{\parbox{2cm}{$I \not\models F$ \\ $I \not\models G$}} \end{equation*}

\begin{equation*} \frac{I \models F \to G}{I \not\models F \mid I \models G}} \text{ and } \frac{I \not\models F \to G}{\parbox{2cm}{$I \models F$ \\ $I \not\models G$}} \end{equation*}

\begin{equation*} \frac{I \models F \leftrightarrow G}{I \models F \wedge G \mid I \not\models F \vee G}} \text{ and } \frac{I \not\models F \leftrightarrow G}{I \models F \wedge \neg G \mid I \models \neg F \wedge G}} \end{equation*}

\begin{equation*} \frac{\parbox{2cm}{$I \models F$ \\ $I \not\models F$}}{I \models \bot} \end{equation*}

Extension to First-order logic

The proof rules above apply in addition to the following proof rules for the quantifiers:

\begin{equation*} \frac{I \models \forall x. F}{I \vartriangleleft \{ x \mapsto v \} \models F} \end{equation*}

for any $v$ in the domain of the interpretation.

\begin{equation*} \frac{I \not\models \exists x. F}{I \vartriangleleft \{ x \mapsto v \} \not\models F} \end{equation*}

for any $v$ in the domain of the interpretation.

\begin{equation*} \frac{I \models \exists x. F}{I \vartriangleleft \{ x \mapsto v \} \models F} \end{equation*}

for a fresh $v$ in the domain of the interpretation.

\begin{equation*} \frac{I \not\models \forall x. F}{I \vartriangleleft \{ x \mapsto v \} \not\models F} \end{equation*}

for a fresh $v$ in the domain of the interpretation.