How to prove ‘∃xP(x)’ from ‘¬∀x(P(x)→Q(x))’











up vote
3
down vote

favorite












What would a formal Fitch proof for this look like?



I am given ¬∀x(P(x)→Q(x)), and need to derive ∃xP(x) from it.



I started with this, but I don't know if I am doing the right thing, and where to go from there:



enter image description here



EDIT: Did it (see answer)










share|improve this question
























  • So far no answers written out in English. Isn't the crux of the matter that if there were no $x$ such that $P(x)$, then $P(x)$ would be false for all $x$ and thus would imply absolutely anything?
    – Wildcard
    Nov 26 at 5:33















up vote
3
down vote

favorite












What would a formal Fitch proof for this look like?



I am given ¬∀x(P(x)→Q(x)), and need to derive ∃xP(x) from it.



I started with this, but I don't know if I am doing the right thing, and where to go from there:



enter image description here



EDIT: Did it (see answer)










share|improve this question
























  • So far no answers written out in English. Isn't the crux of the matter that if there were no $x$ such that $P(x)$, then $P(x)$ would be false for all $x$ and thus would imply absolutely anything?
    – Wildcard
    Nov 26 at 5:33













up vote
3
down vote

favorite









up vote
3
down vote

favorite











What would a formal Fitch proof for this look like?



I am given ¬∀x(P(x)→Q(x)), and need to derive ∃xP(x) from it.



I started with this, but I don't know if I am doing the right thing, and where to go from there:



enter image description here



EDIT: Did it (see answer)










share|improve this question















What would a formal Fitch proof for this look like?



I am given ¬∀x(P(x)→Q(x)), and need to derive ∃xP(x) from it.



I started with this, but I don't know if I am doing the right thing, and where to go from there:



enter image description here



EDIT: Did it (see answer)







logic proof fitch quantification






share|improve this question















share|improve this question













share|improve this question




share|improve this question








edited Nov 25 at 20:58

























asked Nov 25 at 19:56









35308

827




827












  • So far no answers written out in English. Isn't the crux of the matter that if there were no $x$ such that $P(x)$, then $P(x)$ would be false for all $x$ and thus would imply absolutely anything?
    – Wildcard
    Nov 26 at 5:33


















  • So far no answers written out in English. Isn't the crux of the matter that if there were no $x$ such that $P(x)$, then $P(x)$ would be false for all $x$ and thus would imply absolutely anything?
    – Wildcard
    Nov 26 at 5:33
















So far no answers written out in English. Isn't the crux of the matter that if there were no $x$ such that $P(x)$, then $P(x)$ would be false for all $x$ and thus would imply absolutely anything?
– Wildcard
Nov 26 at 5:33




So far no answers written out in English. Isn't the crux of the matter that if there were no $x$ such that $P(x)$, then $P(x)$ would be false for all $x$ and thus would imply absolutely anything?
– Wildcard
Nov 26 at 5:33










4 Answers
4






active

oldest

votes

















up vote
3
down vote



accepted










Resolved! I realised that I was going nowhere by assuming the opposite of what I was given as premise... I obviously had to assume the opposite of what I was trying to prove:



enter image description here






share|improve this answer





















  • Indeed. You have a correct solution. You can now accept your own answer to close this question.
    – Graham Kemp
    Nov 25 at 22:38


















up vote
2
down vote













1) ¬∀x(P(x) → Q(x)) --- premise



2) ¬∃xP(x) --- assumed [a]



3) P(x) --- assumed [b]



4) ∃xP(x) --- from 3) by -intro



5) --- contradiction : from 2) and 4)



6) Q(x) --- from 5) by -elim



7) P(x) → Q(x) --- from 3) and 6) by -intro, discharging [b]



8) ∀x(P(x) → Q(x)) --- from 7) by -intro



9) --- contradiction : from 1) and 8)




10) ∃xP(x) --- from 2) by Double Negation (or ¬-elim), discharging [a].







