> > How do I prove the last one in session 4: (A∨(A→⊥)→⊥)→⊥ ? >> > > Heh... That one looks daunting for some reason. But fear not, search for > "Law of excluded middle implies double negation". Though, I was unable to > find a solution until I solved it myself with much swearing and sweating :( > Correcting myself from creating even more confusion: it should be actually vice versa - "Double negation elimination implies law of excluded middle".
-- You received this message because you are subscribed to the Google Groups "Metamath" group. To unsubscribe from this group and stop receiving emails from it, send an email to [email protected]. To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/1af22f82-1b14-4f71-8fbe-e1a8bb5cd896%40googlegroups.com.
