Question 1003311
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.


<table border=1><tr><th colspan="2">Number</th><th>Statement</th><th>Lines Used</th><th>Reason</th></tr><tr><td>1</td><td></td><td>N &gt; [(P &gt; P) &gt; W]</td><td></td><td></td></tr><tr><td>2</td><td></td><td>W &gt; {[M &gt; (I &gt; M)] &gt; (O * ~O)}</td><td></td><td></td></tr><tr><td>:.</td><td></td><td>~N</td><td></td><td></td></tr><tr><td>|</td><td>3</td><td>~~N</td><td></td><td>AIP</td></tr><tr><td>|</td><td>4</td><td>N</td><td>3</td><td>DN</td></tr><tr><td>|</td><td>5</td><td>(P &gt; P) &gt; W</td><td>1,4</td><td>MP</td></tr><tr><td>|</td><td>6</td><td>(~P v P) &gt; W</td><td>5</td><td>MI</td></tr><tr><td>|</td><td>7</td><td>~(~P v P) v W</td><td>6</td><td>MI</td></tr><tr><td>|</td><td>8</td><td>(~~P * ~P) v W</td><td>7</td><td>DM</td></tr><tr><td>|</td><td>9</td><td>(P * ~P) v W</td><td>8</td><td>DN</td></tr><tr><td>|</td><td>10</td><td>W v (P * ~P)</td><td>9</td><td>Comm</td></tr><tr><td>|</td><td>11</td><td>(W v P) * (W v ~P)</td><td>10</td><td>Dist</td></tr><tr><td>|</td><td>12</td><td>(W v ~P) * (W v P)</td><td>11</td><td>Comm</td></tr><tr><td>|</td><td>13</td><td>W v P</td><td>11</td><td>Simp</td></tr><tr><td>|</td><td>14</td><td>W v ~P</td><td>12</td><td>Simp</td></tr><tr><td>|</td><td>15</td><td>~~W v P</td><td>13</td><td>DN</td></tr><tr><td>|</td><td>16</td><td>~~W v ~P</td><td>14</td><td>DN</td></tr><tr><td>|</td><td>17</td><td>~W &gt; P</td><td>15</td><td>MI</td></tr><tr><td>|</td><td>18</td><td>~W &gt; ~P</td><td>16</td><td>MI</td></tr><tr><td>|</td><td>19</td><td>~~P &gt; ~~W</td><td>18</td><td>Trans</td></tr><tr><td>|</td><td>20</td><td>P &gt; W</td><td>19</td><td>DN</td></tr><tr><td>|</td><td>21</td><td>~W &gt; W</td><td>17,20</td><td>HS</td></tr><tr><td>|</td><td>22</td><td>~~W v W</td><td>21</td><td>MI</td></tr><tr><td>|</td><td>23</td><td>W v W</td><td>22</td><td>DN</td></tr><tr><td>|</td><td>24</td><td>W</td><td>23</td><td>Taut</td></tr><tr><td>|</td><td>25</td><td>[M &gt; (I &gt; M)] &gt; (O * ~O)</td><td>2,24</td><td>MP</td></tr><tr><td>|</td><td>26</td><td>[M &gt; (~I v M)] &gt; (O * ~O)</td><td>25</td><td>MI</td></tr><tr><td>|</td><td>27</td><td>[~M v (~I v M)] &gt; (O * ~O)</td><td>26</td><td>MI</td></tr><tr><td>|</td><td>28</td><td>~[~M v (~I v M)] v (O * ~O)</td><td>27</td><td>MI</td></tr><tr><td>|</td><td>29</td><td>[~~M * ~(~I v M)] v (O * ~O)</td><td>28</td><td>DM</td></tr><tr><td>|</td><td>30</td><td>[M * ~(~I v M)] v (O * ~O)</td><td>29</td><td>DN</td></tr><tr><td>|</td><td>31</td><td>[M * (~~I * ~M)] v (O * ~O)</td><td>30</td><td>DM</td></tr><tr><td>|</td><td>32</td><td>[M * (I * ~M)] v (O * ~O)</td><td>31</td><td>DN</td></tr><tr><td>|</td><td>33</td><td>[M  v (O * ~O)] * [(I * ~M) v (O * ~O)]</td><td>32</td><td>Dist</td></tr><tr><td>|</td><td>34</td><td>[(I * ~M) v (O * ~O)] * [M  v (O * ~O)]</td><td>33</td><td>Comm</td></tr><tr><td>|</td><td>35</td><td>M  v (O * ~O)</td><td>33</td><td>Simp</td></tr><tr><td>|</td><td>36</td><td>(I * ~M) v (O * ~O)</td><td>34</td><td>Simp</td></tr><tr><td>|</td><td>37</td><td>[(I * ~M) v O] * [(I * ~M) v ~O)]</td><td>36</td><td>Dist</td></tr><tr><td>|</td><td>38</td><td>[(I * ~M) v ~O)] * [(I * ~M) v O]</td><td>37</td><td>Comm</td></tr><tr><td>|</td><td>39</td><td>(I * ~M) v O</td><td>37</td><td>Simp</td></tr><tr><td>|</td><td>40</td><td>O v (I * ~M)</td><td>39</td><td>Comm</td></tr><tr><td>|</td><td>41</td><td>~~O v (I * ~M)</td><td>40</td><td>DN</td></tr><tr><td>|</td><td>42</td><td>~O &gt; (I * ~M)</td><td>41</td><td>MI</td></tr><tr><td>|</td><td>43</td><td>(I * ~M) v ~O</td><td>38</td><td>Simp</td></tr><tr><td>|</td><td>44</td><td>~O v (I * ~M)</td><td>43</td><td>Comm</td></tr><tr><td>|</td><td>45</td><td>~~O &gt; (I * ~M)</td><td>44</td><td>MI</td></tr><tr><td>|</td><td>46</td><td>O &gt; (I * ~M)</td><td>45</td><td>DN</td></tr><tr><td>|</td><td>47</td><td>~(I * ~M) &gt; ~O</td><td>46</td><td>Trans</td></tr><tr><td>|</td><td>48</td><td>~(I * ~M) &gt; (I * ~M)</td><td>47,42</td><td>HS</td></tr><tr><td>|</td><td>49</td><td>~~(I * ~M) v (I * ~M)</td><td>48</td><td>MI</td></tr><tr><td>|</td><td>50</td><td>(I * ~M) v (I * ~M)</td><td>49</td><td>DN</td></tr><tr><td>|</td><td>51</td><td>I * ~M</td><td>50</td><td>Taut</td></tr><tr><td>|</td><td>52</td><td>~M * I</td><td>51</td><td>Comm</td></tr><tr><td>|</td><td>53</td><td>~M</td><td>52</td><td>Simp</td></tr><tr><td>|</td><td>54</td><td>O * ~O</td><td>35,53</td><td>DS</td></tr><tr><td>55</td><td></td><td>~(~~N)</td><td>3-54</td><td>IP</td></tr><tr><td>56</td><td></td><td>~N</td><td>55</td><td>DN</td></tr></table>

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