| 021 | Not participating FitchFX | 251002T152310Z | xamid |
| nan | | 250422T182827Z | Anders K |
Not participating (FitchFX, 21 steps)
I was curious in what a short natural deduction proof in a more reasonable system would look like. Here is my result. It can be imported to mrieppel.github.io/FitchFX/.
Problem: |- ((P > Q) <> (~P v Q))
1 | |_ (P > Q) Assumption
2 | | |_ ~(~P v Q) Assumption
3 | | | |_ P Assumption
4 | | | | Q >E 1,3
5 | | | | (~P v Q) vI 4
6 | | | | # ~E 2,5
7 | | | ~P ~I 3-6
8 | | | (~P v Q) vI 7
9 | | | # ~E 2,8
10 | | (~P v Q) IP 2-9
11 | |_ (~P v Q) Assumption
12 | | |_ P Assumption
13 | | | |_ ~Q Assumption
14 | | | | |_ ~P Assumption
15 | | | | | # ~E 12,14
16 | | | | |_ Q Assumption
17 | | | | | # ~E 13,16
18 | | | | # vE 11,14-15,16-17
19 | | | Q IP 13-18
20 | | (P > Q) >I 12-19
21 | ((P > Q) <> (~P v Q)) <>I 1-10,11-20
35 steps
|
sentence |
justification |
| 1. |
p => q |
Assumption |
| 2. |
~(~p | q) |
Assumption |
| 3. |
p |
Assumption |
| 4. |
q |
Implication Elimination: 1, 3 |
| 5. |
~p | q |
Or Introduction: 4 |
| 6. |
p => ~p | q |
Implication Introduction: 3, 5 |
| 7. |
p |
Assumption |
| 8. |
~(~p | q) |
Reiteration: 2 |
| 9. |
p => ~(~p | q) |
Implication Introduction: 7, 8 |
| 10. |
~p |
Negation Introduction: 6, 9 |
| 11. |
~p | q |
Or Introduction: 10 |
| 12. |
~(~p | q) => ~p | q |
Implication Introduction: 2, 11 |
| 13. |
~(~p | q) |
Assumption |
| 14. |
~(~p | q) => ~(~p | q) |
Implication Introduction: 13, 13 |
| 15. |
~~(~p | q) |
Negation Introduction: 12, 14 |
| 16. |
~p | q |
Negation Elimination: 15 |
| 17. |
(p => q) => ~p | q |
Implication Introduction: 1, 16 |
| 18. |
~p | q |
Assumption |
| 19. |
p |
Assumption |
| 20. |
~p |
Assumption |
| 21. |
~q |
Assumption |
| 22. |
p |
Reiteration: 19 |
| 23. |
~q => p |
Implication Introduction: 21, 22 |
| 24. |
~q |
Assumption |
| 25. |
~p |
Reiteration: 20 |
| 26. |
~q => ~p |
Implication Introduction: 24, 25 |
| 27. |
~~q |
Negation Introduction: 23, 26 |
| 28. |
q |
Negation Elimination: 27 |
| 29. |
~p => q |
Implication Introduction: 20, 28 |
| 30. |
q |
Assumption |
| 31. |
q => q |
Implication Introduction: 30, 30 |
| 32. |
q |
Or Elimination: 18, 29, 31 |
| 33. |
p => q |
Implication Introduction: 19, 32 |
| 34. |
~p | q => (p => q) |
Implication Introduction: 18, 33 |
| 35. |
p => q <=> ~p | q |
Biconditional Introduction: 17, 34 |
<proof>
<step>
<number>1</number>
<sentence>p => q</sentence>
<justification>Assumption</justification>
</step>
<step>
<number>2</number>
<sentence>~(~p | q)</sentence>
<justification>Assumption</justification>
</step>
<step>
<number>3</number>
<sentence>p</sentence>
<justification>Assumption</justification>
</step>
<step>
<number>4</number>
<sentence>q</sentence>
<justification>Implication Elimination</justification>
<antecedent>1</antecedent>
<antecedent>3</antecedent>
</step>
<step>
<number>5</number>
<sentence>~p | q</sentence>
<justification>Or Introduction</justification>
<antecedent>4</antecedent>
</step>
<step>
<number>6</number>
<sentence>p => ~p | q</sentence>
<justification>Implication Introduction</justification>
<antecedent>3</antecedent>
<antecedent>5</antecedent>
</step>
<step>
<number>7</number>
<sentence>p</sentence>
<justification>Assumption</justification>
</step>
<step>
<number>8</number>
<sentence>~(~p | q)</sentence>
<justification>Reiteration</justification>
<antecedent>2</antecedent>
</step>
<step>
<number>9</number>
<sentence>p => ~(~p | q)</sentence>
<justification>Implication Introduction</justification>
<antecedent>7</antecedent>
<antecedent>8</antecedent>
</step>
<step>
<number>10</number>
<sentence>~p</sentence>
<justification>Negation Introduction</justification>
<antecedent>6</antecedent>
<antecedent>9</antecedent>
</step>
<step>
<number>11</number>
<sentence>~p | q</sentence>
<justification>Or Introduction</justification>
<antecedent>10</antecedent>
</step>
<step>
<number>12</number>
<sentence>~(~p | q) => ~p | q</sentence>
<justification>Implication Introduction</justification>
<antecedent>2</antecedent>
<antecedent>11</antecedent>
</step>
<step>
<number>13</number>
<sentence>~(~p | q)</sentence>
<justification>Assumption</justification>
</step>
<step>
<number>14</number>
<sentence>~(~p | q) => ~(~p | q)</sentence>
<justification>Implication Introduction</justification>
<antecedent>13</antecedent>
<antecedent>13</antecedent>
</step>
<step>
<number>15</number>
<sentence>~~(~p | q)</sentence>
<justification>Negation Introduction</justification>
<antecedent>12</antecedent>
<antecedent>14</antecedent>
</step>
<step>
<number>16</number>
<sentence>~p | q</sentence>
<justification>Negation Elimination</justification>
<antecedent>15</antecedent>
</step>
<step>
<number>17</number>
<sentence>(p => q) => ~p | q</sentence>
<justification>Implication Introduction</justification>
<antecedent>1</antecedent>
<antecedent>16</antecedent>
</step>
<step>
<number>18</number>
<sentence>~p | q</sentence>
<justification>Assumption</justification>
</step>
<step>
<number>19</number>
<sentence>p</sentence>
<justification>Assumption</justification>
</step>
<step>
<number>20</number>
<sentence>~p</sentence>
<justification>Assumption</justification>
</step>
<step>
<number>21</number>
<sentence>~q</sentence>
<justification>Assumption</justification>
</step>
<step>
<number>22</number>
<sentence>p</sentence>
<justification>Reiteration</justification>
<antecedent>19</antecedent>
</step>
<step>
<number>23</number>
<sentence>~q => p</sentence>
<justification>Implication Introduction</justification>
<antecedent>21</antecedent>
<antecedent>22</antecedent>
</step>
<step>
<number>24</number>
<sentence>~q</sentence>
<justification>Assumption</justification>
</step>
<step>
<number>25</number>
<sentence>~p</sentence>
<justification>Reiteration</justification>
<antecedent>20</antecedent>
</step>
<step>
<number>26</number>
<sentence>~q => ~p</sentence>
<justification>Implication Introduction</justification>
<antecedent>24</antecedent>
<antecedent>25</antecedent>
</step>
<step>
<number>27</number>
<sentence>~~q</sentence>
<justification>Negation Introduction</justification>
<antecedent>23</antecedent>
<antecedent>26</antecedent>
</step>
<step>
<number>28</number>
<sentence>q</sentence>
<justification>Negation Elimination</justification>
<antecedent>27</antecedent>
</step>
<step>
<number>29</number>
<sentence>~p => q</sentence>
<justification>Implication Introduction</justification>
<antecedent>20</antecedent>
<antecedent>28</antecedent>
</step>
<step>
<number>30</number>
<sentence>q</sentence>
<justification>Assumption</justification>
</step>
<step>
<number>31</number>
<sentence>q => q</sentence>
<justification>Implication Introduction</justification>
<antecedent>30</antecedent>
<antecedent>30</antecedent>
</step>
<step>
<number>32</number>
<sentence>q</sentence>
<justification>Or Elimination</justification>
<antecedent>18</antecedent>
<antecedent>29</antecedent>
<antecedent>31</antecedent>
</step>
<step>
<number>33</number>
<sentence>p => q</sentence>
<justification>Implication Introduction</justification>
<antecedent>19</antecedent>
<antecedent>32</antecedent>
</step>
<step>
<number>34</number>
<sentence>~p | q => (p => q)</sentence>
<justification>Implication Introduction</justification>
<antecedent>18</antecedent>
<antecedent>33</antecedent>
</step>
<step>
<number>35</number>
<sentence>p => q <=> ~p | q</sentence>
<justification>Biconditional Introduction</justification>
<antecedent>17</antecedent>
<antecedent>34</antecedent>
</step>
</proof>