Next
Prev
Up
NotBoxStateImpBoxYieldsNotBox
⊢
¬
w
⊃
(
w
)
¬
w
NotBoxStateImpBoxYieldsNotBox
Proof:
1
⊢
w
;
w
≡
w
BoxStateChopBoxEqvBox
2
⊢
w
≡¬¬
w
Prop
3
⊢
w
;
w
≡
w
;
¬¬
w
2
,
RightChopEqvChop
4
⊢ ¬
w
⊃¬
(
w
;
¬¬
w
)
1
,
3
,
Prop
5
⊢ ¬
w
⊃
(
w
)
¬
w
4
,
def. of
qed
Next
Prev
Up
2024-08-03
Contact
|
Home
|
ITL home
|
Course
|
Proofs
|
Algebra
|
FL
© 1996-2024