>> It's beyond me why anyone considers this contentious.

Could you tone this sort of thing down please? Its needlessly confrontational tone only serves to add irrelevant noise to the converstation. Thank you in advance.

>> ?- L = [_,_,_], \+ (member(X, L), \+ (X < 2)).

Thank you for clarifying your intention with the original example. In that case, you could redefine </2 to avoid raising an error. Off the top of my head:

  1 < 2.
  2 < 3.
  3 < 4.

etc. Again it's a matter of implementation - in this case, of the predicate </2, rather than \+/2.

>> ?- forall(s(N), (N = 0; N = s(M), s(M))).

In your previous comment you said that "You can absolutlely prove theorems over infinite domains with [SMT2]", constrasting it with Prolog that if I understand correctly, you claim cannot. In my reply to your comment, I gave examples of theorems over infinite domains (integers and lists), that can be proven with Prolog.

You given an example of how one of those theories can "go infinite" if you make the right query. It can, but if you make a different query, it doesn't go infinite and Prolog proves it. So, Prolog can prove theories over infinite domains.

EDIT:

>> My only claim is that, it's much easier to understand why this happens if one thinks of Prolog as a search language over structural terms, rather than as a logic language where such a statement could be expected to be useful (if not necessarily decidable).

Your claim would be clearer if you explained what you mean by "logic language". Given what you've said so far I honestly have no idea what you mean by that.

In any case, what you say above sounds like the well-understood fact that Prolog programs have a declarative and a procedural reading and that one must be aware of the internal machinery of the interpreter to avoid infinite recursion.