X ^ P is recognized as meaning “there exists an
X such that P is true”, and is treated as equivalent to
simply calling P. The use of the explicit existential
quantifier outside setof/3 and bagof/3 is superfluous.
Variables occurring in Generator will not be treated as free if they are explicitly bound within Generator by an existential quantifier. An existential quantification is written:
Y^Q
meaning “there exists a Y such that Q is true”, where Y is some Prolog variable. For example:
| ?- setof(X, Y^likes(X,Y), S).
would produce the single result
X = _400,
Y = _415,
S = [bill,dick,harry,jan,tom] ;
no
in contrast to the earlier example.
Furthermore, it is possible to existentially quantify a term, where all the variables in that term are taken to be existentially quantified in the goal. e.g.
A=term(X,Y), setof(Z, A^foo(X,Y,Z), L).
will treat X and Y as if they are existentially quantified.