> That is, ((p <-> q) <->c (p <->c q)) is provable in iset.mm. > [...] Using the lemma (a -> -. -. b) -> -. -. (a -> b)
Thanks. So these two statements are intuitionistic. They also hold in classical-refutability logic (simply because they are classical tautologies which remain classical tautologies when all negations (hence also <->c) are interpreted as true). But if I interpreted the article cited below correctly, the lemma, hence the first statement (since it implies the lemma in minimal logic, if I made no mistake) are NOT minimalistic. So to summarize, they hold in minimal logic plus ex-falso (intuitionistic logic) and in minimal logic plus Peirce (classical-refutability logic), but do not hold in minimal logic. The paper is Hannes Diener and Maarten McKubre-Jordens,Classifying Material Implications over Minimal Logic, arXiv:1606.08092 where your lemma is proved to be equivalent over minimal logic to what they call the "weak Tarski formula" ( -. p -> -. -. ( p -> q ) ) which is proved to be not minimalistic by using a Kripke model. 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/8787206d-fb34-429e-87b4-5634c04eae9c%40googlegroups.com.
