User:StarTower/Work/SandBox
Jump to navigation
Jump to search
About
A sand box.
This (and that's a big this) doesn't work.
Sand Castles
By the tableau method of natural deduction:
| Line | Pool | Formula | Rule | Depends upon | Notes | |
|---|---|---|---|---|---|---|
| 1000 | 1000 | $p \implies q$ | Premise | (None) | Test1 | |
| 1001 | 1001 | $p \implies q$ | Assumption | (None) | Test2 | |
| 1002 | 1003 | $p \implies q$ | Rule of Conjunction: $\land \II$ | 1004, 1005 | Test3 | |
| 1006 | 1007 | $p \implies q$ | Rule of Simplification: $\land \EE_1$ | 1008 | Test4 | |
| 1009 | 1010 | $p \implies q$ | Rule of Addition: $\lor \II_1$ | 1011 | Test5 | |
| 1012 | 1013 | $p \implies q$ | Proof by Cases: $\text{PBC}$ | 1, 2 – 3, 4 – 5 | Assumptions 2 and 4 have been discharged | |
| 1014 | 1015 | $p \implies q$ | Modus Ponendo Ponens: $\implies \mathcal E$ | 7, 8 | Test6 | |
| 1016 | 1017 | $p \implies q$ | Modus Tollendo Ponens $\mathrm {MTP}_1$ | 7, 8 | ||
| 1018 | 1019 | $p \implies q$ | Modus Tollendo Tollens (MTT) | 7, 8 | Test7 | |
| 1020 | 1021 | $p \implies q$ | Rule of Implication: $\implies \II$ | 1022 – 1023 | Assumption 1022 has been discharged | |
| 1024 | 1025 | $p \implies q$ | Double Negation Elimination: $\neg \neg \EE$ | 1026 | Test8 | |
| 1027 | 1028 | $p \implies q$ | Double Negation Introduction: $\neg \neg \II$ | 1029 | Test9 | |
| 1030 | 1031 | $p \implies q$ | Biconditional Elimination: $\iff \EE_1$ | 1032 | Test10 | |
| 1033 | 1034 | $p \implies q$ | Biconditional Introduction: $\iff \II$ | 1035, 1036 | Test11
Assumptions 1068 and 1069 have been discharged | |
| 1037 | 1038 | $\bot$ | Principle of Non-Contradiction: $\neg \EE$ | 1039, 1040 | Test12 | |
| 1041 | 1042 | $p \implies q$ | Proof by Contradiction: $\neg \II$ | 1043 – 1044 | Assumption 1043 has been discharged | |
| 1045 | 1046 | $p \implies q$ | Rule of Explosion: $\bot \EE$ | 1047 | Test13 | |
| 1047 | $p \implies q$ | Law of Excluded Middle | (None) | Test14 | ||
| 1048 | 1049 | $p \implies q$ | Reductio ad Absurdum | 999 – 998 | Assumption 999 has been discharged | |
| 1050 | 1051 | $p \implies q$ | Sequent Introduction | 1052 | Disjunction is Commutative | |
| 1053 | 1054 | $p \implies q$ | Sequent Introduction | 1055 | De Morgan's Laws: Disjunction | |
| 1056 | 1057 | $p \implies q$ | Sequent Introduction | 1058 | Rule of Idempotence: Disjunction | |
| 1059 | 1060 | $p \implies q$ | Law of Identity | 1068 | Test15 | |
| 1061 | 1062 | $p \implies q$ | Sequent Introduction | 1063 | Test16 | |
| 1064 | $p \implies q$ | Theorem Introduction | (None) | Test17 | ||
| 1065 | 1066 | $p \implies q$ | Substitution | 1067 | $r \ / \ s$ |