Use algorithm of reduction "\\forall xP(x)\\vee\\forall xQ(x)" to a prenex normal form.
1)"\\forall xQ(x)" is equivalent to"\\forall yQ(y)", so "\\forall xP(x)\\vee\\forall xQ(x)" is equivalent to "\\forall xP(x)\\vee\\forall yQ(y)"
So since "\\forall yQ(y)" does not contain the variable "x", we have "\\forall xP(x)\\vee\\forall yQ(y)" is equivalent to"\\forall x(P(x)\\vee\\forall yQ(y))"
So "\\forall xP(x)\\vee\\forall xQ(x)" is equivalent to "\\forall x(P(x)\\vee\\forall yQ(y))"
2)Consider "P(x)\\vee\\forall yQ(y)".
It is equivalent to "\\forall yQ(y)\\vee P(x)".
Since "P(x)" does not contain the variable "y", we have "\\forall yQ(y)\\vee P(x)" is equivalent to "\\forall y(Q(y)\\vee P(x))".
And since "Q(y)\\vee P(x)" is equivalent to "P(x)\\vee Q(y)", we have "\\forall y(Q(y)\\vee P(x))" is equivalent to "\\forall y(P(x)\\vee Q(y))"
So "P(x)\\vee\\forall yQ(y)" is equivalent to "\\forall y(P(x)\\vee Q(y))"
3)From step 2 we have that "\\forall x(P(x)\\vee\\forall yQ(y))" is equivalent to "\\forall x\\forall y(P(x)\\vee Q(y))"
4)So step 1 and step 3 gives us equivalence of "\\forall xP(x)\\vee\\forall xQ(x)" and "\\forall x\\forall y(P(x)\\vee Q(y))"
Comments
Leave a comment