User:StarTower/Work/SandBox

From ProofWiki
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:

$p \implies q$
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 \mathcal I$ 1004, 1005 Test3
1006 1007 $p \implies q$ Rule of Simplification: $\land \mathcal E_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 \mathcal I$ 1022 – 1023 Assumption 1022 has been discharged
1024 1025 $p \implies q$ Double Negation Elimination: $\neg \neg \mathcal E$ 1026 Test8
1027 1028 $p \implies q$ Double Negation Introduction: $\neg \neg \mathcal I$ 1029 Test9
1030 1031 $p \implies q$ Biconditional Elimination: $\iff \mathcal E_1$ 1032 Test10
1033 1034 $p \implies q$ Biconditional Introduction: $\iff \mathcal I$ 1035, 1036 Test11

Assumptions 1068 and 1069 have been discharged

1037 1038 $\bot$ Principle of Non-Contradiction: $\neg \mathcal E$ 1039, 1040 Test12
1041 1042 $p \implies q$ Proof by Contradiction: $\neg \mathcal I$ 1043 – 1044 Assumption 1043 has been discharged
1045 1046 $p \implies q$ Rule of Explosion: $\bot \mathcal E$ 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$