During Resolution, Can a skolemization constant be replaced by a function?
For example:
∃X e(X)∧ g(X)
After replacing with skolemization constant
e(a)∧g(a)
I separate both the clauses:
e(a)
b(a)
Suppose I have one more clause ~b(X) ∨ ~e(f(X))
Here f(X) is the skolemization function which I got after Existential Elimination for that clause.
So When resolving
e(a)... (1)
b(a).... (2)
~b(X) ∨ ~e(f(X)).... (3)
Resolving (1) and (3) by Unification a/f(X)
~b(X)..(4)
This is my query. Can I replace a (which is a skolemization constant by f(X) which is a function) by unification.
Resolving (4) and (2) by Unification X/a
Null
Please let me know
No, you cannot unify $e(a)$ and $\neg e(f(X))$
Formally you can't, because there is no way to substitute anything for $X$ in $\neg e(f(X))$ so it ends up as $\neg e(a)$. That is: you can substitute terms for a variable, but you can never substitute terms for a constant.
But more importantly, logically you can't, because as the function $f$ indicates, the object that does not have property $e$ is dependent on the variable that you pick, and there is no guarantee that that function ever maps to $a$.
I am wondering though ... is there any way to avoid the function? For example, if the original statement you were working with is:
$$\forall x (b(x) \rightarrow \exists y \ \neg e(y))$$
Now, there are two ways to rewrite this to get it ready for resolution:
The 'obvious' way is:
$$\forall x (b(x) \rightarrow \exists y \ \neg e(y)) \Leftrightarrow$$
$$\forall x \exists y (b(x) \rightarrow \neg e(y)) \Leftrightarrow$$
$$\forall x \exists y (\neg b(x) \lor \neg e(y))$$
and that gives you clause $\{ \neg b(x), \neg e(f(x)) \}$
But you can also do:
$$\forall x (b(x) \rightarrow \exists y \ \neg e(y)) \Leftrightarrow$$
$$\exists x b(x) \rightarrow \exists y \ \neg e(y) \Leftrightarrow$$
$$\exists y (\exists x b(x) \rightarrow \neg e(y) \Leftrightarrow$$
$$\exists y \forall x(b(x) \rightarrow \neg e(y) \Leftrightarrow$$
$$\exists y \forall x(\neg b(x) \lor \neg e(y)$$
and that gives you clause $\{ \neg b(x), \neg e(y) \}$
and that one you can resolve with $e(a)$