> 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)).
Of course ! Actually the current proof uses id, pm2.01 and mt2, which are all minimalistic. I should have checked it first ! Therefore, set.mm's df-bi would provide a definitional extension in iset.mm as well, but it would define the "classical equivalence", which is strictly weaker than the intuitionistic equivalence. Is that correct ? > 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 /\ ). iset.mm's df-bi does not use \/ and seems to be conservative over the axioms for ->, -. and /\ alone, without the axiom for \/ ax-io. Probably you mean in your first sentence the more general statement: *to achieve functional completeness*, you also need /\ and \/ ? 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/cad31bdc-837f-4bf3-96ee-70170d2ba0ea%40googlegroups.com.
