1
$\begingroup$

I think that I need to assume $¬∀x ¬P(x)$ and then do a proof by contradiction but I am not sure if that is correct or how to go about it.

$\endgroup$
7
$\begingroup$

We need contradiction in the proof (but it is not a poof by contradiction) :

1) $\lnot \exists x \ Px$ --- premise

2) $\quad\quad| \quad Px$ --- assumed [a]

3) $\quad\quad| \quad \exists x \ Px$ --- from 2) by $\exists$-intro

4) $\quad\quad| \quad\bot$ --- contradiction! from 1) and 3)

5) $\lnot Px$ --- from 2)-4) by $\lnot$-intro, discharging [a]

6) $\forall x \ \lnot Px$ --- from 5) by $\forall$-intro.

$\endgroup$
7
  • 1
    $\begingroup$ Would steps 2-4 be a subproof? If I make that a subproof and assume $[a]P(a)$ then step 5 - $¬Px$ is not a sentence. $\endgroup$ – Daryn Wilkinson Mar 7 '18 at 8:36
  • $\begingroup$ In step 5 I am not able to cite steps 2 and 4. I have to select the whole sub proof which doesn't work. $\endgroup$ – Daryn Wilkinson Mar 7 '18 at 8:53
  • $\begingroup$ @DarynWilkinson - you can freely modify the proof to adapt it to your needs... :-) $\endgroup$ – Mauro ALLEGRANZA Mar 7 '18 at 8:55
  • $\begingroup$ ∀-intro needs a sub proof cited. I can't just reference step 5. $\endgroup$ – Daryn Wilkinson Mar 7 '18 at 8:58
  • $\begingroup$ @DarynWilkinson The subproof is the introduction of an arbitrary element $c$, for which is proven must be $\neg Pc$. $\endgroup$ – Graham Kemp Mar 7 '18 at 9:00
2
$\begingroup$

Here is a proof for that in Fitch. Exact same idea as Mauro's proof but it does not have free variables anywhere which, it seems, your proof system does not want either:

enter image description here

$\endgroup$
0
$\begingroup$

We have for any proposition $Q$ not containing $x$ free, $(\exists x.P(x))\to Q\vdash \forall x.(P(x)\to Q)$. This is constructively true. Assume $P(c)$ for some arbitrary $c$, then use modus ponens on the assumption after introducing an existential, then generalize as $c$ is arbitrary. As a lambda term, it is basically currying. If you choose $Q\equiv\bot$, you get your statement using the fact that (even constructively) $\neg P\equiv P\to \bot$.

$\endgroup$

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.