My professor asks us to either prove a logical consequence by resolution or disprove it by giving a suitable interpretation.
While doing one of the tasks, I encountered a problem with skolemization. Let's say I want to prove the following consequence by resolution
$$ \exists x Q(x) \models \exists y Q(y) $$
I introduce scolem constants a, b and try to infer the empty clause from this clausal form
$$ { [Q(a)], [\neg Q(b)] } $$
I cannot unify and therefore cannot prove by resolution. According to the task, I then have to disprove through example, but I feel like this logical consequence is always true.
A second side question: if I want to show $ \forall x \exists y P(x,y) \models \exists z P(a,z) $ where a is a constant, I can disprove by choosing $ I=\langle D, \phi \rangle $ with $ D=\emptyset $, right?
Best Answer
You application of Resolution is not correct.
In order to prove that $\Gamma \vDash \varphi$ you have to consider:
i.e. the set of formulas: $\Gamma \cup \{ \lnot \varphi \}$.
This means that, in order to prove: $∃xQ(x) \vDash ∃yQ(y)$ you have to apply the procedure to:
i.e. $∃xQ(x), \forall y \lnot Q(y)$.
Regarding the second question, the standard semantics for FOL needs interpretations with non-empty domains.
In addition, you set of formulas has an individual constant $a$; thus, you needs domains with at least one object $a^D \in D$ to be used as interpretation for the symbol $a$.
Added after comments.
The problem to be answered is: $∀x∃yP(x,y),∀x(∃yP(y,x) \to Q(x)) \vDash ∃xQ(x)$.
After initial transformations, we have:
Then, we have to apply Unification with a first substitution: $[w \leftarrow f(x), x \leftarrow g(w)]$ to the first two clauses to get: $Q(f(x))$ by Resolution.
A second substitution: $[z \leftarrow f(x)]$ applied to third clause will produce the empty clause.