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!

  • $\begingroup$ 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. $\endgroup$ – Sentinel135 Feb 25 '17 at 5:53
  • $\begingroup$ Yeah. it's quite intuitive, what I want here is a systematic structural proof. $\endgroup$ – 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:

enter image description here


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

  • $\begingroup$ I'm sorry that I'm not familiar with your system's notation. Is step 3 equivalent to $\forall a \neg P(a)$? $\endgroup$ – Han Feb 25 '17 at 5:41
  • $\begingroup$ @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. $\endgroup$ – Bram28 Feb 25 '17 at 13:32
  • $\begingroup$ 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? $\endgroup$ – Han Feb 25 '17 at 16:43
  • $\begingroup$ @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. $\endgroup$ – Bram28 Feb 25 '17 at 18:25
  • $\begingroup$ 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. $\endgroup$ – 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$.

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

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.