On Mon, Mar 9, 2020, 1:17 PM Benoit <[email protected]> wrote: > > 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 ? >
Not quite. It is easy to see that classical equivalence is not equivalent to intuitionistic equivalence, for example (p <-> T.) is equivalent to p but (p <->c T.) is equivalent to -. -. p. But for this very reason, because df-bi shows only the classical equivalence of the newly defined notion to classical equivalence, it is not a definitional extension. I will show that df-bi is *also* provable if we interpret the new connective as intuitionistic equivalence! That is, ((p <-> q) <->c (p <->c q)) is provable in iset.mm. It is not hard to show that (p <-> q) -> (p <->c q), so the goal reduces to -. -. ((p <->c q) -> (p <-> q)). Using the lemma (a -> -. -. b) -> -. -. (a -> b) this reduces to ((p <->c q) -> -. -. (p <-> q)) which is easy: unfolding the definition of <->c and applying contraposition it becomes (-. (p <-> q) -> ((p -> q) -> -. (q -> p))), and after com12 and contraposition again becomes ((p -> q) -> ((q -> p) -> (p <-> q))) which is part of the definition of intuitionistic equivalence. The lemma is not true in mimimal logic (or at least, the proof I will give makes essential use of ex falso). Suppose (1) (a -> -. -. b) and (2) -. (a -> b), we want to prove false. Applying (2) we have to show (a -> b) so suppose (3) a as well, we have to show b. By (1) and (3) we have -. -. b, and by (2) and (3) we have -. b, so false, so b by ex falso. > 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 \/ ? > Yes, that's what I meant. I'm mostly hedging because I don't usually consider "random subsets" of the logic by just cutting off certain axioms or connectives; I have decent intuitions for intuitionistic and minimal logic but for other subsets it becomes more delicate and I would have to work it out formally to say for sure. Mario -- 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/CAFXXJSvOEEGtQjZm2jkrfwpAZXb4i%3DSvGv7KYdKp4T380JxWdQ%40mail.gmail.com.
