SD Theorems Logic HW due Please help

[yankes2k]

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.

Thanks,

-Tony

[honestrosewater]

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?

[yankes2k]

I can use conjunction elimination and introduction
biconditional introduction and elimination
negation elimination/introduction
disjunction elimination/introduction
conditional introduction and elimination

that's it.

[yankes2k]

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!

[honestrosewater]

I can use conjunction elimination and introduction
biconditional introduction and elimination
negation elimination/introduction
disjunction elimination/introduction
conditional introduction and elimination

that's it.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.

[yankes2k]

conjunction ibtroduction
P
Q
P&Q

conjunction Elination
P&Q
P or Q

biconditional introduction

Sub Der:Assume P
Q

Assume Q
P
P (triple Bar) Q

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

Disjunction Intro

P

PvQ or QvP

Disjunction Elination

PvQ
sub Derivation: P
R

Sub Derivation:Q
R
Therefore, R

Negation introduction

Subderivation:P
Q
~Q
Therefore, ~P

Negation Elimination
Sub derivation:~P
Q
~Q
THerefore, P

[yankes2k]

Sorry forgot conditional intro and elimination

Condition elimination

P implies Q
P
Therefore, Q

Condition introduction
Subderivation:P
Q
Therefore, P implies Q

[honestrosewater]

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]
3)

Maybe you can think of a way to do this using your rules.

[honestrosewater]

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]

[honestrosewater]

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?