Why \+ member(X, [1,2,3]) fails for unbound X

Short answer: \+ is negation as failure, not logical negation. \+ Goal means "Goal is not provable right now," and it operates by actually trying to prove Goal. With X unbound, member(X, [1,2,3]) is trivially provable (it succeeds, binding X = 1), so \+ reports failure. You read it as "is there an X not in the list?" but Prolog computed "is it impossible to find any X in the list?" — to which the answer is correctly "no." The query is sound for what it actually asks; it's just not asking what you think.

The operational meaning of \+

\+ Goal is documented as: true if Goal cannot be proven (the mnemonic: + = "provable", \ = negation). Operationally it is essentially:

\+ Goal :- ( call(Goal) -> fail ; true ).

So Prolog runs Goal. If Goal succeeds even once, \+ Goal fails; if Goal finitely fails, \+ Goal succeeds. Trace it for the unbound case:

1. Try to prove member(X, [1,2,3]).
2. It succeeds immediately, unifying X = 1.
3. Because the inner goal succeeded, \+ fails.
4. The whole query fails — false.

A second crucial property: \+ never exports bindings. Even when the inner goal succeeds, the binding (X = 1) is undone — \+ is implemented via if-then-else / cut-fail, which discards bindings on the way out. So \+ can only ever answer yes/no; it can never produce a witness X. That is why you never get the "X that is not a member" you might have hoped for — \+ structurally cannot return one.

Why this is "not provable", not "false"

For ground goals, negation-as-failure and classical negation ¬ coincide (under the closed-world assumption: if a ground fact can't be proven, treat it as false). For example \+ member(5, [1,2,3]) correctly succeeds.

For nonground (variable-containing) goals they diverge sharply:

• Classical ¬∃X. member(X,[1,2,3]) is false (there clearly are members).
• \+ member(X,[1,2,3]) evaluates to false too — but for the operational reason that a proof was found, not because of any quantifier reasoning.

The mismatch is that \+ member(X, L) operationally asks "is member(X, L) unprovable for every X?" (a universally-quantified, all-or-nothing test), whereas users typically intend "find an X for which member(X, L) is false" (an existential search). Negation as failure cannot do the latter at all.

Floundering: the underlying soundness issue

Selecting a nonground negative literal is called floundering. SLDNF resolution (the formal basis of Prolog's negation) is only guaranteed sound when the negated goal is ground at the moment it is selected. Standard Prolog does not enforce this — it just runs \+ anyway and silently gives you the operational result, which is why the answer can look "wrong." It is the programmer's responsibility to ensure negated goals are sufficiently instantiated.

The fix: ground it first, then negate

Bind the variable with a positive goal before negating, so the negation runs on ground terms. The classic example — "elements of a list that are not 1":

?- member(X, [1,2,3]), \+ X = 1.   % correct: enumerate, then test
X = 2 ;
X = 3.

?- \+ X = 1, member(X, [1,2,3]).    % wrong: \+ runs on unbound X
false.                              % X=1 unifies, \+ fails immediately

In the first query, member/2 enumerates concrete values and each \+ X = 1 is a ground test — sound and gives the intended answers. In the second, \+ X = 1 flounders: X = 1 succeeds, so \+ fails before member ever runs.

For "is there an X not in the list," \+ is the wrong tool entirely; you need a generator with a known domain plus a membership test (e.g. member(X, Domain), \+ member(X, [1,2,3])), or constraints (dif/2), not bare negation as failure.

Takeaway: \+ tests provability of the goal as written, runs the goal to do so, and discards any bindings. Apply it only to ground (or sufficiently instantiated) goals; on a goal with unbound variables it answers a different, universally-quantified question and can flounder — which is exactly what makes \+ member(X, [1,2,3]) fail despite 1, 2, 3 being members.

Sources:

• https://www.swi-prolog.org/pldoc/man?section=control
• https://en.wikipedia.org/wiki/Negation_as_failure
• https://github.com/dtonhofer/prolog_notes/blob/master/other_notes/about_negation/floundering.md
• https://github.com/dtonhofer/prolog_notes/blob/master/other_notes/about_negation/README.md
• https://cs.union.edu/~striegnk/learn-prolog-now/html/node90.html
• https://cliplab.org/~vocal/public_info/seminar_notes/node52.html