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 (and df-bi is really just an obfuscated version of dfbi2 anyway, once you unfold the definition of /\ ).
Regarding provability of bijust, it is intuitionistically provable with the standard intuitionistic interpretations of -> and -. . It is an instance of -. ((p -> p) -> -. (p -> p)), which is true because |- p -> p is provable, and so from ((p -> p) -> -. (p -> p)) you can conclude -. (p -> p) and from there, falsity, so -. ((p -> p) -> -. (p -> p)). On Sun, Mar 8, 2020 at 10:07 AM Benoit <[email protected]> wrote: > 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 > <https://groups.google.com/d/msgid/metamath/8bff49a5-66ea-4598-a0be-a156dcb02e32%40googlegroups.com?utm_medium=email&utm_source=footer> > . > -- 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/CAFXXJSvE3FNE4nYFiPP0EwTRu8mZGr-LhipBB5WeKeDxM0jykA%40mail.gmail.com.
