I am going to write predicate which is true iff only and only when element X occurs before Y on list L
before(L, X, Y) :-
nth1(PX, L, X),
nth1(PY, L, Y),
PX < PY.
Above, you can see my solution. What do you think about it ?
When it comes to my specific question:
My predicate returns true when there is exists at least one pair that Y followed X. How to define predicate such that it is true for each pair ?
If the condition should hold for all pairs, the condition should hold for at least one pair, while its converse shouldn't be true for any pair.
I took the liberty of renaming your before/3 to beforeSome/3.
beforeSome(L, X, Y) :-
nth1(PX, L, X),
nth1(PY, L, Y),
PX < PY.
beforeAll(L, X, Y) :-
beforeSome(X,Y),
not(beforeSome(L, Y, X)).
Which yields the desired results:
?- beforeAll([1,2,3,1,4,5], 1, 4).
true.
?- beforeAll([1,2,3,1,4,5], 1, 2).
false.
Please note that your use of nth1/3 precludes it being used with uninstantiated variables. In other words, beforeAll([1,2,3,1,4,5], X, Y). is false.
A better implementation of beforeSome/3 would be something like
beforeSome([X|T], X, Y) :-
member(Y, T).
beforeSome([_|T], X, Y) :-
beforeSome(T, X, Y).
% no change needed, but repeated here for sake of completeness
beforeAll(L, X, Y) :-
beforeSome(X,Y),
not(beforeSome(L, Y, X)).