4.13.2.1 Existential Quantifier

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

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.