|
|
Post by Eugene 2.0 on Dec 4, 2021 21:07:19 GMT
M13. ~□A ≡ ◊~A
Part I: ~□A→◊~A
1. □A→~~□A ppt N14
2. ~◊~A→~~□A Df (1)
3. (~◊~A→~~□A)→(~□A→◊~A) ppt N42
~□A→◊~A MP (2,3).
Part II: ◊~A→~□A
1. A→~~A ppt N14
2. □(A→~~A) □-intr
3. □(A→~~A)→(□A→□~~A) ppt M2
4. □A→□~~A MP (2,3)
5. (□A→□~~A)→(~□~~A→~□A) ppt N17
6. ~□~~A→~□A MP (4,5)
◊~A→~□A Df (6)
|
|
|
|
Post by Eugene 2.0 on Dec 4, 2021 21:07:41 GMT
M15. □(A→B)→(◊A→◊B)
1. □(A→B) assum.
2. ◊A assum.
3. A→B □-deletion (1)
4. ~□~A df(2)
5. (A→B)→(~B→~A) ppt, T17
6. ~B→~A MP(3,5)
7. □(~B→~A) □-introduction (6)
8. □(~B→~A)→(□~B→□~A) ppt, M2
9. □~B→□~A MP(7,8)
10. (□~B→□~A)→(~□~A→~□~B) ppt, T17
11. ~□~A→~□~B MP(9,10)
12. ~□~B MP(4,11)
◊B df(12)
|
|
|
|
Post by Eugene 2.0 on Dec 10, 2021 9:03:30 GMT
M16. ◊(A&B)→(◊A&◊B)
Part I: ◊(A&B)→◊A
1. ◊(A&B) assum.
2. (A&B)→A ppt, T7
3. □((A&B)→A) □-introduction (2)
4. □((A&B)→A)→(◊(A&B)→◊A) ppt, M15
5. ◊(A&B)→◊A MP (2,3)
◊A MP (1,4)
Part I: ◊(A&B)→◊B
1. ◊(A&B) assum.
2. (A&B)→B ppt, T8
3. □((A&B)→B) □-introduction (2)
4. □((A&B)→B)→(◊(A&B)→◊B) ppt, M15
5. ◊(A&B)→◊B MP (2,3)
◊B MP (1,4)
|
|
|
|
Post by Eugene 2.0 on Dec 13, 2021 14:36:13 GMT
M.17 ◊(AvB)↔(◊Av◊B)
Part I: ◊(AvB)→(◊Av◊B) we have to do a little trick for using a constructive method to prove[◊(AvB)→(~□~Av~□~B) df; ◊(AvB)→~(□~A&□~B) de Morgan]
1. ◊(AvB) assum.
2. ~□~(AvB) df (1)
3. □~A&□~B weak indirect proof
4. □~A &-elemination (3)
5. □~B &-elemination (3)
6. ~A □-deletion (4)
7. ~B □-deletion (5)
8. ~A&~B &-introduction (6,7)
9. ~A→(~B→~(AvB)) ppt, T27
10. □~(AvB) □-introduction (4,5,9)
11. ~◊(AvB)↔□~(AvB) ppt, M14
12. □~(AvB)→~◊(AvB) →-elimination (11)
13. ~◊(AvB) MP (10,12)
Contradiction: 1, 13.
Part IIa: ◊A→◊(AvB)
1. ◊A assum.
2. A→(AvB) ppt, T10
3. □(A→(AvB)) □-introduction (2)
4. □(A→(AvB))→(◊A→◊(AvB)) ppt, M15
5. ◊A→◊(AvB) MP (3,4)
◊(AvB) MP (1,5)
Part IIb: ◊B→◊(AvB)
1. ◊B assum.
2. B→(AvB) ppt, T11
3. □(B→(AvB)) □-introduction (2)
4. □(B→(AvB))→(◊B→◊(AvB)) ppt, M15
5. ◊B→◊(AvB) MP (3,4)
◊(AvB) MP (1,5)
|
|
|
|
Post by Eugene 2.0 on Dec 14, 2021 15:40:02 GMT
M.18 ◊(A→B)→(□A→◊B)
1. ◊(AvB) assum.
2. □A assum.
3. (A→B)≡(~AvB) ppt, T50
4. (A→B)→(~AvB) →-eliminaton (3)
5. □((A→B)→(~AvB)) □-elimination (4)
6. □((A→B)→(~AvB))→(◊(A→B)→◊(~AvB)) ppt, M15
7. ◊(A→B)→◊(~AvB) MP (5,6)
8. ◊(~AvB) MP (1,7)
9. ◊(~AvB)≡(◊~Av◊B) ppt, M17
10. ◊(~AvB)→(◊~Av◊B) →-elimination (9)
11. ◊~Av◊B MP (8,10)
12. (◊~Av◊B)→(~◊~A→◊B) ppt, T35
13. ~◊~A→◊B MP (11,12)
14. ~◊~A df (2)
◊B MP (14,13)
|
|
|
|
Post by Eugene 2.0 on Dec 14, 2021 15:53:11 GMT
M21. ◊A≡◊◊A
Part I: ◊A→◊◊A
◊A→◊◊A ppt, M7
Part II: ◊◊A→◊A [doint a trick: ◊◊A→~□~A]
1. ◊◊A assum.
2. □~A weak ind. proof
3. □□~A ppt, M`axiom
4. ◊~□~A df(1)
5. ~◊~□~A df(3)
Contradiction: 4,5.
|
|
|
|
Post by Eugene 2.0 on Dec 17, 2021 14:00:23 GMT
M22. (□Av□B)≡□(□Av□B)
Part Ia: □A→□(□Av□B)
1. □A assum.
2. □□A M1 axiom 1
3. □A→(□Av□B) ppt, T10
4. □Av□B MP (1,3)
□(□Av□B) □-introduction (4)
Part Ib: □B→□(□Av□B)
1. □B assum.
2. □□B M1 axiom 1
3. □B→(□Av□B) ppt, T11
4. □Av□B MP (1,3)
□(□Av□B) □-introduction (4)
Part II: □(□Av□B)→(□Av□B)
1. □(□Av□B) assum.
□Av□B □-deleting (1)
|
|
|
|
Post by Eugene 2.0 on Dec 17, 2021 14:02:26 GMT
M23. (□A∧□B)≡□(□A∧□B)
Part I: (□A∧□B)→□(□A∧□B)
1. □A∧□B assum.
2. □A ∧-deletion (1)
3. □B ∧-deletion (1)
4. A □-deletion (2)
5. B □-deletion (3)
6. A→(B→(A∧B)) ppt, T6
7. □(A∧B) □-introduction (2,3,6)
8. □□(A∧B) M1 axiom 1 (7)
9. □(A∧B)≡(□A∧□B) ppt, M3
10. □(A∧B)→(□A∧□B) →-elimination (9)
11. □A∧□B MP (7, 10)
□(□A∧□B) □-introduction (8,10)
Part IIa: □(□A∧□B)→□A
1. □(□A∧□B) assum.
2. □A∧□B □-deletion (1)
□A ∧-elimination (2)
Part IIb: □(□A∧□B)→□B
1. □(□A∧□B) assum.
2. □A∧□B □-deletion (1)
□B ∧-elimination (2)
|
|
