Can you show the validity of this by means of a derivation? $( \neg P \equiv \forall x Fx) \; \lor \; \exists x(Fx \equiv P)$

Question

$$( \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.

Answer 1

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$.