Fitch proof exercise: showing $(\lnot \forall x \; P(x)) \leftrightarrow (\exists x \lnot P(x))$

first-order-logiclogicpredicate-logic

I have got a Problem with the following fitch proof excercise:

$\quad\;\; |$

$\triangleright \quad | \quad ?. \quad (\lnot \forall x \; P(x)) \leftrightarrow (\exists x \lnot P(x))$

This is how far I got: (Notice: I started from the bottom to the top!)

enter image description here

My problem is, that I can't find a way how to contradict $P(c)$. My first idea was, to proof $\forall x \; P(x)$ in the subproof in order to get a contradiction.

As you can see, this is only the first part of the proof. I know that I will have to use a Biconditional introduction in the end. I only need help for the first subproof.

Would be great if anyone could give me some hints.

Best Answer

It looks to me like you are trying to show that $\lnot P(c)$ as a lemma, where you have made no assumptions about $c$. If that were provable, then it would follow that $\forall x ( \lnot P(x))$. But that's too strong -- you only want to show that $\exists x (\lnot P(x))$. (Convince yourself that $\forall x ( \lnot P(x))$ is not necessarily implied by $\lnot (\forall x ( P(x))$, perhaps by thinking of an example set of $x$s and predicate $P$.)

So your dilemma is that you need to get the correct $c$ somehow, in order to prove that $\exists x (\lnot P(x))$; but you only know that $\lnot \forall x. P(x)$, and there's no way to get a $c$ directly from that statement.

In a situation where you get stuck it's good to try proof by contradiction. So, instead of proving $\exists x (\lnot P(x))$ (we have no idea how to get $c$ to make this true), try proving $$ \lnot \lnot (\exists x ( \lnot P(x))), $$ by assuming $\lnot \exists x ( \lnot P(x)))$ and getting a contradiction. The proof structure will look like this:

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

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

  2. ...[fill in here]...

  3. $\bot$

5. $\lnot \lnot \exists x (\lnot P(x))$

6. $\exists x (\lnot P(x))$ (double negation elimination from 5)

But you have to fill in the details for step 3. ... above. To do this, show as another lemma there that $\forall x (P(x))$. Proving this lemma will just rely on premise $2$, but may require some more nested reasoning$^1$. Then this lemma will get a contradiction with your original assumption $1$.

$^1$ To prove $\forall x ( P(x))$ we want to start from no assumptions and get $P(a)$. To do this, assume $\lnot P(a)$ and derive a contradiction, thus showing $\lnot \lnot P(a)$, then double negation to $P(a)$.