Showing equivalence of two equalities

Question

I'm working through a book on logic and wanted to check one of my steps in a derivation I'm working out. Given the two quantifier negation equalities:

1. $\lnot\exists P(x) = \forall\lnot P(x)$

2. $\exists\lnot P(x) = \lnot\forall P(x)$

I'm trying to derive (2) from (1). I'm not asking for the solution if I have it wrong -- I think I've got it, but I want to find out if my last step is valid.

Negating both sides of (1):

$\lnot\lnot\exists P(x) = \lnot\forall\lnot P(x)$

Then removing the double negation, you get:

$\exists P(x) = \lnot\forall\lnot P(x)$

Now, it's not at all clear to me that algebraically, you can just slap a negation of both sides inside the quantifiers to get to (2), preserving correctness. But I notice that this equation has the same "shape" as (2). Intuitively, it seems to be saying the same thing, because you could define a predicate $R(x) = \lnot P(x)$ and obtain:

$\exists\lnot R(x) = \lnot\forall R(x)$

...but I don't like "intuitively". This step feels like a hand-wavy leap of faith -- is it valid? If so, is there a name for it?

Answer 1

Yes, it is valid. The $P$ refers to an arbitrary predicate. That means that it can be anything, including $\lnot P'$ for some predicate $P'$. That is exactly what you did.

Answer 2

The full statement is Second Order Logic

1. $\forall P\; \big(\neg \exists x \; P(x) \;\leftrightarrow\; \forall x\;\neg P(x)\big)$

Then we can use Universal Instantiation

1.1. $\neg \exists x\;\neg Q(x)\;\leftrightarrow\; \forall x\; \neg\neg Q(x)$

Double Negation Elimination

1.2. $\neg \exists x\;\neg Q(x)\;\leftrightarrow\; \forall x\; Q(x)$

Equivalence $\neg a\leftrightarrow b \iff a\leftrightarrow \neg b$

1.3. $\exists x\;\neg Q(x)\;\leftrightarrow\; \neg \forall x\; Q(x)$

And Universal Generalisation

2. $\forall P\;\big(\exists x\;\neg P(x)\;\leftrightarrow\; \neg \forall x\; P(x)\big)$