cannot prove ∀x. x = x ⇒ ∀x. ∃y. x = y

[ddssff]

> :set -XFlexibleInstances -XOverloadedStrings
> :load Data.Logic
> let f = (let (x, y) = (vt "x" :: TTerm, vt "y" :: TTerm) in ((for_all "x" ((x .=. x))) .=>. (for_all "x" (exists "y" ((x .=. y))))) :: TFormula)
> putStrLn (prettyShow f)
∀x. (¬x = x) ∨ ∀x. ∃y. x = y
> runNormal (theorem f)
False

[ddssff]

We have these definitions:

theorem f = inconsistent <$> (.~.) f
inconsistent f = not $ satisfiable f

Here is the trace of the conversion to CNF of (.~.) f

> putStrLn (fst (runNormal (cnfTrace pPrint pPrint pPrint ((.~.) f)) :: (String, Set (Set TFormula))))
Original:
  ¬((∀x. (x = x) ⇒ ∀x. ∃y. (x = y)))
Simplified:
  ¬((∀x. (x = x) ⇒ ∀x. ∃y. (x = y)))
Negation Normal Form:
  ∀x. (x = x) ∧ ∃x. ∀y. (¬((x = y)))
Prenex Normal Form:
  ∀x. ∃x2. ∀y. ((x = x) ∧ ¬((x2 = y)))
Skolem Normal Form:
  (x = x) ∧ ¬((sKx[] = x))
Clause Normal Form:
  [[x = x]]
  [[sKx[] = x]]

[ddssff]

> prettyCNF (runNormal (clauseNormalForm ((.~.) f)) :: Set (Set TFormula))
x = x ∧ ¬(sKx[] = x)

So if this is not satisfiable the theorem is proved - but above we see the result of theorem is False. Is this the wrong CNF? Is this actually satisfiable?

[ddssff]

I think the problem is the way I am deciding whether clauses are satisfiable, specifically those involving skolem constants and functions.

[ddssff]

The issue is that while it is easy to prove such a thing for a finite domain, proving it in the general case requires more sophisticated machinery, i.e. Herbrand's theorem, David-Putnam, and onwards. I will know more shortly.