share|improve this answer






























    up vote
    2
    down vote













    The following proof is the same as Mauro ALLEGRANZA's but it uses Klement's Fitch-style proof checker. Descriptions of the rules are in forallx. Both are available online and listed below. They may help as supplementary material to what you are currently using.



    You may be required in your proof checker to represent contradictions as conjunctions of contradictory statements. This proof checker only requires noting the contradiction as "⊥" and listing the contradictory lines such as I did on lines 5 and 9.



    enter image description here





    References



    Kevin Klement's JavaScript/PHP Fitch-style natural deduction proof editor and checker http://proofs.openlogicproject.org/



    P. D. Magnus, Tim Button with additions by J. Robert Loftis remixed and revised by Aaron Thomas-Bolduc, Richard Zach, forallx Calgary Remix: An Introduction to Formal Logic, Winter 2018. http://forallx.openlogicproject.org/






    share|improve this answer





















    • I managed to do it, but my result is slightly different from yours. I tried yours out of curiosity, and it does not work in the Fitch program I have. I'm puzzled by the fact that your proof checker allowed you to export the temporary assumption 'a' outside of its subproof!
      – 35308
      Nov 25 at 21:07










    • @35308 You could look at that subproof (lines 3-6) as saying the same thing as the conditional statement on line 7 "Pa > Qa". Given the assumption Pa, I can derive Qa with what is available (namely line 2). The subproof just showed how that was done and the proof checker required that I show that before using line 7.
      – Frank Hubeny
      Nov 25 at 21:21












    • The issue is that you really should not be allowed to introduce a new free term 'a' without raising a new context to isolate it.
      – Graham Kemp
      Nov 25 at 22:48


















    up vote
    1
    down vote













    Pr. ~∀x(P(x)->Q(x))



    2.∃x~(P(x)->Q(x)) ~ Universal out Pr.



    3.~(P(a)->Q(a)) Existential out (x/a) 2



    4.P(a)&~Q(a) ~ conditional out 3



    5.P(a) Conjunction out 4



    6.∃xP(x) Existential In 5






    share|improve this answer





















      Your Answer








      StackExchange.ready(function() {
      var channelOptions = {
      tags: "".split(" "),
      id: "265"
      };
      initTagRenderer("".split(" "), "".split(" "), channelOptions);

      StackExchange.using("externalEditor", function() {
      // Have to fire editor after snippets, if snippets enabled
      if (StackExchange.settings.snippets.snippetsEnabled) {
      StackExchange.using("snippets", function() {
      createEditor();
      });
      }
      else {
      createEditor();
      }
      });

      function createEditor() {
      StackExchange.prepareEditor({
      heartbeatType: 'answer',
      convertImagesToLinks: false,
      noModals: true,
      showLowRepImageUploadWarning: true,
      reputationToPostImages: null,
      bindNavPrevention: true,
      postfix: "",
      imageUploader: {
      brandingHtml: "Powered by u003ca class="icon-imgur-white" href="https://imgur.com/"u003eu003c/au003e",
      contentPolicyHtml: "User contributions licensed under u003ca href="https://creativecommons.org/licenses/by-sa/3.0/"u003ecc by-sa 3.0 with attribution requiredu003c/au003e u003ca href="https://stackoverflow.com/legal/content-policy"u003e(content policy)u003c/au003e",
      allowUrls: true
      },
      noCode: true, onDemand: true,
      discardSelector: ".discard-answer"
      ,immediatelyShowMarkdownHelp:true
      });


      }
      });














      draft saved

      draft discarded


















      StackExchange.ready(
      function () {
      StackExchange.openid.initPostLogin('.new-post-login', 'https%3a%2f%2fphilosophy.stackexchange.com%2fquestions%2f57440%2fhow-to-prove-%25e2%2588%2583xpx-from-%25c2%25ac%25e2%2588%2580xpx%25e2%2586%2592qx%23new-answer', 'question_page');
      }
      );

      Post as a guest















      Required, but never shown

























      4 Answers
      4






      active

      oldest

      votes








      4 Answers
      4






      active

      oldest

      votes









      active

      oldest

      votes






      active

      oldest

      votes








      up vote
      3
      down vote



      accepted










      Resolved! I realised that I was going nowhere by assuming the opposite of what I was given as premise... I obviously had to assume the opposite of what I was trying to prove:



      enter image description here






      share|improve this answer





















      • Indeed. You have a correct solution. You can now accept your own answer to close this question.
        – Graham Kemp
        Nov 25 at 22:38















      up vote
      3
      down vote



      accepted










      Resolved! I realised that I was going nowhere by assuming the opposite of what I was given as premise... I obviously had to assume the opposite of what I was trying to prove:



      enter image description here






      share|improve this answer





















      • Indeed. You have a correct solution. You can now accept your own answer to close this question.
        – Graham Kemp
        Nov 25 at 22:38













      up vote
      3
      down vote



      accepted







      up vote
      3
      down vote



      accepted






      Resolved! I realised that I was going nowhere by assuming the opposite of what I was given as premise... I obviously had to assume the opposite of what I was trying to prove:



      enter image description here






      share|improve this answer












      Resolved! I realised that I was going nowhere by assuming the opposite of what I was given as premise... I obviously had to assume the opposite of what I was trying to prove:



      enter image description here







      share|improve this answer












      share|improve this answer



      share|improve this answer










      answered Nov 25 at 20:57









      35308

      827




      827












      • Indeed. You have a correct solution. You can now accept your own answer to close this question.
        – Graham Kemp
        Nov 25 at 22:38


















      • Indeed. You have a correct solution. You can now accept your own answer to close this question.
        – Graham Kemp
        Nov 25 at 22:38
















      Indeed. You have a correct solution. You can now accept your own answer to close this question.
      – Graham Kemp
      Nov 25 at 22:38




      Indeed. You have a correct solution. You can now accept your own answer to close this question.
      – Graham Kemp
      Nov 25 at 22:38










      up vote
      2
      down vote













      1) ¬∀x(P(x) → Q(x)) --- premise



      2) ¬∃xP(x) --- assumed [a]



      3) P(x) --- assumed [b]



      4) ∃xP(x) --- from 3) by -intro



      5) --- contradiction : from 2) and 4)



      6) Q(x) --- from 5) by -elim



      7) P(x) → Q(x) --- from 3) and 6) by -intro, discharging [b]



      8) ∀x(P(x) → Q(x)) --- from 7) by -intro



      9) --- contradiction : from 1) and 8)




      10) ∃xP(x) --- from 2) by Double Negation (or ¬-elim), discharging [a].







      share|improve this answer



























        up vote
        2
        down vote













        1) ¬∀x(P(x) → Q(x)) --- premise



        2) ¬∃xP(x) --- assumed [a]



        3) P(x) --- assumed [b]



        4) ∃xP(x) --- from 3) by -intro



        5) --- contradiction : from 2) and 4)



        6) Q(x) --- from 5) by -elim



        7) P(x) → Q(x) --- from 3) and 6) by -intro, discharging [b]



        8) ∀x(P(x) → Q(x)) --- from 7) by -intro



        9) --- contradiction : from 1) and 8)




        10) ∃xP(x) --- from 2) by Double Negation (or ¬-elim), discharging [a].







        share|improve this answer

























          up vote
          2
          down vote










          up vote
          2
          down vote









          1) ¬∀x(P(x) → Q(x)) --- premise



          2) ¬∃xP(x) --- assumed [a]



          3) P(x) --- assumed [b]



          4) ∃xP(x) --- from 3) by -intro



          5) --- contradiction : from 2) and 4)



          6) Q(x) --- from 5) by -elim



          7) P(x) → Q(x) --- from 3) and 6) by -intro, discharging [b]



          8) ∀x(P(x) → Q(x)) --- from 7) by -intro



          9) --- contradiction : from 1) and 8)




          10) ∃xP(x) --- from 2) by Double Negation (or ¬-elim), discharging [a].







          share|improve this answer














          1) ¬∀x(P(x) → Q(x)) --- premise



          2) ¬∃xP(x) --- assumed [a]



          3) P(x) --- assumed [b]



          4) ∃xP(x) --- from 3) by -intro



          5) --- contradiction : from 2) and 4)



          6) Q(x) --- from 5) by -elim



          7) P(x) → Q(x) --- from 3) and 6) by -intro, discharging [b]



          8) ∀x(P(x) → Q(x)) --- from 7) by -intro



          9) --- contradiction : from 1) and 8)




          10) ∃xP(x) --- from 2) by Double Negation (or ¬-elim), discharging [a].








          share|improve this answer














          share|improve this answer



          share|improve this answer








          edited Nov 25 at 20:21

























          answered Nov 25 at 20:07









          Mauro ALLEGRANZA

          27.3k21962




          27.3k21962






















              up vote
              2
              down vote













              The following proof is the same as Mauro ALLEGRANZA's but it uses Klement's Fitch-style proof checker. Descriptions of the rules are in forallx. Both are available online and listed below. They may help as supplementary material to what you are currently using.



              You may be required in your proof checker to represent contradictions as conjunctions of contradictory statements. This proof checker only requires noting the contradiction as "⊥" and listing the contradictory lines such as I did on lines 5 and 9.



              enter image description here





              References



              Kevin Klement's JavaScript/PHP Fitch-style natural deduction proof editor and checker http://proofs.openlogicproject.org/



              P. D. Magnus, Tim Button with additions by J. Robert Loftis remixed and revised by Aaron Thomas-Bolduc, Richard Zach, forallx Calgary Remix: An Introduction to Formal Logic, Winter 2018. http://forallx.openlogicproject.org/






              share|improve this answer





















              • I managed to do it, but my result is slightly different from yours. I tried yours out of curiosity, and it does not work in the Fitch program I have. I'm puzzled by the fact that your proof checker allowed you to export the temporary assumption 'a' outside of its subproof!
                – 35308
                Nov 25 at 21:07










              • @35308 You could look at that subproof (lines 3-6) as saying the same thing as the conditional statement on line 7 "Pa > Qa". Given the assumption Pa, I can derive Qa with what is available (namely line 2). The subproof just showed how that was done and the proof checker required that I show that before using line 7.
                – Frank Hubeny
                Nov 25 at 21:21












              • The issue is that you really should not be allowed to introduce a new free term 'a' without raising a new context to isolate it.
                – Graham Kemp
                Nov 25 at 22:48















              up vote
              2
              down vote













              The following proof is the same as Mauro ALLEGRANZA's but it uses Klement's Fitch-style proof checker. Descriptions of the rules are in forallx. Both are available online and listed below. They may help as supplementary material to what you are currently using.



              You may be required in your proof checker to represent contradictions as conjunctions of contradictory statements. This proof checker only requires noting the contradiction as "⊥" and listing the contradictory lines such as I did on lines 5 and 9.



              enter image description here





              References



              Kevin Klement's JavaScript/PHP Fitch-style natural deduction proof editor and checker http://proofs.openlogicproject.org/



              P. D. Magnus, Tim Button with additions by J. Robert Loftis remixed and revised by Aaron Thomas-Bolduc, Richard Zach, forallx Calgary Remix: An Introduction to Formal Logic, Winter 2018. http://forallx.openlogicproject.org/






              share|improve this answer





















              • I managed to do it, but my result is slightly different from yours. I tried yours out of curiosity, and it does not work in the Fitch program I have. I'm puzzled by the fact that your proof checker allowed you to export the temporary assumption 'a' outside of its subproof!
                – 35308
                Nov 25 at 21:07










              • @35308 You could look at that subproof (lines 3-6) as saying the same thing as the conditional statement on line 7 "Pa > Qa". Given the assumption Pa, I can derive Qa with what is available (namely line 2). The subproof just showed how that was done and the proof checker required that I show that before using line 7.
                – Frank Hubeny
                Nov 25 at 21:21












              • The issue is that you really should not be allowed to introduce a new free term 'a' without raising a new context to isolate it.
                – Graham Kemp
                Nov 25 at 22:48













              up vote
              2
              down vote










              up vote
              2
              down vote









              The following proof is the same as Mauro ALLEGRANZA's but it uses Klement's Fitch-style proof checker. Descriptions of the rules are in forallx. Both are available online and listed below. They may help as supplementary material to what you are currently using.



              You may be required in your proof checker to represent contradictions as conjunctions of contradictory statements. This proof checker only requires noting the contradiction as "⊥" and listing the contradictory lines such as I did on lines 5 and 9.



              enter image description here





              References



              Kevin Klement's JavaScript/PHP Fitch-style natural deduction proof editor and checker http://proofs.openlogicproject.org/



              P. D. Magnus, Tim Button with additions by J. Robert Loftis remixed and revised by Aaron Thomas-Bolduc, Richard Zach, forallx Calgary Remix: An Introduction to Formal Logic, Winter 2018. http://forallx.openlogicproject.org/






              share|improve this answer












              The following proof is the same as Mauro ALLEGRANZA's but it uses Klement's Fitch-style proof checker. Descriptions of the rules are in forallx. Both are available online and listed below. They may help as supplementary material to what you are currently using.



              You may be required in your proof checker to represent contradictions as conjunctions of contradictory statements. This proof checker only requires noting the contradiction as "⊥" and listing the contradictory lines such as I did on lines 5 and 9.



              enter image description here





              References



              Kevin Klement's JavaScript/PHP Fitch-style natural deduction proof editor and checker http://proofs.openlogicproject.org/



              P. D. Magnus, Tim Button with additions by J. Robert Loftis remixed and revised by Aaron Thomas-Bolduc, Richard Zach, forallx Calgary Remix: An Introduction to Formal Logic, Winter 2018. http://forallx.openlogicproject.org/







              share|improve this answer












              share|improve this answer



              share|improve this answer










              answered Nov 25 at 20:36









              Frank Hubeny

              6,48751344




              6,48751344












              • I managed to do it, but my result is slightly different from yours. I tried yours out of curiosity, and it does not work in the Fitch program I have. I'm puzzled by the fact that your proof checker allowed you to export the temporary assumption 'a' outside of its subproof!
                – 35308
                Nov 25 at 21:07










              • @35308 You could look at that subproof (lines 3-6) as saying the same thing as the conditional statement on line 7 "Pa > Qa". Given the assumption Pa, I can derive Qa with what is available (namely line 2). The subproof just showed how that was done and the proof checker required that I show that before using line 7.
                – Frank Hubeny
                Nov 25 at 21:21












              • The issue is that you really should not be allowed to introduce a new free term 'a' without raising a new context to isolate it.
                – Graham Kemp
                Nov 25 at 22:48


















              • I managed to do it, but my result is slightly different from yours. I tried yours out of curiosity, and it does not work in the Fitch program I have. I'm puzzled by the fact that your proof checker allowed you to export the temporary assumption 'a' outside of its subproof!
                – 35308
                Nov 25 at 21:07










              • @35308 You could look at that subproof (lines 3-6) as saying the same thing as the conditional statement on line 7 "Pa > Qa". Given the assumption Pa, I can derive Qa with what is available (namely line 2). The subproof just showed how that was done and the proof checker required that I show that before using line 7.
                – Frank Hubeny
                Nov 25 at 21:21












              • The issue is that you really should not be allowed to introduce a new free term 'a' without raising a new context to isolate it.
                – Graham Kemp
                Nov 25 at 22:48
















              I managed to do it, but my result is slightly different from yours. I tried yours out of curiosity, and it does not work in the Fitch program I have. I'm puzzled by the fact that your proof checker allowed you to export the temporary assumption 'a' outside of its subproof!
              – 35308
              Nov 25 at 21:07




              I managed to do it, but my result is slightly different from yours. I tried yours out of curiosity, and it does not work in the Fitch program I have. I'm puzzled by the fact that your proof checker allowed you to export the temporary assumption 'a' outside of its subproof!
              – 35308
              Nov 25 at 21:07












              @35308 You could look at that subproof (lines 3-6) as saying the same thing as the conditional statement on line 7 "Pa > Qa". Given the assumption Pa, I can derive Qa with what is available (namely line 2). The subproof just showed how that was done and the proof checker required that I show that before using line 7.
              – Frank Hubeny
              Nov 25 at 21:21






              @35308 You could look at that subproof (lines 3-6) as saying the same thing as the conditional statement on line 7 "Pa > Qa". Given the assumption Pa, I can derive Qa with what is available (namely line 2). The subproof just showed how that was done and the proof checker required that I show that before using line 7.
              – Frank Hubeny
              Nov 25 at 21:21














              The issue is that you really should not be allowed to introduce a new free term 'a' without raising a new context to isolate it.
              – Graham Kemp
              Nov 25 at 22:48




              The issue is that you really should not be allowed to introduce a new free term 'a' without raising a new context to isolate it.
              – Graham Kemp
              Nov 25 at 22:48










              up vote
              1
              down vote













              Pr. ~∀x(P(x)->Q(x))



              2.∃x~(P(x)->Q(x)) ~ Universal out Pr.



              3.~(P(a)->Q(a)) Existential out (x/a) 2



              4.P(a)&~Q(a) ~ conditional out 3



              5.P(a) Conjunction out 4



              6.∃xP(x) Existential In 5






              share|improve this answer

























                up vote
                1
                down vote













                Pr. ~∀x(P(x)->Q(x))



                2.∃x~(P(x)->Q(x)) ~ Universal out Pr.



                3.~(P(a)->Q(a)) Existential out (x/a) 2



                4.P(a)&~Q(a) ~ conditional out 3



                5.P(a) Conjunction out 4



                6.∃xP(x) Existential In 5






                share|improve this answer























                  up vote
                  1
                  down vote










                  up vote
                  1
                  down vote









                  Pr. ~∀x(P(x)->Q(x))



                  2.∃x~(P(x)->Q(x)) ~ Universal out Pr.



                  3.~(P(a)->Q(a)) Existential out (x/a) 2



                  4.P(a)&~Q(a) ~ conditional out 3



                  5.P(a) Conjunction out 4



                  6.∃xP(x) Existential In 5






                  share|improve this answer












                  Pr. ~∀x(P(x)->Q(x))



                  2.∃x~(P(x)->Q(x)) ~ Universal out Pr.



                  3.~(P(a)->Q(a)) Existential out (x/a) 2



                  4.P(a)&~Q(a) ~ conditional out 3



                  5.P(a) Conjunction out 4



                  6.∃xP(x) Existential In 5







                  share|improve this answer












                  share|improve this answer



                  share|improve this answer










                  answered Nov 25 at 23:02









                  Bertrand Wittgenstein's Ghost

                  2717




                  2717






























                      draft saved

                      draft discarded




















































                      Thanks for contributing an answer to Philosophy Stack Exchange!


                      • Please be sure to answer the question. Provide details and share your research!

                      But avoid



                      • Asking for help, clarification, or responding to other answers.

                      • Making statements based on opinion; back them up with references or personal experience.


                      To learn more, see our tips on writing great answers.





                      Some of your past answers have not been well-received, and you're in danger of being blocked from answering.


                      Please pay close attention to the following guidance:


                      • Please be sure to answer the question. Provide details and share your research!

                      But avoid



                      • Asking for help, clarification, or responding to other answers.

                      • Making statements based on opinion; back them up with references or personal experience.


                      To learn more, see our tips on writing great answers.




                      draft saved


                      draft discarded














                      StackExchange.ready(
                      function () {
                      StackExchange.openid.initPostLogin('.new-post-login', 'https%3a%2f%2fphilosophy.stackexchange.com%2fquestions%2f57440%2fhow-to-prove-%25e2%2588%2583xpx-from-%25c2%25ac%25e2%2588%2580xpx%25e2%2586%2592qx%23new-answer', 'question_page');
                      }
                      );

                      Post as a guest















                      Required, but never shown





















































                      Required, but never shown














                      Required, but never shown












                      Required, but never shown







                      Required, but never shown

































                      Required, but never shown














                      Required, but never shown












                      Required, but never shown







                      Required, but never shown







                      Popular posts from this blog

                      Wiesbaden

                      Marschland

                      Dieringhausen