On Sun, Mar 8, 2020 at 9:18 PM Mario Carneiro <[email protected]> wrote:
> If you actually want intuitionistic logic, you cannot get away with using > just -> and -. as your basis. You have to add in /\ and \/ , but once you > have that, you can just use dfbi1 as the definition > correction: dfbi2 -- 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/CAFXXJStjeV-%2BfkRFECLWw%2BN91XU0RdqktTwezY6hKOXRkj2eHg%40mail.gmail.com.
