Question 1009931
Conditional Proof


<table border=1><tr><th colspan="2">Number</th><th>Statement</th><th>Lines Used</th><th>Reason</th></tr><tr><td>:.</td><td></td><td>P -&gt; (~P -&gt; (Q &lt;-&gt; (R v S)))</td><td></td><td></td></tr><tr><td></td><td>1</td><td>P</td><td></td><td>ACP</td></tr><tr><td></td><td>2</td><td>~~P</td><td>1</td><td>DN</td></tr><tr><td></td><td>3</td><td>~~P v (P -&gt; (Q &lt;-&gt; (R v S)))</td><td>2</td><td>Add</td></tr><tr><td></td><td>4</td><td>~P -&gt; (P -&gt; (Q &lt;-&gt; (R v S)))</td><td>3</td><td>MI</td></tr><tr><td></td><td>5</td><td>(~P &amp; P) -&gt; (Q &lt;-&gt; (R v S))</td><td>4</td><td>Exp</td></tr><tr><td></td><td>6</td><td>(P &amp; ~P) -&gt; (Q &lt;-&gt; (R v S))</td><td>5</td><td>Comm</td></tr><tr><td></td><td>7</td><td>P -&gt; (~P -&gt; (Q &lt;-&gt; (R v S)))</td><td>6</td><td>Exp</td></tr><tr><td>8</td><td></td><td>P -&gt; {P -&gt; (~P -&gt; (Q &lt;-&gt; (R v S)))}</td><td>1-7</td><td>CP</td></tr><tr><td>9</td><td></td><td>(P &amp; P) -&gt; (~P -&gt; (Q &lt;-&gt; (R v S)))</td><td>8</td><td>Exp</td></tr><tr><td>10</td><td></td><td>P -&gt; (~P -&gt; (Q &lt;-&gt; (R v S)))</td><td>9</td><td>Taut</td></tr></table>


-------------------------------------------------------------------------------


Proof by contradiction (alternate method)



<table border=1><tr><th colspan="2">Number</th><th>Statement</th><th>Lines Used</th><th>Reason</th></tr><tr><td>:.</td><td></td><td>P -&gt; (~P -&gt; (Q &lt;-&gt; (R v S)))</td><td></td><td></td></tr><tr><td></td><td>1</td><td>~[P -&gt; (~P -&gt; (Q &lt;-&gt; (R v S)))]</td><td></td><td>AIP</td></tr><tr><td></td><td>2</td><td>~[~P v (~P -&gt; (Q &lt;-&gt; (R v S)))]</td><td>1</td><td>MI</td></tr><tr><td></td><td>3</td><td>~[~P v (~~P v (Q &lt;-&gt; (R v S)))]</td><td>2</td><td>MI</td></tr><tr><td></td><td>4</td><td>~[~P v (P v (Q &lt;-&gt; (R v S)))]</td><td>3</td><td>DN</td></tr><tr><td></td><td>5</td><td>~[(~P v P) v (Q &lt;-&gt; (R v S))]</td><td>4</td><td>Assoc</td></tr><tr><td></td><td>6</td><td>~(~P v P) &amp; ~(Q &lt;-&gt; (R v S))</td><td>5</td><td>DM</td></tr><tr><td></td><td>7</td><td>~(~P v P)</td><td>6</td><td>Simp</td></tr><tr><td></td><td>8</td><td>~~P &amp; ~P</td><td>7</td><td>DM</td></tr><tr><td></td><td>9</td><td>P &amp; ~P</td><td>8</td><td>DN</td></tr><tr><td>10</td><td></td><td>P -&gt; (~P -&gt; (Q &lt;-&gt; (R v S)))</td><td>1-9</td><td>IP</td></tr></table>



-------------------------------------------------------------------------------



Abbreviations/Acronyms Used


ACP = Assumption for Conditional Proof
AIP = Assumption for Indirect Proof (aka proof by contradiction)
Add = Addition
Assoc = Associative Rule
Comm = Commutation
CP = Conditional Proof
DM = De Morgan's Law
DN = Double Negation
Exp = Exportation
IP = Indirect Proof (aka proof by contradiction)
MI = Material Implication
Simp = Simplification
Taut = Tautology