Nested Quantifier Negation and Scoping

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.

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.

• Would that mean that the application of the Prenex laws to original statement is also incorrect? I'm also confused as to whether the grouping is necessarily correct here; my understanding was that when we negate a quantifier, we push the negation onto predicates involving the quantification. Specifically, wouldn't A(x) ∧ B(x) ∧ A(y) ∧ B(y) ∧ P(x,y) be Q(x) ∧ S(y) ∧ P(x,y), with Q(x) not being bound by ∃x? Jul 28 at 8:42
• I've also attempted to translate your example to a similar statement to the one I posited. Since I'm considered a nested ∃x¬∃y, I have ∃m¬∃b[G(m) ∧ R(b)] which should be logically equivalent to ∃m G(m) ∧ ¬∃b R(b) or "There exists a green marble and there does not exist a red ball. This in turn could be written as ∃m G(m) ∧ ∀b ¬R(b), which would in turn be equivalent to ∃m∀b[G(m) ∧ ¬R(b)]. This was how I understood the material here: link Jul 28 at 9:12
• @MathematicallyCorrectMongoose You're asking multiple questions (I suspect they are variations of one/two questions), each of which is ambiguous what (object) it is referring to. It would be easier to address your doubts if they are better-crystallised and your question(s) more streamlined and clearly-expressed. Thanks! Jul 28 at 11:08
• My apologies, I've tried clarifying them below, and I just want to say that I really appreciate your input on this! My core question was: I believe that statement ∃x¬∃y[ A(x) ∧ B(x) ∧ A(y) ∧ B(y) ∧ P(x,y) ] is the prenex normal form of an equivalent statement ∃x [ A(x) ∧ B(x) ∧ ¬∃y[ A(y) ∧ B(y) ∧ P(x,y) ] ]. Is this correct, and if not, where am I misapplying the PNF laws? I believe the addendums may have muddied the waters a bit by asking a variation of the question and I apologize again for that confusion. Jul 28 at 12:58
• @MathematicallyCorrectMongoose No worries—it can be hard to formulate the right question(s) while being tangled. I've expanded my answer; does it begin to clarify your doubts? Jul 28 at 13:56