proof for relational predicate logic











up vote
3
down vote

favorite












I have been working on this problem for over an hour and I think I have simply missed something. I need some help. The rules I am allowed to use are the Basic Inference rules (MP, MT, HS, Simp, Conj, DS, Add, CD), the Replacement Rules (DN, Comm, Assoc, Dup, DeM, BE, Contrap, CE, Exp, Dist.), CP, IP, and EI, UI, EG, UG.



The problem is:




  1. ¬(∃x)(Axa ∧ ~Bxb)

  2. ¬(∃x)(Cxc ∧ Cbx)

  3. (∀x)(Bex → Cxf)


/∴ ¬(Aea ∧ Cfc)



Any help would be appreciated. Thanks.



Edit: Fixed the format of the question. The system is quantificational predicate logic. I've never called it anything else.










share|improve this question









New contributor




fantasticorangina is a new contributor to this site. Take care in asking for clarification, commenting, and answering.
Check out our Code of Conduct.
















  • 1




    This formula is unreadable. Please reformat it with ∀, ∃ for quantifiers, ∨, ∧, →, ¬ for connectives (you can copy symbols from here), and predicates as P(x,y,z). What > and // are I can not even guess. "Basic Inference rules" and "Replacement Rules" are specific to your book and not standard terminology, so best provide a reference and what type of system it is using (natural deduction, sequent calculus, something else?).
    – Conifold
    6 hours ago








  • 1




    I formatted the premises and conclusion to use Conifold's symbols. You may roll this back or continue editing if I got it wrong.
    – Frank Hubeny
    5 hours ago















up vote
3
down vote

favorite












I have been working on this problem for over an hour and I think I have simply missed something. I need some help. The rules I am allowed to use are the Basic Inference rules (MP, MT, HS, Simp, Conj, DS, Add, CD), the Replacement Rules (DN, Comm, Assoc, Dup, DeM, BE, Contrap, CE, Exp, Dist.), CP, IP, and EI, UI, EG, UG.



The problem is:




  1. ¬(∃x)(Axa ∧ ~Bxb)

  2. ¬(∃x)(Cxc ∧ Cbx)

  3. (∀x)(Bex → Cxf)


/∴ ¬(Aea ∧ Cfc)



Any help would be appreciated. Thanks.



Edit: Fixed the format of the question. The system is quantificational predicate logic. I've never called it anything else.










share|improve this question









New contributor




fantasticorangina is a new contributor to this site. Take care in asking for clarification, commenting, and answering.
Check out our Code of Conduct.
















  • 1




    This formula is unreadable. Please reformat it with ∀, ∃ for quantifiers, ∨, ∧, →, ¬ for connectives (you can copy symbols from here), and predicates as P(x,y,z). What > and // are I can not even guess. "Basic Inference rules" and "Replacement Rules" are specific to your book and not standard terminology, so best provide a reference and what type of system it is using (natural deduction, sequent calculus, something else?).
    – Conifold
    6 hours ago








  • 1




    I formatted the premises and conclusion to use Conifold's symbols. You may roll this back or continue editing if I got it wrong.
    – Frank Hubeny
    5 hours ago













up vote
3
down vote

favorite









up vote
3
down vote

favorite











I have been working on this problem for over an hour and I think I have simply missed something. I need some help. The rules I am allowed to use are the Basic Inference rules (MP, MT, HS, Simp, Conj, DS, Add, CD), the Replacement Rules (DN, Comm, Assoc, Dup, DeM, BE, Contrap, CE, Exp, Dist.), CP, IP, and EI, UI, EG, UG.



The problem is:




  1. ¬(∃x)(Axa ∧ ~Bxb)

  2. ¬(∃x)(Cxc ∧ Cbx)

  3. (∀x)(Bex → Cxf)


/∴ ¬(Aea ∧ Cfc)



Any help would be appreciated. Thanks.



Edit: Fixed the format of the question. The system is quantificational predicate logic. I've never called it anything else.










share|improve this question









New contributor




fantasticorangina is a new contributor to this site. Take care in asking for clarification, commenting, and answering.
Check out our Code of Conduct.











I have been working on this problem for over an hour and I think I have simply missed something. I need some help. The rules I am allowed to use are the Basic Inference rules (MP, MT, HS, Simp, Conj, DS, Add, CD), the Replacement Rules (DN, Comm, Assoc, Dup, DeM, BE, Contrap, CE, Exp, Dist.), CP, IP, and EI, UI, EG, UG.



