Results 1 to 6 of 6

Math Help - Derive C V ~A

  1. #1
    Member
    Joined
    Oct 2010
    Posts
    150

    Derive C V ~A

    1| A⊃(B ∧ ~C) ASS
    2| C V ~ B ASS


    So far I have:


    1| A⊃(B ∧ ~C) ASS
    2| C V ~ B ASS
    3 |A ASS/⊃E
    4 |B ∧ ~C 1,3⊃E
    5 |B 4, ∧E
    6 |~C 4, ∧E


    I'm not sure how to progress from here. I tried disjunction intro. on the next line to get ~C V ~B but it didn't help. Any ideas would be appreciated!
    Follow Math Help Forum on Facebook and Google+

  2. #2
    MHF Contributor
    Joined
    Oct 2009
    Posts
    5,537
    Thanks
    778

    Re: Derive C V ~A

    To continue your proof, use disjunction elimination (reasoning by cases) on C \/ ~B. Assuming either C or ~B leads to contradiction with formulas in steps 5 and 6. So, in fact, from 1 and 2 you can derive ~A, which is stronger than C \/ ~A.
    Follow Math Help Forum on Facebook and Google+

  3. #3
    Member
    Joined
    Oct 2010
    Posts
    150

    Re: Derive C V ~A

    The problem is, I see the contradction, but I don't know how to write it out syntactically correct with the rules. Do I assume C or ~B for the purposes of negation introduction?
    Follow Math Help Forum on Facebook and Google+

  4. #4
    MHF Contributor
    Joined
    Oct 2009
    Posts
    5,537
    Thanks
    778

    Re: Derive C V ~A

    At this point it would be nice if you specified the proof system you are using, according to this sticky thread. My guess that it is Fitch-style natural deduction. Do you have the description of the marks on the right, such as ASS/⊃E? Also, are you familiar with the disjunction elimination rule?

    Do I assume C or ~B for the purposes of negation introduction?
    Both in turn using disjunction elimination.
    Follow Math Help Forum on Facebook and Google+

  5. #5
    Member
    Joined
    Oct 2010
    Posts
    150

    Re: Derive C V ~A

    The book calls the system "SD", and refers to it as a "derivation system". What do you mean by the description? For example, ASS/⊃E means assumption for the purposes of conditional elimination, if that's what you mean.
    Follow Math Help Forum on Facebook and Google+

  6. #6
    MHF Contributor
    Joined
    Oct 2009
    Posts
    5,537
    Thanks
    778

    Re: Derive C V ~A

    It sure is not easy to extract information from you Which book are you using? (I am interested to know anyway, but I won't be able to consult it to see the description of the proof system unless it is online.) Also, you have not said if you understand disjunction elimination, which is important in this example.

    Here is my best guess about the complete derivation.
    Code:
     1| C ∨ ~B ASS
     2|| C ASS/∨E
     3|| A ⊃ (B ∧ ~C) ASS
     4||| A ASS/~I
     5||| B ∧ ~C 4,3⊃E
     6||| ~C 5∧E
     7|| ~A 4,2,6~I
     8|| ~B ASS/∨E
     9|| A ⊃ (B ∧ ~C) ASS
    10||| A ASS/~I
    11||| B ∧ ~C 10,11⊃E
    12||| B 11∧E
    13|| ~A 10,12,8~I
    14| ~A 1,2,7,8,13∨E
    15| C ∨ ~A 14∨I
    I prefer a tree presentation of the derivation. Here closed assumptions are labeled with step numbers in the derivation above where these assumptions are introduced. Similarly, rules that close assumptions (~I and ∨E) are labeled with the assumptions' numbers.
    Follow Math Help Forum on Facebook and Google+

Similar Math Help Forum Discussions

  1. Replies: 2
    Last Post: March 27th 2011, 08:19 AM
  2. Derive this?
    Posted in the Calculus Forum
    Replies: 7
    Last Post: January 23rd 2011, 12:05 PM
  3. Help with to derive this
    Posted in the Calculus Forum
    Replies: 5
    Last Post: August 14th 2010, 12:23 AM
  4. Derive 6 help please
    Posted in the Math Software Forum
    Replies: 0
    Last Post: April 8th 2009, 05:00 PM
  5. derive
    Posted in the Calculus Forum
    Replies: 1
    Last Post: March 29th 2009, 09:42 PM

Search Tags


/mathhelpforum @mathhelpforum