Results 1 to 11 of 11

Math Help - Abstract reasoning/natural deduction with Fitch

  1. #1
    Junior Member
    Joined
    Jul 2011
    Posts
    53

    Abstract reasoning/natural deduction with Fitch

    I'm practicing natural deduction, using a system similar to Fitch. I'm wondering if what I'm doing is legal, especially the => intro @ 5.

    I've to prove ((P \implies Q) \implies P) \implies ((P \implies Q) \implies Q) is a tautology. I've set my reasoning up as follows:

    Code:
    1, H:                              (P => Q) => P
    2, H:                                 P
    3, => elim on 1 & 2                      P => Q
    4, => elim on 2 & 3                      Q
    5, => intro on 3 & 4                  (P => Q) => Q
    6, => intro on 1 & 5               ((P => Q) => P) => ((P => Q) => Q)
    Is this approach correct? I think not, because I'm not actually using the hypothesis (2) in my conclusion (5).

    Am I allowed to do this?
    Code:
    1, H:        P
    2, H:             Q
    3, ^I 1,2              P ^ Q
    4, =>I 3,2       (P ^ Q) => Q
         || ||
    Last edited by Lepzed; October 16th 2011 at 03:48 AM.
    Follow Math Help Forum on Facebook and Google+

  2. #2
    Junior Member
    Joined
    Jul 2011
    Posts
    53

    Re: Abstract reasoning/natural deduction with Fitch

    I've a new way to solve the first one:
    Code:
    1, H:       (P => Q) => P
    2, H:           P => Q
    3, =>E 1,2:         P
    4, =>E 2,3:         Q
    5, =>I 2,4:     (P => Q) => Q
    6, =>I 1,5: ((P => Q) => P) => ((P => Q) => Q)
    I think this is correct, any advice?

    Regarding the second part, the question was to prove P => ((P ^ Q) => Q) is a tautology, now I've set up my reasoning as follows
    Code:
    1, H:       P
    2, H:           Q
    3, ^I 1,2:          P ^ Q
    4, ^E 3:            Q
    5, =>I 3,4:    (P ^ Q) => Q
    6, =>I 1,5: P => ((P ^ Q) => Q
    Furthermore I'm trying to prove (P => Q) => ((P ^ R) => (Q ^ R)) and having some trouble introducing the R, my current train of thought leaves me with an assumption i can't get rid of.
    Code:
    1, H:       P => Q
    2, H:           P
    3, =>E 1,2:         Q
    4, H:                    R
    5, ^I 2,4:                    P ^ R
    6, ^I 3,4:                    Q ^ R
    7, =>I 5,6:              (P ^ R) => (Q ^ R)
    8, =>I 1,7: (P => Q) => ((P ^ R) => (Q ^ R))
    As you see, I'm left out with an assumption too many. I guess I'm introducing the R (4) incorrect, any pointers?
    Last edited by Lepzed; October 16th 2011 at 05:12 AM.
    Follow Math Help Forum on Facebook and Google+

  3. #3
    MHF Contributor
    Joined
    Oct 2009
    Posts
    5,513
    Thanks
    769

    Re: Abstract reasoning/natural deduction with Fitch

    Quote Originally Posted by Lepzed View Post
    Code:
    1, H:                              (P => Q) => P
    2, H:                                 P
    3, => elim on 1 & 2                      P => Q
    4, => elim on 2 & 3                      Q
    5, => intro on 3 & 4                  (P => Q) => Q
    6, => intro on 1 & 5               ((P => Q) => P) => ((P => Q) => Q)
    Step 3 is wrong because MP gives you the conclusion of an implication, not the premise. Step 5 is also wrong because =>I can only close an assumption and never a formula that is a conclusion of a subderivation, like formula 3.

    Quote Originally Posted by Lepzed View Post
    Code:
    1, H:        P
    2, H:             Q
    3, ^I 1,2              P ^ Q
    4, =>I 3,2       (P ^ Q) => Q
         || ||
    =>I cannot close P ^ Q since it's not an assumption.

    Quote Originally Posted by Lepzed View Post
    I've a new way to solve the first one:
    Code:
    1, H:       (P => Q) => P
    2, H:           P => Q
    3, =>E 1,2:         P
    4, =>E 2,3:         Q
    5, =>I 2,4:     (P => Q) => Q
    6, =>I 1,5: ((P => Q) => P) => ((P => Q) => Q)
    This is correct.

    Quote Originally Posted by Lepzed View Post
    Regarding the second part, the question was to prove P => ((P ^ Q) => Q) is a tautology, now I've set up my reasoning as follows
    Code:
    1, H:       P
    2, H:           Q
    3, ^I 1,2:          P ^ Q
    4, ^E 3:            Q
    5, =>I 3,4:    (P ^ Q) => Q
    6, =>I 1,5: P => ((P ^ Q) => Q
    Cannot close P ^ Q: not an assumption. You need to assume P ^ Q (along with a vacuous assumption P) and deduce Q by ^E.

    Quote Originally Posted by Lepzed View Post
    Furthermore I'm trying to prove (P => Q) => ((P ^ R) => (Q ^ R)) and having some trouble introducing the R, my current train of thought leaves me with an assumption i can't get rid of.
    Code:
    1, H:       P => Q
    2, H:           P
    3, =>E 1,2:         Q
    4, H:                    R
    5, ^I 2,4:                    P ^ R
    6, ^I 3,4:                    Q ^ R
    7, =>I 5,6:              (P ^ R) => (Q ^ R)
    8, =>I 1,7: (P => Q) => ((P ^ R) => (Q ^ R))
    As you see, I'm left out with an assumption too many. I guess I'm introducing the R (4) incorrect, any pointers?
    Same mistake: you need to assume P ^ R instead of proving it. From it you get P and (using another assumption P => Q) Q. From P ^ R you also get R and hence Q ^ R.
    Follow Math Help Forum on Facebook and Google+

  4. #4
    Junior Member
    Joined
    Jul 2011
    Posts
    53

    Re: Abstract reasoning/natural deduction with Fitch

    Hmm, I see. Is there some sort of 'algorithm' I should follow when trying to solve questions like this?
    Currently I try to work from bottom to top and fill in blanks when needed and apparantly I'm not quite sure what's allowed to be used as a hypotheses..
    Follow Math Help Forum on Facebook and Google+

  5. #5
    MHF Contributor
    Joined
    Oct 2009
    Posts
    5,513
    Thanks
    769

    Re: Abstract reasoning/natural deduction with Fitch

    At least when the formula has only conjunctions and implications and its proof uses only the rules for those connectives (no reasoning by contradiction, for example), then the principle is pretty simple. Each branch in the shortest derivation starts with a series of elimination rules and ends with a series of introduction rules. So, going bottom up, you introduce all assumptions and split all conjunctions, and then see what you can get with the assumptions you collected.
    Follow Math Help Forum on Facebook and Google+

  6. #6
    Junior Member
    Joined
    Jul 2011
    Posts
    53

    Re: Abstract reasoning/natural deduction with Fitch

    After reading your answer regarding

    Code:
    1, H:       P
    2, H:           Q
    3, ^I 1,2:          P ^ Q
    4, ^E 3:            Q
    5, =>I 3,4:    (P ^ Q) => Q
    6, =>I 1,5: P => ((P ^ Q) => Q
    Cannot close P ^ Q: not an assumption. You need to assume P ^ Q (along with a vacuous assumption P) and deduce Q by ^E.
    I'm not sure if I follow, instead of assuming Q, I should've assumed P ^ Q as follows:
    Code:
    1, H:       P
    2, H:           P ^ Q
    3, ^E 2:            Q
    4, =>I 2,3:    (P ^ Q) => Q
    5, =>I 1,4: P => ((P ^ Q) => Q
    Is this correct? If so then I think I understand this part now.
    I'm going to spend the evening practicing (at work now, 40 hour job next to uni is hard work, especially if you cant attend lectures because of it :<) and then ND with negation, disjunction and quantifiers is next Thanks again!
    Follow Math Help Forum on Facebook and Google+

  7. #7
    MHF Contributor
    Joined
    Oct 2009
    Posts
    5,513
    Thanks
    769

    Re: Abstract reasoning/natural deduction with Fitch

    Quote Originally Posted by Lepzed View Post
    Code:
    1, H:       P
    2, H:           P ^ Q
    3, ^E 2:            Q
    4, =>I 2,3:    (P ^ Q) => Q
    5, =>I 1,4: P => ((P ^ Q) => Q
    Yes, this is correct.
    Follow Math Help Forum on Facebook and Google+

  8. #8
    Junior Member
    Joined
    Jul 2011
    Posts
    53

    Re: Abstract reasoning/natural deduction with Fitch

    I can't help but trying to work on (P => Q) => ((P ^ R) => (Q ^ R)) during lunch break
    Code:
    1, H:       P => Q
    2, H:           P ^ R
    3, ^E 2:            P   
    4, =>E 1,3:         Q
    5, ^E 2:            R
    6, ^I 4,5:          Q ^ R 
    7, =>I 2,6:    (P ^ R) => (Q ^ R)
    8, =>I 1,7: (P => Q) => ((P ^ R) => (Q ^ R))
    I'm having some doubts about the long list of conclusions starting at 3, is this allowed?
    Follow Math Help Forum on Facebook and Google+

  9. #9
    MHF Contributor
    Joined
    Oct 2009
    Posts
    5,513
    Thanks
    769

    Re: Abstract reasoning/natural deduction with Fitch

    Yes, you are absolutely right. Good work.
    Follow Math Help Forum on Facebook and Google+

  10. #10
    Junior Member
    Joined
    Jul 2011
    Posts
    53

    Re: Abstract reasoning/natural deduction with Fitch

    I've been working on some examples and exercises, and I think I'm getting there, there are however 4 exercises I'm having some difficulties with, I was hoping I could get soms feedback on them, since they're a bit harder than the rest. I think I've done 2 of them reasonably well, the other 2 not so much Still, just implication and conjunction.

    1) (P => Q) => (P => (P ^ Q))
    Code:
    1, H:        P => Q
    2, H:             P
    3, => E 1,2:           Q
    4, ^I 2,3:             P ^ Q
    5, =>I 2,4:       P => (P ^ Q)
    6, =>I 1,5: (P => Q) => (P => (P ^ Q))
    Seems sound, right?

    2) ((P => Q) ^ (R => S)) => ((P ^ R) => (Q ^ S))
    Code:
     1, H:           (P => Q)  ^ (R => S)
     2, H:                (P ^ R)
     3, ^E 1:                   P => Q
     4, ^E 1:                   R => S
     5, ^E 2:                   P
     6, ^E 2:                   R
     7, =>E 3,5:                Q                
     8, =>E 4,6:                S
     9, ^I 5,6:                 P ^ R
    10, ^I 7,8:                 Q ^ S
    11, =>I 9, 10:             (P ^ R) => (Q ^ S)
    12, =>I 1, 11: ((P => Q) ^ (R => S)) => ((P ^ R) => (Q ^ S))
    I think I did this okay, I have no idea how to do this otherwise.

    3) (P => Q) => ((R => (P => Q)) ^ ((P ^ R) => Q))
    Code:
     1, H:         P => Q
     2, H:              P ^ R
     3, ^E 2:               P
     4, ^E 2:               R
     5, =>E 1,3:            Q
     6, =>I 4,1:            R => (P = > Q)
     7, H:              P ^ R
     8, ^E 7:               P
     9, =>E 1,8             Q
    10, =>I 7,9:        (P ^ R) => Q
    11, ^I 6, 10: (R => (P => Q)) ^ ((P ^ R) => Q)
    12, =>I 1, 11: (P => Q) => ((R => (P => Q)) ^ ((P ^ R) => Q))
    This one I'm not so sure about. Seems a bit redundant to assume P ^ Q twice for example, but I'm not sure how else I can get to the ^I I need to connect the two parts.

    And lastly:
    4) (P => (Q => R)) => ((P => Q) => (P => R))
    And this one I get stuck, doing too many assumptions.
    I tried the following
    Code:
     1, H:         P => (Q => R)
     2, H:              P ^ Q
     3, ^E 2:               P
     4, ^E 2:               Q
     5, =>I 2,3:        P => Q
     6, H:              P ^ Q
     7, ^E 6:               P
     8, ^E 6                Q
     9, =>E 1,7:            Q => R
    10, =>E 8,9:            R
    11, =>I 7, 10:       P => R
    Im stuck here, again, assuming the same thing twice just seems wrong. I can't really wrap my head around it, any tips? I seem to miss an assumption as well, but if I would assume P, well think im being twice as redundant :P May be it's super easy, but I think this is rather harder than the other exercises hehe
    Follow Math Help Forum on Facebook and Google+

  11. #11
    MHF Contributor
    Joined
    Oct 2009
    Posts
    5,513
    Thanks
    769

    Re: Abstract reasoning/natural deduction with Fitch

    Quote Originally Posted by Lepzed View Post
    1) (P => Q) => (P => (P ^ Q))
    Code:
    1, H:        P => Q
    2, H:             P
    3, => E 1,2:           Q
    4, ^I 2,3:             P ^ Q
    5, =>I 2,4:       P => (P ^ Q)
    6, =>I 1,5: (P => Q) => (P => (P ^ Q))
    Correct.

    Quote Originally Posted by Lepzed View Post
    2) ((P => Q) ^ (R => S)) => ((P ^ R) => (Q ^ S))
    Code:
     1, H:           (P => Q)  ^ (R => S)
     2, H:                (P ^ R)
     3, ^E 1:                   P => Q
     4, ^E 1:                   R => S
     5, ^E 2:                   P
     6, ^E 2:                   R
     7, =>E 3,5:                Q                
     8, =>E 4,6:                S
     9, ^I 5,6:                 P ^ R
    10, ^I 7,8:                 Q ^ S
    11, =>I 9, 10:             (P ^ R) => (Q ^ S)
    12, =>I 1, 11: ((P => Q) ^ (R => S)) => ((P ^ R) => (Q ^ S))
    Line 9 is not needed, and line 11 should close line 2.

    Quote Originally Posted by Lepzed View Post
    3) (P => Q) => ((R => (P => Q)) ^ ((P ^ R) => Q))
    Code:
     1, H:         P => Q
     2, H:              P ^ R
     3, ^E 2:               P
     4, ^E 2:               R
     5, =>E 1,3:            Q
     6, =>I 4,1:            R => (P = > Q)
     7, H:              P ^ R
     8, ^E 7:               P
     9, =>E 1,8             Q
    10, =>I 7,9:        (P ^ R) => Q
    11, ^I 6, 10: (R => (P => Q)) ^ ((P ^ R) => Q)
    12, =>I 1, 11: (P => Q) => ((R => (P => Q)) ^ ((P ^ R) => Q))
    Line 6 closes line 4, which is not an assumption. Should be like this.

    Code:
     1, H:        P => Q
     2, H:              R
     3, =>I 1,2:        R => (P => Q)
     4, H:              P ^ R
     5, ^E 4:               P
     6, =>E 1,5:            Q
     7, =>I 4,6:        P ^ R => Q
     8, ^I 3, 7:        (R => (P => Q)) ^ ((P ^ R) => Q)
     9, =>I 1, 8: (P => Q) => ((R => (P => Q)) ^ ((P ^ R) => Q))
    I am not sure if the hypothesis 1 should be repeated between lines 2 and 3 (probably not). In a tree-form derivation, the hypothesis P => Q occurs twice, but in Fitch style it should probably be declared just once.

    Quote Originally Posted by Lepzed View Post
    4) (P => (Q => R)) => ((P => Q) => (P => R))
    And this one I get stuck, doing too many assumptions.
    I tried the following
    Code:
     1, H:         P => (Q => R)
     2, H:              P ^ Q
     3, ^E 2:               P
     4, ^E 2:               Q
     5, =>I 2,3:        P => Q
     6, H:              P ^ Q
     7, ^E 6:               P
     8, ^E 6                Q
     9, =>E 1,7:            Q => R
    10, =>E 8,9:            R
    11, =>I 7, 10:       P => R
    In the shortest derivation, all formulas should be subformulas of open assumptions or of the conclusion. (If I remember correctly, this is true when double-negation elimination is not used.) So, P ^ Q is not needed; one can do with implication only.

    There are three levels. You assume P => (Q => R)), (P => Q), and P, and then you derive in turn:

    Q => R
    Q
    R

    and close everything.

    Also, note that rule #8 in this sticky thread says not to ask more than two questions in one thread.
    Follow Math Help Forum on Facebook and Google+

Similar Math Help Forum Discussions

  1. natural deduction
    Posted in the Discrete Math Forum
    Replies: 3
    Last Post: December 12th 2011, 08:31 AM
  2. Natural Deduction
    Posted in the Discrete Math Forum
    Replies: 9
    Last Post: June 9th 2011, 03:15 AM
  3. Could use some help with a Natural Deduction proof
    Posted in the Discrete Math Forum
    Replies: 2
    Last Post: May 4th 2010, 05:58 AM
  4. natural deduction
    Posted in the Discrete Math Forum
    Replies: 5
    Last Post: April 24th 2010, 11:47 AM
  5. Help with Logic (Natural Deduction)
    Posted in the Discrete Math Forum
    Replies: 7
    Last Post: January 12th 2010, 02:07 PM

Search Tags


/mathhelpforum @mathhelpforum