Dismiss Notice
Join Physics Forums Today!
The friendliest, high quality science and math community on the planet! Everyone who loves science is here!

Homework Help: SD Theorems Logic HW due Please help

  1. Jun 5, 2005 #1
    Hi everyone,

    I really need help proving a theorem for logic HW. I am allowed to use all the standard derivations in Sentential Logic.

    Also I do not know how to enter in the symbols so I will use ">" to signify conditional in the problem below.

    Instructions: Show that each of the following is a theorem in SD by constructing a derivation.

    1:) ~A>((B&A)>C)

    2:) (AvB)>(BvA)

    If someone could help me out I would really appreciate it as I am so lost right now.


  2. jcsd
  3. Jun 6, 2005 #2


    User Avatar
    Gold Member

    1:) ~A>((B&A)>C)
    Assume ~A. Use Commutation and Exportation ([(p & q) -> r] <=> [p -> (q -> r)]) on [(B & A) -> C] to get a new statement. See it now?

    2:) (AvB)>(BvA)
    Eh, this is just Commutation. Do you not have a rule that says [(p v q) <=> (q v p)]?
    Edit: Okay, that's probably a stupid question on my part. Can you type up the rules you have? I'm guessing you have Modus Ponens, Modus Tollens,
    (p & q) => p
    p, q, => (p & q)
    p => p v q
    What else?
    Last edited: Jun 6, 2005
  4. Jun 6, 2005 #3
    I can use conjunction elimination and introduction
    biconditional introduction and elimination
    negation elimination/introduction
    disjunction elimination/introduction
    conditional introduction and elimination

    that's it.
  5. Jun 6, 2005 #4
    Also I don't know how to use "Commutation and Exportation" rules either. We can only use what is listed above. Class is at 1:30 U.S. Eastern standard time please help!
  6. Jun 6, 2005 #5


    User Avatar
    Gold Member

    I have to go look up what these rules are- they go by different names. If you really want to save time, you could type out the rules.
  7. Jun 6, 2005 #6
    conjunction ibtroduction

    conjunction Elination
    P or Q

    biconditional introduction

    Sub Der:Assume P

    Assume Q
    P (triple Bar) Q

    biconditional Elimination
    P (triple bar) Q
    P or Q
    THerefore, Q Therefore, P

    Disjunction Intro


    PvQ or QvP

    Disjunction Elination

    sub Derivation: P

    Sub Derivation:Q
    Therefore, R

    Negation introduction

    Therefore, ~P

    Negation Elimination
    Sub derivation:~P
    THerefore, P
  8. Jun 6, 2005 #7
    Sorry forgot conditional intro and elimination

    Condition elimination

    P implies Q
    Therefore, Q

    Condition introduction
    Therefore, P implies Q
  9. Jun 6, 2005 #8


    User Avatar
    Gold Member

    Okay, I'm used to having more rules- every proof I think of uses rules you don't have. While I'm thinking, here's what I meant earlier:
    1) (B & A) -> C
    2) (A & B) -> C [1, Commutation]
    3) A -> (B -> C) [2, Exportation]
    4) ~A v (B -> C) [3, Implication]

    So you would just go backwards. In your proof, you assume ~A (hypothetically) and try to derive (B & A) -> C, so you can infer ~A -> (B & A) -> C.

    1) ~A [conditional introduction]
    2) ~A v (B -> C) [1, disjunction introduction]

    Maybe you can think of a way to do this using your rules.
  10. Jun 6, 2005 #9


    User Avatar
    Gold Member

    I'll just name the rules that you need, and maybe you can prove them yourself. Or maybe you have already proven them.

    (P -> Q) <=> (~P v Q)
    (P -> Q) <=> (~Q -> ~P)
    (~~P) <=> P

    If you can prove those:

    1)) A v B [conditional intro]
    2)) ~~A v B [1, subproof (~~P) <=> P]
    3)) ~A -> B [2, subproof (P -> Q) <=> (~P v Q)]
    4)) ~B -> ~~A [3, subproof (P -> Q) <=> (~Q -> ~P)]
    5)) ~B -> A [4, subproof (~~P) <=> P]
    6)) B v A [5, subproof (P -> Q) <=> (~P v Q)]
    7) (A v B) -> (B v A) [1, 6, conditional intro]
  11. Jun 6, 2005 #10


    User Avatar
    Gold Member

    Are you still there?

    (P & Q) <=> (Q & P) is easy as pie
    1)) P & Q
    2)) Q
    3)) P
    4)) Q & P
    5) (P & Q) -> (Q & P)
    Repeat other way. So you have commutation for conjunction: (P & Q) <=> (Q & P)

    Exportation the way you need it is also easy as pie, if you have (P -> Q) <=> (~P v Q):

    1)) P -> (Q -> R) [1, conditional intro)
    2)) ~P v (Q -> R) [2, subproof (P -> Q) <=> (~P v Q)]
    3)) ~P v (~Q v R) [3, subproof (P -> Q) <=> (~P v Q)]
    4)) (~P v ~Q) v R [4, Please say you've proved association?]
    5)) ~(P & Q) v R [5, and DeMorgan's Theorems?]
    6)) (P & Q) -> R [6, subproof (P -> Q) <=> (~P v Q)]
    7) (P -> (Q -> R)) -> ((P & Q) -> R [1, 6]

    Have you seen these before? Am I just scaring you?
Share this great discussion with others via Reddit, Google+, Twitter, or Facebook