narain@randvax.UUCP (Sanjai Narain) (07/19/90)
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 Naraintorkel@sics.se (Torkel Franzen) (07/19/90)
In article <2635@randvax.UUCP> narain@randvax.UUCP (Sanjai Narain) writes: >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. c isn't new in the required sense if it occurs in S, which you presuppose in resolving with c=a->.