Lambda the Ultimate

I have been working on an interpreter for a mini-subset of Prolog as I find it interesting how logic languages hold a central place in proof-assistants, theorem-provers and type-systems.

What I am interested in is a minimal and sound dialect of prolog to server as a starting point for further investigation. There are obviously several design points to discuss, but negation appears to be the most fundamental. Obviously as I am interested in soundness I want to operate in a Herbrand universe, which means unification with an occurs check.

The problem with negation seems to stem from the Prolog programming model. It appears to me that at some point "failure/unsat" and "falseness" (and "success/sat" and "truthfulness") have become confused with each other. This leads to negation as failure, the unsoundness of which is easily shown:

:- not (not (X = 0)), not (not (X = 1)).
yes.

Various solutions to this have been proposed, three-valued (Kleene) logic, four valued (Belnap) logic, negation as inconsistency, negation as refutation etc. All of those complicate the resolution process, but do solve the problem. Strong negation seems interesting because it is local and not fragile like some of these methods. I particularly liked the combination of a four-valued logic (because the bilattice structure is nice) and strong negation, and started to look at implementing it.

What interested me is that the logic values are seen as success values, so that a functor can be 'true' or 'false' without failing. In which case, why make them special 'values' in the language at all, surely they can be treated as normal atoms? Taking list membership as an example, we might want to define:

member(Key, cons(def(Key, _), _), true).
member(Key, nil, false).
member(Key, cons(_, Tail), X) :- member(Key, Tail, X).

We can even define 'not' as a predicate (fail if arg is true):

not(false).

not_member(Key, List) :- member(Key, List, X), not(X).

or a binary operator

not(true, false).
not(false, true).

not_member(Key, List, X) :- member(Key, List, Y), not(Y, X).

Without any of the logical unsoundness of negation as failure. There is obviously a parallel with dependent type systems (curry-howard), which I don't think have negation.

I have put the source code for my simple logic language "Clors" on GitHub https://github.com/keean/Clors. Its a still experimental, and is suffering form many changes and false starts, so needs a little tidying up (I have just removed meta-interpreters because they turn out to be unsound), and needs updating to use my parser combinator library.

So the question is, do logic languages need builtin negation?