Is the proof below correct for the following premise?: ⊤ ⊢ (B → ¬B) → ¬B
1 B → ~B :AS
2 B :AS
3 ~B : → E1,2
4 ⊥
5 ~B :~I1-4
6 --
7 (B->~B)-> ~B :->I1-4
-
Here is a natural deduction proof checker: proofs.openlogicproject.org – lemontree Oct 25 '20 at 20:51
-
You should cite the rule name and source lines for ⊥, and the source lines for your last -> should be 1-5; otherwise your proof looks fine -- well done! – lemontree Oct 25 '20 at 20:54
-
@lemontree thank you!! – Pri Oct 25 '20 at 20:56
