Sidenote: since bijust is a negation, it is provable from ax-mp, ax-1, ax-2, Peirce, and the minimalistic contraposition ( ( ph -> -. ps ) -> ( ps -> -. ph ) ). This system is strictly weaker than classical propositional calculus, and is called "classical refutability". So df-bi provides a definitional extension in this weaker system.
By contrast, bijust is (probably) not intuitionistic (one could try to find a counterexample using open subsets of \R, for instance, but this looks tedious; maybe Mario or Jim know a faster method), and this explains why df-bi is different in iset.mm. Benoît -- 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/8bff49a5-66ea-4598-a0be-a156dcb02e32%40googlegroups.com.
