Problem 7 - Predicate Logic

1.

Let $P, Q_1, \dots, Q_n$ be formulas in the first-order logic. Describe the definition of the following: '$P$ is a logical consequence of $Q_1, Q_2, \dots, Q_n$'.

2.

Let $Q_1$ be $(\forall x)(F(x) \rightarrow G(x))$ and $Q_2$ be $F(a)$. Prove that formula $G(a)$ is a logical consequence of $Q_1$ and $Q_2$.

$P$ is a logical consequence of $Q_1, Q_2, \dots, Q_n$ means that for all the interpretations that satisfy all the wffs of the set $\{ Q_1, Q_2, \dots, Q_n \}$ (these interpretations are also called models of the set $\{ Q_1, Q_2, \dots, Q_n \}$), $P$ is satified as well. The fact that $P$ is true in every model of $\{ Q_1, Q_2, \dots, Q_n \}$ is know as logical consequence. More precisely, we say that $P$ is then a logical consequence of $\{ Q_1, Q_2, \dots, Q_n \}$ or that $P$ is logically implied by $\{ Q_1, Q_2, \dots, Q_n \}$. As a notation, $\{ Q_1, Q_2, \dots, Q_n \} \models A$.

We want to prove that $G(a)$ is a logical consequence of $Q_1$ and $Q_2$, i.e. that $(\forall x)(F(x) \rightarrow G(x)) \wedge F(a) \rightarrow G(a)$ is valid. We just need to refute its negation $\neg ((\forall x)(F(x) \rightarrow G(x)) \wedge F(a) \rightarrow G(a))$ which the same as $(\forall x)(F(x) \rightarrow G(x)) \wedge F(a) \wedge \neg G(a)$. By refuting its negation, we show that this negation is unsatisfiable, i.e. that no model assign it a true value, which implies that its negation is always true (our definition of logical consequence).

We use ground resolution. We write the above CNF in the standard set notation using ground clauses and check if the set of ground clauses is unsatisfiable. If we find the empty clause, then it means that $G(a)$ is a logical consequence of $Q_1$ and $Q_2$.