SOLUTION: I have been on these proofs for days and I can't seem to figure my homework out. Thank you for looking at this problem. Here is an example that would help me if figured out. N>[

Algebra ->  Proofs -> SOLUTION: I have been on these proofs for days and I can't seem to figure my homework out. Thank you for looking at this problem. Here is an example that would help me if figured out. N>[      Log On


   

Question 1003311: I have been on these proofs for days and I can't seem to figure my homework out. Thank you for looking at this problem. Here is an example that would help me if figured out.
N>[(P>P)>W] / W>{[M>(I>M)]>(O.~O)} // ~N
The > represents the horseshoe
Thanks again.
Answer by jim_thompson5910(35256) About Me  (Show Source):
You can put this solution on YOUR website!
This proof was very difficult. Probably the longest and most difficult (or one of the most difficult) I've ever come across. There may be an easier way, but I haven't found it. It took me quite a wihle to figure it out, so that may explain why I'm not the most efficient in this derivation.

NumberStatementLines UsedReason
1N > [(P > P) > W]
2W > {[M > (I > M)] > (O * ~O)}
:.~N
|3~~NAIP
|4N3DN
|5(P > P) > W1,4MP
|6(~P v P) > W5MI
|7~(~P v P) v W6MI
|8(~~P * ~P) v W7DM
|9(P * ~P) v W8DN
|10W v (P * ~P)9Comm
|11(W v P) * (W v ~P)10Dist
|12(W v ~P) * (W v P)11Comm
|13W v P11Simp
|14W v ~P12Simp
|15~~W v P13DN
|16~~W v ~P14DN
|17~W > P15MI
|18~W > ~P16MI
|19~~P > ~~W18Trans
|20P > W19DN
|21~W > W17,20HS
|22~~W v W21MI
|23W v W22DN
|24W23Taut
|25[M > (I > M)] > (O * ~O)2,24MP
|26[M > (~I v M)] > (O * ~O)25MI
|27[~M v (~I v M)] > (O * ~O)26MI
|28~[~M v (~I v M)] v (O * ~O)27MI
|29[~~M * ~(~I v M)] v (O * ~O)28DM
|30[M * ~(~I v M)] v (O * ~O)29DN
|31[M * (~~I * ~M)] v (O * ~O)30DM
|32[M * (I * ~M)] v (O * ~O)31DN
|33[M v (O * ~O)] * [(I * ~M) v (O * ~O)]32Dist
|34[(I * ~M) v (O * ~O)] * [M v (O * ~O)]33Comm
|35M v (O * ~O)33Simp
|36(I * ~M) v (O * ~O)34Simp
|37[(I * ~M) v O] * [(I * ~M) v ~O)]36Dist
|38[(I * ~M) v ~O)] * [(I * ~M) v O]37Comm
|39(I * ~M) v O37Simp
|40O v (I * ~M)39Comm
|41~~O v (I * ~M)40DN
|42~O > (I * ~M)41MI
|43(I * ~M) v ~O38Simp
|44~O v (I * ~M)43Comm
|45~~O > (I * ~M)44MI
|46O > (I * ~M)45DN
|47~(I * ~M) > ~O46Trans
|48~(I * ~M) > (I * ~M)47,42HS
|49~~(I * ~M) v (I * ~M)48MI
|50(I * ~M) v (I * ~M)49DN
|51I * ~M50Taut
|52~M * I51Comm
|53~M52Simp
|54O * ~O35,53DS
55~(~~N)3-54IP
56~N55DN

Acronyms/Abbreviations Used:

AIP = Assumption for Indirect Proof
Comm = Commutation
Dist = Distribution
DM = De Morgan's Law
DN = Double Negation
DS = Disjunctive Syllogism
HS = Hypothetical Syllogism
IP = Indirect Proof (aka proof by contradiction)
MI = Material Implication
MP = Modus Ponens
Simp = Simplification
Taut = Tautology
Trans = Transposition