Question #0970c
1 Answer
Jun 7, 2017
See explanation...
Explanation:
From:
EE x not P(x)
we have some
Then:
AAx(P(x)vvQ(x)) |-- P(x_1)vvQ(x_1)
Then:
(P(x_1)vvQ(x_1))^^not P(x_1) |-- Q(x_1)
We have
AAx(not Q(x)vvS(x)) |-- not Q(x_1) vv S(x_1)
Then:
(not Q(x_1) vv S(x_1)) ^^ Q(x_1) |-- S(x_1)
We have:
AAx(R(x)->not S(x)) |- R(x_1)->not S(x_1)
Then:
(R(x_1)->not S(x_1)) ^^ S(x_1)->not R(x_1)
Finally:
not R(x_1) |-- EEx not R(x)
Rules used
The rules we have used are:
-
EExP(x) |-- P(x_1)" " for somex_1 -
AAxP(x) |-- P(x_1)" " for anyx_1 -
(PvvQ)^^not P |-- Q -
(not P vv Q) ^^ P |-- Q -
(P->not Q) ^^ Q |-- not P