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

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