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

Related Introductory Physics Homework Help News on Phys.org
honestrosewater
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:
I can use conjunction elimination and introduction
biconditional introduction and elimination
negation elimination/introduction
disjunction elimination/introduction
conditional introduction and elimination

that's it.

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
Gold Member
yankes2k said:
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.

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

Sorry forgot conditional intro and elimination

Condition elimination

P implies Q
P
Therefore, Q

Condition introduction
Subderivation:P
Q
Therefore, P implies Q

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

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

honestrosewater
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]

honestrosewater
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?