🚀 go-pugleaf

What is the bug in the following reasoning?

Claim:  The following set of clauses, S, is inconsistent:

	{p(x)->x=a, x=a->p(x)} U EQ_0

where EQ_0 is a set of clauses containing ->z=z, z a variable, and for
each pair of distinct 0-ary function symbols c and d, the clause c=d->
(i.e. ~(c=d)).

Proof: We first show that S->exists(u).p(u) is valid.  We do this by
assuming ~exists(u).p(u), adding it to S, and showing the result to be
inconsistent.  We obtain:

	S, (u).~p(u)

In clausal form we obtain:

	S, p(u)->

Now, p(u)-> resolves with x=a->p(x) to yield x=a->. This resolves
with ->z=z in EQ_0 to yield ->. Contradiction.

We now show that S->~exists(u).p(u) is valid.  We add exists(u).p(u) to S.
Skolemizing, we obtain:

	S, ->p(c) where c is a new 0-ary constant.

->p(c) resolves with p(x)->x=a to yield ->c=a.  This resolves with c=a->
in EQ_0 to yield ->.  Contradiction.

Thus, S is inconsistent. QED.

Sanjai Narain