# Given ∃x.¬p(x), use the Fitch System to prove ¬∀x.p(x).

What I am thinking was I need two formulas,
AX.p(X) => something
AX.p(X) => ~ something

I guess something maybe is the p(x) and the other is ~p(x) since we was given EX.~p(x)..But actually it can't work for me. And I guess maybe is EX.~p(x) and ~EX.~p(x)..But if I am doing that then the it will go to deadend..so I give up..;(

Wish someone can help me.

1: EX.p(X) 2: AX.(p(X) => something)
3: something EE1,2
But something cann't have the free variable from p..in this sample, then soemthing cannot including X..so if something is p(X) it cannot use EE, but if p(Y) then can use EE.

• Hint: first prove $\lnot p(x) \vdash \lnot \forall x ~ p(x)$. Note the $x$ represent different variables. – DanielV Apr 20 '17 at 3:01
• Thanks!! slime face ;) @DanielV – tang aqua Apr 21 '17 at 0:49

Given your EE rule, you need to prove $\forall x (\neg p(x) \rightarrow \neg \forall x \ P(x))$, which you do by a universal introduction on $\neg p(x) \rightarrow \forall x \ p(x)$, which on its turn you prove by a conditional Introduction on a subproof that assumes $\neg p(x)$ and derives $\neg \forall x \ p(x)$ .. and the latter you get by a proof by contradiction as you yourself surmised. So:

1. $\exists x \neg p(x)$ Premise

2. $\quad \neg p(x)$ Assumption

3. $\quad \quad \forall x \ p(x)$ Assumption

4. $\quad \quad p(x)$ $\forall$ Elim 3

5. $\quad \forall x \ p(x) \rightarrow p(x)$ $\rightarrow$ Intro 3-4

6. $\quad \quad \forall x \ p(x)$ Assumption

7. $\quad \quad \neg p(x)$ Reiteration 2

8. $\quad \forall x \ p(x) \rightarrow \neg p(x)$ $\rightarrow$ Intro 6-7

9. $\quad \neg \forall x \ p(x)$ $\neg$ Intro 5,8

10. $\neg p(x) \rightarrow \neg \forall x \ p(x)$ $\rightarrow$ Intro 2-9

11. $\forall x (\neg p(x) \rightarrow \neg \forall x \ p(x))$ $\forall$ Intro 10

12. $\neg \forall x \ p(x)$ $\exists$ Elim 1, 11

• How you know that much~!!?? I always stuck at some points and cannot go through...Probably I go into a wrong way.And Thanks again and again~!! – tang aqua Apr 20 '17 at 21:22
• @tangaqua After years of practice you really start to 'know' all the different patterns :) So yeah, that took me a long time, so don't feel bad if you're struggling. And I said some time before: you don't have the most user-friendly system either ... so it is not necessarily that you are bad with logic, but just that you have a hard time putting that into this particular proof system. – Bram28 Apr 20 '17 at 22:06
• By your inspiration, I just solve the other prove by myself~! Hahaha~! Helps me a lot~ – tang aqua Apr 21 '17 at 0:51
• @tangaqua Yay! Good for you!! :) – Bram28 Apr 21 '17 at 0:52
• @tangaqua You shouldn't try writing a formal proof until you can write an informal proof first. Formal proofs are just a language, not an idea. You have to have the idea (the reason why you think the theorem is true) before you can put the idea into a language. – DanielV Apr 21 '17 at 3:11

Here is my solution:

$1.~\exists X~\lnot p(X)\quad$ Premise

$2.~\quad \lnot p(c)\quad$ Existential Elimination:1, Witness Assumed: $[c]$

$3.~\qquad\forall X~p(X)\quad$ Assumption

$4.~\qquad p(c)\quad$ Universal Elimination:3

$5.~\quad \forall X~p(X) \implies p(c)\quad$ Implication Introduction 3-4

$6.~\qquad\forall X~p(X)\quad$ Assumption

$7.~\qquad\lnot p(c)\quad$ Reiteration:2

$8.~\quad\forall X p(X) \implies \lnot p(c)\quad$ Implication Introduction: 6-7

$9.~\quad\lnot \forall X~p(X)\quad$ Negation Introduction 5,8

$10.~\lnot \forall X~p(X)\quad$ Witness Eliminated 2-9