i am trying to fix a conversion to basic prenex i've been doing for a while with no success. would appreciate understanding what i'm doing wrong:
$((∃x∀yp(x) \land (∃x∀y(s(y) \to q(y,x))) \lor ∃x∃yR(x,y))$
so first we'll rename the variables and change $s(y)) \to q(y,x) \equiv \lnot s(y) \lor q(y,x)$
so we get:
$\equiv ((∃a∀bp(a) \land (∃c∀d(\lnot s(d) \lor q(d,c))) \lor ∃x∃yR(x,y))$
now we'll take x,y out:
$\equiv \exists y \exists x(∃a∀bp(a) \land (∃c∀d(\lnot s(d) \lor q(d,c))) \lor R(x,y))$
now c,d:
$\equiv \exists y \exists x \exists c \forall d(∃a∀bp(a) \land (\lnot s(d) \lor q(d,c)) \lor R(x,y))$
we'll take a,b out:
$\equiv \exists y \exists x \exists c \exists a \forall d \forall b(p(a) \land (\lnot s(d) \lor q(d,c)) \lor R(x,y))$.
my main problem for here is continuing with $\lnot$, as i'm not sure how to proceed.
thank you very much for helping me and correcting me if i've done any mistake along the way!
$$((∃x∀y~p(x) \land (∃x∀y~(s(y) \to q(y,x))) ~\lor~ ∃x∃y~R(x,y))$$
Since there are no quantification within that implication, it can be treated as a single predicate, so we may temporarily substitute: $T(y,x)\equiv (s(y)\to q(y,x))$.
$$\big((\exists x\forall y~p(x))\land (\exists x\forall y~T(y,x))\big)\lor (\exists x\exists y~R(x,y))$$
Then (with assurance that $a,b,c,d$ do not occur freely within $p(x),T(y,x),$ or $R(x,y)$) alpha-substitution gives:
$$\big((\exists a\forall b~p(a))\land (\exists c\forall d~T(d,c))\big)\lor (\exists x\exists y~R(x,y))$$
And so distribution of quantifiers then gives:
$$\exists a\forall b~\exists c\forall d~\exists x\exists y~\Big(\big(p(a)\land T(d,c)\big)\lor R(x,y)\Big)$$
Note: the order of the three pairs of quantifiers is not critical, although the order within the first two is.
Then it is just a matter of releasing the temporary substitution: $T(d,c)\equiv (s(d)\to q(d,c))$
$$\exists a\forall b~\exists c\forall d~\exists x\exists y~\Big(\big(p(a)\land (s(d)\to q(d,c))\big)\lor R(x,y)\Big)$$
If you wish, you may distribute the existentials forward.
$$\exists x\exists y\exists a\exists c~\forall b\forall d~\Big(\big(p(a)\land (s(d)\to q(d,c))\big)\lor R(x,y)\Big)$$
Remark: That $\forall b$ seems a bit redundant...