Confusion in output of double negation as failure

Question

I am trying to learn prolog and i came across the following problem:

Given -

try(X):-not(not((member(X,[a,b,c])))),write(X). 

I would expect the query ?- try(X)., for the following query to be something like

X=a
a;
X=b
b;
X=c
c.

But in fact, the output is:

?- try(X).
_12010
true.

Why is that? Why the variable is not initiated to some value?

Answer 1

In addition to what @VictoriaRuiz says, notice a few other things:

?- \+ member(X, [a,b,c]).
false.

This is false because member(X, [a,b,c]) has solutions, but the variable binding is lost when you negate it. So that means

?- \+ \+ member(X, [a,b,c]).
true.

is the same as

?- \+ false.
true.

In other words, there's nowhere for X to materialize from. Your write(X) happens outside the scope of the variable binding for X, it's as though you did this:

?- \+ false, write(X).
_4082
true.

which is basically the same as

?- write(X).
_4014
true.

If you wanted to see evidence of backtracking in the negation, you might expect to see it with this query:

?- \+ \+ (member(X, [a,b,c]), write(X), nl).
a
true.

But because you obtained a true solution on the first try, the negation of that is false. Then the negation of that is true. So we see that it produced a solution inside the goal (member(X, [a,b,c]), write(X), nl), which is enough to know that the negation of that is false. Negating false again gives you true, but no variable bindings.

Answer 2

Prolog operates with a closed world assumption. You provide a knowledge base and only what is in it is true.

When you negate, Prolog doesn't know what values to check for. It can't add "a" as a part of this universe that is worth checking. And since it can't check for anything, it just returns nonsense.