Logical consequence relation How to check whether formulas have logical consequence relation or not ?
Consider the problems:
$\forall xA\&\forall xB \ |= \forall x(A\&B) $
$\forall x P\&E \exists Q\&R \ |= P\&Q\&R$
$\forall x(P \implies Q \lor R) \ |= \forall xP \implies Q \lor R$
Where $|=$ logical consequence relation.
I can solve this problem without quantifiers using the implication instead of $|=$ and trying to find out counterexample, but with quantifiers I don't know what is the algorithm to solve this kind of problems ?
 A: As it turns out, there is no algorithm that can check for consequence that works for any problem like this.
However, there are several methods and algorithms that often do work.
Maybe the easiest thing to do is to try and generate a counterexample: think of a domain of objects, and provide interpretations for the predicates involved so that the left hand side is true, but the right hand side is not ... if you can find such a counterexample: great; you got your answer; the statement on the right is not a consequence of the one on the left.  If you can't find a counterexample ... try a little harder ... and if you still can't find one ... well, maybe it is time to see if you can derive the right side from the left side using rules of equivalence or inference. ... Are you provided with any such rules?
A very nice method that is able to figure out consequence as well as non-consequence is the tree or tableaux method ... but this will take a bit of explanation (if you're interested, just search for it online) .. and I am not sure that that is what your instructor is looking for anyway ...
