Question #0970c

1 Answer
Jun 7, 2017

See explanation...

Explanation:

From:

EE x not P(x)

we have some x_1 such that not P(x_1)

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)

color(white)()
Rules used

The rules we have used are:

  • EExP(x) |-- P(x_1)" " for some x_1

  • AAxP(x) |-- P(x_1)" " for any x_1

  • (PvvQ)^^not P |-- Q

  • (not P vv Q) ^^ P |-- Q

  • (P->not Q) ^^ Q |-- not P