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!)
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:
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)$.