I've recently been dealing with a question involving negating multiple stacked quantifiers, where the scopes of the quantifiers are potentially non-overlapping. I was wondering how someone would go about completing the negation for something like this:
$$\ ∃x¬∃y[ A(x) ∧ B(x) ∧ A(y) ∧ B(y) ∧ P(x, y) ] $$
Since only A(y), B(y) and P(x,y) are affected by the existential quantifier on y, would it be correct to rewrite it as something like this:
$$\ ∃x[ A(x) ∧ B(x) ∧ ¬∃y[ A(y) ∧ B(y) ∧ P(x, y) ] ] $$
My understanding here is that this should be acceptable with the Prenex Laws, but I want to check if I'm actually applying it correctly.
Addendum:
I suppose my question really boils down to which parts of the quantified statement will be negated. Specifically, should we write:
$$\ ∃x¬∃y[ A(x) ∧ B(x) ∧ A(y) ∧ B(y) ∧ P(x, y) ] $$
as:
$$\ ∃x∀y ¬ [ A(x) ∧ B(x) ∧ A(y) ∧ B(y) ∧ P(x, y) ] $$
or as:
$$\ ∃x∀y[ A(x) ∧ B(x) ∧ ¬ [A(y) ∧ B(y) ∧ P(x, y)] ] $$
given that $\ A(x) $ and $\ B(x) $ are not bound by the second quantifier involving y. And is this equivalent to the applying the Prenex laws in a situation where we move the negated existential quantifier into the statement. Specifically, by converting from the prenex normal form:
$$\ ∃x¬∃y[ A(x) ∧ B(x) ∧ A(y) ∧ B(y) ∧ P(x, y) ] $$
to the form:
$$\ ∃x[ A(x) ∧ B(x) ∧ ¬∃y[ A(y) ∧ B(y) ∧ P(x, y) ] ] $$
The first option in your addendum, but not the second, is correct.
For example, the negation of “there exists a marble such that the marble is green and the ball is red” is not “for each marble, the ball is red and the marble isn’t green”, but “for each marble, the marble isn’t green or the ball isn’t red”.
Thinking of $A(x) ∧ B(x) ∧ A(y) ∧ B(y) ∧ P(x, y)$ as a single compound predicate Q(x,y) makes it clear that the negation applies to the entirety of $A(x) ∧ B(x) ∧ A(y) ∧ B(y) ∧ P(x, y)$ instead of merely the portions containing the variable $y$ of the negated quantifier.
EDIT in response to the 4th comment under this post:
The two sentences that you gave, $$\exists x\lnot\exists y[ A(x) \land B(x) \land A(y) \land B(y) \land P(x,y)] \tag{1a}$$ and $$\exists x [ A(x) \land B(x) \land ¬∃y[ A(y) \land B(y) \land P(x,y) ] ],\tag{2a}$$ are not in prenex form.
They can be written in prenex form as $$\exists x\forall y[ \lnot [A(x) \land B(x)] \lor \lnot[ A(y) \land B(y) \land P(x,y)]]\tag{1b}$$ and $$\exists x \forall y\left[ [A(x) \land B(x)] \land \lnot[ A(y) \land B(y) \land P(x,y)] \right],\tag{2b}$$ respectively; from this, it can be seen that they are not equivalent.