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

2023-09-12
Contact | Home | ITL home | Course | Proofs | Algebra | FL
© 1996-2023