Prove (¬(∀(¬()))) ⊢ (∃ ()) by Natural Deduction

Question

I want to prove (¬(∀(¬()))) ⊢ (∃()) using only the basic rules of the Natural Deduction system for propositional logic and predicate logic.

I am not sure how to get rid of the negation before the universal quantifier.

How should I prove this?

Answer 1

If in doubt, try reductio ....

So after the initial premiss, assume $\neg\exists xPx$

Now what?

You'll have to make another assumption to get anywhere ....

So suppose $Pa$ (the obvious thing ...why??)

Then you can infer $\exists xPx$, contradiction!

So you can infer $\neg Pa$

And that gives you $\forall x\neg Px$

And now the end is in sight, because this contradicts the initial premiss ...

Join up the dots, and finish the proof.

Answer 2

Natural deduction rules are all about introduction and eliminations of connectives and quantifiers.   Hence the rules' names.   Writing a natural deduction proof basically consists of deciding what needs to be introduced or eliminated and when.   The rules themselves tell you how.

I am not sure how to get rid of the negation before the universal quantifier.

Okay, obviously, eliminating the negation will be done using the rule of negation elimination.   That was easy!

Well, the hard bit of this is arranging to have what the rule requires.   Although it is not that hard.

It requires two contradicting statements and we have only one premise in the base context.   An assumption must be raised!   So what do we assume to derive a contradiction of the premise?   Also what do we do with that contradiction?

Well, if the premise actually does entails the conclusion, assuming the contrary should derive a contradiction.   So let us assume that: $\neg\exists x~P(x)$ , and aim to derive this: $\forall x~\lnot P(x)$.   This also tells use what we're doing with that contradiction.   We will be using a proof by reduction to absurdity — discharging the assumption by introducing a negation, and then eliminating the double negation that results to derive the desired conclusion.

Okay, now, to get that contradiction you need to introduce a universal quantifier.   Continue thinking in this manner and the proof almost writes itself.

$$\def\fitch#1#2{\quad\begin{array}{|l}#1\\\hline#2\end{array}}\fitch{\neg\forall x~\neg P(x)\qquad~~~\textsf{Premise}}{\fitch{\neg\exists x~P(x)\qquad\textsf{Assumption}}{~\vdots\\\forall x~\neg P(x)\qquad\textsf{Universal Introduction}\\\bot\qquad\qquad\quad~\textsf{Negation Elimination}}\\\neg\neg\exists x~P(x)\qquad\quad\textsf{Negation Introduction}\\\exists x~P(x)\qquad\qquad\textsf{Double Negation Elimination}}$$