On Tue, 28 May 2019 19:11:24 -0400, Mario Carneiro <[email protected]> wrote: > I think you are right - the appropriate intuitionistic version is F/2, > which is equivalent to F/1 so is least disruptive. But in set.mm, we're > being classical anyway so if the "naive" reading is simpler (always true or > always false) then that seems best.
In cases like this, where there's not a "really obviously winning definition", I'd prefer to use a definition that would also work in intuitionistic logic (iset.mm). That would make the iset.mm work a little easier, and there's also the argument that if it's still valid in intuitionistic logic (which is strictly weaker) then it's a definition that makes "fewer" assumptions. That would move this to F/2. I don't want to go too far with this idea, because there are lots of cases where that's too hard / not worth it. But if it's relatively painless, then using the definition that ports more easily seems reasonable. You can always prove the equivalence of one definition with another, as we've done in many other cases. --- David A. Wheeler -- 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/E1hVo40-0004ET-SA%40rmmprod07.runbox.