The problem is:




  1. ¬(∃x)(Axa ∧ ~Bxb)

  2. ¬(∃x)(Cxc ∧ Cbx)

  3. (∀x)(Bex → Cxf)


/∴ ¬(Aea ∧ Cfc)



Any help would be appreciated. Thanks.



Edit: Fixed the format of the question. The system is quantificational predicate logic. I've never called it anything else.







logic symbolic-logic






share|improve this question









New contributor




fantasticorangina is a new contributor to this site. Take care in asking for clarification, commenting, and answering.
Check out our Code of Conduct.











share|improve this question









New contributor




fantasticorangina is a new contributor to this site. Take care in asking for clarification, commenting, and answering.
Check out our Code of Conduct.









share|improve this question




share|improve this question








edited 5 hours ago









Frank Hubeny

6,18141244




6,18141244






New contributor




fantasticorangina is a new contributor to this site. Take care in asking for clarification, commenting, and answering.
Check out our Code of Conduct.









asked 6 hours ago









fantasticorangina

162




162




New contributor




fantasticorangina is a new contributor to this site. Take care in asking for clarification, commenting, and answering.
Check out our Code of Conduct.





New contributor





fantasticorangina is a new contributor to this site. Take care in asking for clarification, commenting, and answering.
Check out our Code of Conduct.






fantasticorangina is a new contributor to this site. Take care in asking for clarification, commenting, and answering.
Check out our Code of Conduct.








  • 1




    This formula is unreadable. Please reformat it with ∀, ∃ for quantifiers, ∨, ∧, →, ¬ for connectives (you can copy symbols from here), and predicates as P(x,y,z). What > and // are I can not even guess. "Basic Inference rules" and "Replacement Rules" are specific to your book and not standard terminology, so best provide a reference and what type of system it is using (natural deduction, sequent calculus, something else?).
    – Conifold
    6 hours ago








  • 1




    I formatted the premises and conclusion to use Conifold's symbols. You may roll this back or continue editing if I got it wrong.
    – Frank Hubeny
    5 hours ago














  • 1




    This formula is unreadable. Please reformat it with ∀, ∃ for quantifiers, ∨, ∧, →, ¬ for connectives (you can copy symbols from here), and predicates as P(x,y,z). What > and // are I can not even guess. "Basic Inference rules" and "Replacement Rules" are specific to your book and not standard terminology, so best provide a reference and what type of system it is using (natural deduction, sequent calculus, something else?).
    – Conifold
    6 hours ago








  • 1




    I formatted the premises and conclusion to use Conifold's symbols. You may roll this back or continue editing if I got it wrong.
    – Frank Hubeny
    5 hours ago








1




1




This formula is unreadable. Please reformat it with ∀, ∃ for quantifiers, ∨, ∧, →, ¬ for connectives (you can copy symbols from here), and predicates as P(x,y,z). What > and // are I can not even guess. "Basic Inference rules" and "Replacement Rules" are specific to your book and not standard terminology, so best provide a reference and what type of system it is using (natural deduction, sequent calculus, something else?).
– Conifold
6 hours ago






This formula is unreadable. Please reformat it with ∀, ∃ for quantifiers, ∨, ∧, →, ¬ for connectives (you can copy symbols from here), and predicates as P(x,y,z). What > and // are I can not even guess. "Basic Inference rules" and "Replacement Rules" are specific to your book and not standard terminology, so best provide a reference and what type of system it is using (natural deduction, sequent calculus, something else?).
– Conifold
6 hours ago






1




1




I formatted the premises and conclusion to use Conifold's symbols. You may roll this back or continue editing if I got it wrong.
– Frank Hubeny
5 hours ago




I formatted the premises and conclusion to use Conifold's symbols. You may roll this back or continue editing if I got it wrong.
– Frank Hubeny
5 hours ago










2 Answers
2






active

oldest

votes

















up vote
1
down vote













It is useful to have a proof checker to aid learning how to use natural deduction. I have linked to one below in the references.



Using that proof checker and the rules described in forallx I was able to prove the result in 22 lines which included 3 lines for the premises and 1 line for the goal.



Although I don't see it listed I assume you have the change of quantifier replacement rule. If not a derivation is in forallx on pages 260-1. Use that to change the first two premises from "~(∃x)" to "(∀x)~".



