| ?- [user].
compiling user for byte code...
formula_0(P, Q):- (P; Q), \+ P.
user compiled, 2 lines read - 768 bytes written, 37208 ms
yes
| ?- formula_0(P, Q).
uncaught exception: error(instantiation_error,formula_0/2)
All I basically want to do is to ask is the set of expressions {P or Q, ~P} satisfiable?
But the error message is not helping here...
PS. The answer should be "yes", this formula is satisfied when P = false and Q = true.
The reason you get an instantiation error is that too little is known about P and Q to say anything about them at the time they are used as goals. You are right that when you ask for example:
?- G.
then G = true is a solution that makes the query succeed. But so is for example G = (a=a) because a=a is also true. Since it is not possible to enumerate all goals G that succeed, you get an instantiation error. But notice for example that when you explicitly give a binding, you get the result you expect:
?- G = true, G.
G = true.
So, you should provide a set of values you are interested in:
?- maplist(boolean, [P,Q]), formula(P, Q).
and define for example:
boolean(true).
boolean(false).
to obtain concrete solutions. Or use constraints, which let you constrain the domain of variables before using them.
EDIT: Since there was some discussion about this, I go into more detail. The main question that arose is: Why does the query
?- Q.
not succeed with the sole solution
Q = true.
since obviously, true succeeds and is thus a valid solution? Answer: There are other possible answers as well, since true is not the only goal that succeeds. For example, the conjunction (true,true) succeeds as well. Suppose now that Q = true were the only solution to the above query, then it would be the case that:
?- Q, Q = (true, true).
fails (since dif(true, (true,true)) is itself true), but simply exchanging the goals like
?- Q = (true,true), Q.
succeeds because otherwise ?- true, true would also have to fail and that cannot be the case. This would violate commutativity of conjunction already for the most basic predicate (unification).
Note that while true and (true,true) both succeed when executed as goals, they are obviously different terms and cannot replace each other in general. Similarly, the term append([], [], []) is different from the term true, although both succeed when executed as goals. You therefore get an instantiation error, since too little is known about Q in a query like ?- Q. to give useful results.