Can you show the validity of this by means of a derivation? $( \neg P \equiv \forall x Fx) \; \lor \; \exists x(Fx \equiv P)$ $$( \neg P  \equiv  \forall x Fx) \; \lor \; \exists x(Fx \equiv P)$$
My friend and I have been trying to figure out how to show the validity by means of derivation, but we've gotten no where.
 A: By Natural Deduction.
1) $\forall x Fx$ --- assumed
2) $\lnot P$ --- assumed [a] from $\lnot P \lor P$
3) $\lnot P \to \forall x Fx$ --- from 1) by $\to$-intro
4) $\forall x Fx \to \lnot P$ --- from 1) and 2) by $\to$-intro
5) $\lnot P \leftrightarrow \forall x Fx$ --- from 3) and 4) by $\leftrightarrow$-intro

6)  $(\lnot P \leftrightarrow \forall x Fx) \lor ∃x(Fx \leftrightarrow P)$ --- from 5) by $\lor$-intro


7) $P$ --- assumed [b] from $\lnot P \lor P$
8) $Fx \to P$ --- by $\to$-intro
9) $Fx$ --- from 1) by $\forall$-elim
10) $P \to Fx$ --- from 9) by $\to$-intro
11) $Fx \leftrightarrow Px$ --- from 8) and 10) by $\leftrightarrow$-intro
12) $∃x(Fx \leftrightarrow P)$ --- from 11) by $\exists$-intro

13)  $(\lnot P \leftrightarrow \forall x Fx) \lor ∃x(Fx \leftrightarrow P)$ --- from 12) by $\lor$-intro




14)  $(\lnot P \leftrightarrow \forall x Fx) \lor ∃x(Fx \leftrightarrow P)$ --- from 2)-6) and 7)-13), by $\lor$-elim from $\lnot P \lor P$, discharging [a] and [b].



So far, we have derived the formula, using the following instance of LEM: $\lnot P \lor P$, under the assumption $\forall xFx$.
In a similar way, we can derive it under the assumption $\lnot \forall xFx$.
Thus, the result will follow from the instance of LEM: $\forall xFx \lor \lnot 
 \forall xFx$.