Next eliminate the universal quantifier by assigning a different name to the variable "x" in each premise. You should chose these names wisely. Look at the goal to try to pick names that will help you reach the goal.



Then use De Morgan rules to transform the lines with a negation in front of the conjunction to a disjunction of negations.



After that preparatory work, I derived something like the following line: "¬Aea ∨ ¬¬Beb". I used disjunction elimination by considering both cases. I wanted to reach the following: "¬Aea ∨ ¬Cfc". Now that is not quite the desired result but with a use of the De Morgan rules I could convert that into the final goal: "¬(Aea ∧ Cfc)".





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




























    up vote
    1
    down vote













    Use an Indirect Proof.



    Begin by assuming (Aea ∧ Cfc), use the first premise to derive Beb, the third to derive Cbf, and the second to derive a contradiction.



    Some of your subproofs will likewise be Indirect Proofs; using existential generalisation to derive their contradictions.



    Assuming, that the thing you call IP operates as expected (derive a contradiction from an assumption, thereby deducing that the negation of the assumption holds).






    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
      });


      }
      });






      fantasticorangina is a new contributor. Be nice, and check out our Code of Conduct.










      draft saved

      draft discarded


















      StackExchange.ready(
      function () {
      StackExchange.openid.initPostLogin('.new-post-login', 'https%3a%2f%2fphilosophy.stackexchange.com%2fquestions%2f57639%2fproof-for-relational-predicate-logic%23new-answer', 'question_page');
      }
      );

      Post as a guest















      Required, but never shown

























      2 Answers
      2






      active

      oldest

      votes








      2 Answers
      2






      active

      oldest

      votes









      active

      oldest

      votes






      active

      oldest

      votes








      up vote
      1
      down vote













      It is useful to have a proof checker to aid learning how to use natural deduction. I have linked to one below in the references.



      Using that proof checker and the rules described in forallx I was able to prove the result in 22 lines which included 3 lines for the premises and 1 line for the goal.



      Although I don't see it listed I assume you have the change of quantifier replacement rule. If not a derivation is in forallx on pages 260-1. Use that to change the first two premises from "~(∃x)" to "(∀x)~".



      Next eliminate the universal quantifier by assigning a different name to the variable "x" in each premise. You should chose these names wisely. Look at the goal to try to pick names that will help you reach the goal.



      Then use De Morgan rules to transform the lines with a negation in front of the conjunction to a disjunction of negations.



      After that preparatory work, I derived something like the following line: "¬Aea ∨ ¬¬Beb". I used disjunction elimination by considering both cases. I wanted to reach the following: "¬Aea ∨ ¬Cfc". Now that is not quite the desired result but with a use of the De Morgan rules I could convert that into the final goal: "¬(Aea ∧ Cfc)".





      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

























        up vote
        1
        down vote













        It is useful to have a proof checker to aid learning how to use natural deduction. I have linked to one below in the references.



        Using that proof checker and the rules described in forallx I was able to prove the result in 22 lines which included 3 lines for the premises and 1 line for the goal.



        Although I don't see it listed I assume you have the change of quantifier replacement rule. If not a derivation is in forallx on pages 260-1. Use that to change the first two premises from "~(∃x)" to "(∀x)~".



        Next eliminate the universal quantifier by assigning a different name to the variable "x" in each premise. You should chose these names wisely. Look at the goal to try to pick names that will help you reach the goal.



        Then use De Morgan rules to transform the lines with a negation in front of the conjunction to a disjunction of negations.



        After that preparatory work, I derived something like the following line: "¬Aea ∨ ¬¬Beb". I used disjunction elimination by considering both cases. I wanted to reach the following: "¬Aea ∨ ¬Cfc". Now that is not quite the desired result but with a use of the De Morgan rules I could convert that into the final goal: "¬(Aea ∧ Cfc)".





        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























          up vote
          1
          down vote










          up vote
          1
          down vote









          It is useful to have a proof checker to aid learning how to use natural deduction. I have linked to one below in the references.



          Using that proof checker and the rules described in forallx I was able to prove the result in 22 lines which included 3 lines for the premises and 1 line for the goal.



          Although I don't see it listed I assume you have the change of quantifier replacement rule. If not a derivation is in forallx on pages 260-1. Use that to change the first two premises from "~(∃x)" to "(∀x)~".



          Next eliminate the universal quantifier by assigning a different name to the variable "x" in each premise. You should chose these names wisely. Look at the goal to try to pick names that will help you reach the goal.



          Then use De Morgan rules to transform the lines with a negation in front of the conjunction to a disjunction of negations.



          After that preparatory work, I derived something like the following line: "¬Aea ∨ ¬¬Beb". I used disjunction elimination by considering both cases. I wanted to reach the following: "¬Aea ∨ ¬Cfc". Now that is not quite the desired result but with a use of the De Morgan rules I could convert that into the final goal: "¬(Aea ∧ Cfc)".





          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












          It is useful to have a proof checker to aid learning how to use natural deduction. I have linked to one below in the references.



          Using that proof checker and the rules described in forallx I was able to prove the result in 22 lines which included 3 lines for the premises and 1 line for the goal.



          Although I don't see it listed I assume you have the change of quantifier replacement rule. If not a derivation is in forallx on pages 260-1. Use that to change the first two premises from "~(∃x)" to "(∀x)~".



          Next eliminate the universal quantifier by assigning a different name to the variable "x" in each premise. You should chose these names wisely. Look at the goal to try to pick names that will help you reach the goal.



          Then use De Morgan rules to transform the lines with a negation in front of the conjunction to a disjunction of negations.



          After that preparatory work, I derived something like the following line: "¬Aea ∨ ¬¬Beb". I used disjunction elimination by considering both cases. I wanted to reach the following: "¬Aea ∨ ¬Cfc". Now that is not quite the desired result but with a use of the De Morgan rules I could convert that into the final goal: "¬(Aea ∧ Cfc)".





          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 5 hours ago









          Frank Hubeny

          6,18141244




          6,18141244






















              up vote
              1
              down vote













              Use an Indirect Proof.



              Begin by assuming (Aea ∧ Cfc), use the first premise to derive Beb, the third to derive Cbf, and the second to derive a contradiction.



              Some of your subproofs will likewise be Indirect Proofs; using existential generalisation to derive their contradictions.



              Assuming, that the thing you call IP operates as expected (derive a contradiction from an assumption, thereby deducing that the negation of the assumption holds).






              share|improve this answer



























                up vote
                1
                down vote













                Use an Indirect Proof.



                Begin by assuming (Aea ∧ Cfc), use the first premise to derive Beb, the third to derive Cbf, and the second to derive a contradiction.



                Some of your subproofs will likewise be Indirect Proofs; using existential generalisation to derive their contradictions.



                Assuming, that the thing you call IP operates as expected (derive a contradiction from an assumption, thereby deducing that the negation of the assumption holds).






                share|improve this answer

























                  up vote
                  1
                  down vote










                  up vote
                  1
                  down vote









                  Use an Indirect Proof.



                  Begin by assuming (Aea ∧ Cfc), use the first premise to derive Beb, the third to derive Cbf, and the second to derive a contradiction.



                  Some of your subproofs will likewise be Indirect Proofs; using existential generalisation to derive their contradictions.



                  Assuming, that the thing you call IP operates as expected (derive a contradiction from an assumption, thereby deducing that the negation of the assumption holds).






                  share|improve this answer














                  Use an Indirect Proof.



                  Begin by assuming (Aea ∧ Cfc), use the first premise to derive Beb, the third to derive Cbf, and the second to derive a contradiction.



                  Some of your subproofs will likewise be Indirect Proofs; using existential generalisation to derive their contradictions.



                  Assuming, that the thing you call IP operates as expected (derive a contradiction from an assumption, thereby deducing that the negation of the assumption holds).







                  share|improve this answer














                  share|improve this answer



                  share|improve this answer








                  edited 3 hours ago

























                  answered 3 hours ago









                  Graham Kemp

                  83018




                  83018






















                      fantasticorangina is a new contributor. Be nice, and check out our Code of Conduct.










                      draft saved

                      draft discarded


















                      fantasticorangina is a new contributor. Be nice, and check out our Code of Conduct.













                      fantasticorangina is a new contributor. Be nice, and check out our Code of Conduct.












                      fantasticorangina is a new contributor. Be nice, and check out our Code of Conduct.
















                      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%2f57639%2fproof-for-relational-predicate-logic%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

                      Accessing regular linux commands in Huawei's Dopra Linux

                      Can't connect RFCOMM socket: Host is down

                      Kernel panic - not syncing: Fatal Exception in Interrupt