# Relational Proofs with Fitch Systems

I need to prove:
$\forall x.p(x) \Rightarrow \neg \exists x.\neg p(x)$
I know I probably have to assume $\exists x.\neg p(x)$ to reach a contradiction. However, I am not quite sure about how to reach the contradiction.
The premise is that $\forall x.p(x)$, so maybe I had to prove $\exists x.\neg p(x) \Rightarrow \neg \forall x.p(x)$ in this case. However, to get $\neg \forall x.p(x)$ required assuming $\forall x.p(x)$ in advance, which is the same as the premise. Is it feasible? Whether such scenario would cause a endless loop?
I am not sure how could I get a contradiction for this case, any help would be appreciated, thanks!

• Shouldn't this follow from De Morgan's laws. In which you can prove it directly with a logical map. in either case, you are trying to prove that you can use contrapositive logic to prove things are true. – Sentinel135 Feb 25 '17 at 5:53
• Yeah. it's quite intuitive, what I want here is a systematic structural proof. – Han Feb 25 '17 at 6:25

Different systems define the Existential Elimination (or Existential Instantiation) differently, but here is a proof in the Fitch system I use:

EDIT

OK, so your system is indeed a good bit different from the one I use above. Here is a proof in your system:

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

2. $\quad \exists x \neg P(x)$ Assumption

3. $\quad \quad \neg P(x)$ Assumption

4. $\quad \quad \quad \forall x P(x)$ Reiteration 1

5. $\quad \quad \quad \neg P(x)$ Reiteration 3

6. $\quad \quad \forall x P(x) \rightarrow \neg P(x)$ $\rightarrow \: I$ 4-5

7. $\quad \quad \quad \forall x P(x)$ Assumption

8. $\quad \quad \quad P(x)$ $\forall \: E$ 7

9. $\quad \quad \forall x P(x) \rightarrow P(x)$ $\rightarrow \: I$ 7-8

10. $\quad \quad \neg \forall x P(x)$ $\neg \: I$ 6,9

11. $\quad \neg P(x) \rightarrow \neg \forall x P(x)$ $\rightarrow \: I$ 3-10

12. $\quad \forall x (\neg P(x) \rightarrow \neg \forall x P(x))$ $\forall \: I$ 11

13. $\quad \neg \forall x P(x)$ $\exists \: E$ 2,12

14. $\exists x \neg P(x) \rightarrow \neg \forall x P(x)$ $\rightarrow \: I$ 2-13

15. $\quad \exists x \neg P(x)$ Assumption

16. $\forall x P(x)$ Reiteration 1

17. $\exists x \neg P(x) \rightarrow \forall x P(x)$ $\rightarrow \: I$ 15-16

18. $\neg \exists x \neg P(x)$ $\neg \: I$ 14,17

• I'm sorry that I'm not familiar with your system's notation. Is step 3 equivalent to $\forall a \neg P(a)$? – Han Feb 25 '17 at 5:41
• @Han Yeah, I was afraid your system might be different ... How is your Existential Elimination rule defined? ... And no, you don't want to use $\forall a \neg P(a)$, since $a$ is a constant, and you can only quantify over variables. – Bram28 Feb 25 '17 at 13:32
• EE is such, $\exists x.p(X)$ $\forall x.(p(X) \Rightarrow q(X))$, then we could obtain $q(X)$. So the figure you show is a workflow without details, right? – Han Feb 25 '17 at 16:43
• @Han. I really doubt that that is how EE is defined ... i have seen many different particular implemenations of EE, but I have never seen anyone that requires you to have a $\forall$. indeed, how would you infer $\exists x (P(x) \land Q(x))$ from $\exists x (Q(x) \land P(x))$ using this as the EE rule? Also, no, the figure I show is not just a workflow ... It does have all the details for the particular proof system I work with. – Bram28 Feb 25 '17 at 18:25
• Sorry for the late response. This EE is defined under logic.stanford.edu/intrologic/notes/chapter_08.html. This definition seemed like Or Elimination. The question you proposed is solvable in this case, s.t. assume $Q(x)\wedge P(x)$ then using EI to obtain $Q(x)\wedge P(x) \Rightarrow \exists x.(P(x)\wedge Q(x))$. Then using UI to introduce the $\forall$ symbol. Last step is a direct application of EE. – Han Feb 26 '17 at 2:38

I may be misunderstanding the question, but it seems like the contradiction follows almost directly from supposing the negation of the conclusion. By negating the conclusion, we have $\exists x$ such that $\neg p(x)$, call it $x_0$. So, by using that particular $x_0$ we have a contradiction to the premise that $p(x)$ for any $x$.

• Yeah, this problem is really easy because it's intuitive. However, here I need a systematic structure. – Han Feb 25 '17 at 5:13