 |
The Game of Modern Logic By Layman E. Allen Professor of Law and Senior Research Scientist, University of Michigan |
|
|
The Game of Modern Logic By Layman E. Allen Professor of Law and Senior Research Scientist, University of Michigan |
18 Basic Derived Rules of WFF
'N PROOF
(In Alphabetic Order)
| AoAi: Avw --** Awv 10 | AoCi: Avw --**
CNvw 6
ANvw --** Cvw |
|
| AoNKi: Avw --** NKNvNw
12
ANvw --** NKvNw AvNw --** NKNvw ANvNw --** NKvw |
AoNo: Avw, Nv --** w
7
Avw, Nw --** v ANvw, v --** w AvNw, w --** v |
|
| CoAi: Cvw --** ANvw
9
CNvw --** Avw |
CoCi: Cvw --** CNwNv
13
CNvw --** CNwv CvNw --** CwNv CNvNw --** Cwv |
|
| CoNKi: Cvw --** NKvNw
11
CvNw --** NKvw |
CoNo: Cvw, Nw -- ** Nv 5
CNvw, Nw --** v |
|
| KoKi: Kpq --** Kqp 4 | KoNAi: Kvw --** NANvNw
14
KNvw --** NAvNw KvNw --** NANvw KNvNw --** NAvw |
|
| KoNCi: Kvw --** NCvNw
15
KvNw --** NCvw |
NAoKi: NAvw --** KNvNw
8
NANvw --** KvNw NavNw --** KNvw NANvNw --** Kvw |
|
| NCoKi: NCvw -- ** KvNw
16
NCvNw --** Kvw |
NKoAi: NKvw --** ANvNw
18
NKNvw --** AvNw NKvNw --** ANvw NKNvNw --** Avw |
|
| NKoCi: NKvw --** CvNw
17
NKvNw --** Cvw |
NNi: w --** NNw 3 | |
| NNo: NNw --** w 2 | Rp: w --** w 1 |
PROOFS
(In Numerical Order of Proof)
NOTE: Once a rule has been proved,
it can be used in later proofs.
| Rp: w --** w 1 | NNo: NNw --** w 2 | |
| 1|_ p
s
2| a|_ p s 2| b| p 1R 3| Cpp 2,Ci 4| p 3,1,Co |
1|_NNp
s
2| a|_Np s 2| b| Np a,Rp 2| c| NNp 1R 3| p 2,No |
| NNi: w --** NNw 3 | KoKi: Kpq --** Kqp 4 | |
| 1|_
p s
2| a|_ Np s 2| b| p 1R 2| c| Np a,Rp 3| NNp 2,Ni |
1|_Kpq s
2| p 1,Ko 3| q 1,Ko 4| Kqp 3,2,Ki |
| CoNo: Cvw, Nw -- ** Nv
5
CNvw, Nw --** v |
AoCi: Avw --** CNvw
6
ANvw --** Cvw |
|
|
1| Cpq
s
2|_Nq s 3| a|_ p s 3| b| q 1R,a,Co 3| c| Nq 2R 4| Np 3,Ni |
1|_ Apq
s
2| a|_ Np s 2| b| 1|_ p s 2| b| 2| a|_Nq s 2| b| 2| b| p 1R 2| b| 2| c| Np aRR 2| b| 3| q 2,No | | 2| c| 1|_ q s 2| c| 2| q 1,Rp 2| d| q 1R,b,c,Ao 3| CNpq 2,Ci |
| AoNo: Avw, Nv --** w
7
Avw, Nw --** v ANvw, v --** w AvNw, w --** v |
NAoKi: NAvw --**
KNvNw 8
NANvw --** KvNw NavNw --** KNvw NANvNw --** Kvw |
|
|
1| Apq
s
2|_Np s 3| CNpq 1,AoCi 4| q 3,2,Co
|
1|_ NApq
s
2| a|_ p s 2| b| Apq a,Ai 2| c| NApq 1R | 3| a|_ q s 3| b| Apq a,Ai 3| c| NApq 1R 4| Np 2,Ni 5| Nq 3,Ni 6| KNpNq 4,5,Ki |
| CoAi: Cvw --** ANvw
9
CNvw --** Avw |
AoAi: Avw --** Awv 10 | |
| 1|_
Cpq s
2| a|_NANpq s 2| b| KpNq a,NAoKi 2| c| p b,Ko 2| d| q 1R,c,Co 2| e| Nq b,Ko 3| ANpq 2,No |
1|_ Apq
s
2| a|_p s 2| b| Aqp a,Ai | 3| a|_q s 3| b| Aqp a,Ai 4| Aqp 1,2,3,Ao |
| CoNKi: Cvw --**
NKvNw 11
CvNw --** NKvw |
AoNKi:
Avw --** NKNvNw 12
ANvw --** NKvNw AvNw --** NKNvw ANvNw --** NKvw |
|
| 1|_ Cpq
s
2| a|_KpNq s 2| b| p a,Ko 2| c| q 1R,b,Co 2| d| Nq a,Ko 3| NKpNw 2,Ni |
1|_Apq
s
2| CNpq 1,AoCi 3| NKNpNq 2,CoNKi |
| CoCi: Cvw --**
CNwNv 13
CNvw --** CNwv CvNw --** CwNv CNvNw --** Cwv |
KoNAi: Kvw --**
NANvNw 14
KNvw --** NAvNw KvNw --** NANvw KNvNw --** NAvw |
|
| 1|_ Cpq
s
2| a|_ Nq s 2| b| 1|_ p s 2| b| 2| q 1RR,1,Co 2| b| 3| Nq 1R 2| c| Np b,Ni 3| CNqNp 2,Ci |
1|_Kpq
s
2| a|_ ANpNq s 2| b| CpNq a,AoCi 2| c| p 1R,Ko 2| d| q 1R,Ko 2| e| Nq b,c,Co 3| NANpNq 2,Ni |
| KoNCi: Kvw --**
NCvNw 15
KvNw --** NCvw |
NCoKi: NCvw -- **
KvNw 16
NCvNw --** Kvw |
|
|
1|_ Kpq
s
2| a|_ CpNq s 2| b| p 1R,Ko 2| c| q 1R,Ko 2| d| Nq a,b,Co 3| NCpNq 2,Ni
|
1|_ NCpq
s
2| a|_ Np s 2| b| 1|_ p s 2| b| 2| a|_Nq s 2| b| 2| b| p 1R 2| b| 2| c| Np aRR 2| b| 3| q 2,No 2| c| Cpq b,Ci 2| d| NCpq 1R | 3| a|_ q s 3| b| 1|_ p s 3| b| 2| q aR 3| c| Cpq b,Ci 3| d| NCpq 1R 4| p 2,No 5| Nq 3,Ni 6| KpNq 4,5,Ki |
| NKoCi: NKvw --**
CvNw 17
NKvNw --** Cvw |
NKoAi: NKvw --**
ANvNw 18
NKNvw --** AvNw NKvNw --** ANvw NKNvNw --** Avw |
|
| 1|_ NKpq
s
2| a|_ p s 2| b| 1|_q s 2| b| 2| Kpq aR,1,Ki 2| b| 3| NKpq 1RR 2| c| Nq b,Ni 3| CpNq 2,Ci |
1|_NKpq
s
2| CpNq 1,NKoCi 3| ANpNq 3,CoAi |
| If you notice any typographic errors or have any other
suggestions for improving this web page, please notify me at the email
address:
|