On Mon, Mar 11, 2024 at 11:36 AM Jim Kingdon <[email protected]> wrote:
> If this is just a hypothetical question I guess we don't really need to > come up with a definitive answer, but I will say that if we want to keep > some of our other values (like preferring short proofs), we'd end up > with a lot of ALT theorems or other ways in which there is a classical > proof, there is an intuitionistic proof, and the intuitionistic proof is > much longer. We already have a caveat in the proof shortening rules for this. We want shorter proofs but *only* assuming it doesn't take the theorem out of a "subsystem of interest". For the most part that means that proof searches using MINIMIZE will add /NO_NEW_AXIOMS to ensure that intuitionistic proofs stay intuitionistic. So in the variation you are talking about I would expect there to only be an intuitionistic proof, and the classical proof (if the statement is different) would be the shorter of "do the proof directly" and "apply the intuitionistic version and remove the unnecessary assumptions", which probably would end up with the latter most of the time. > Proof length aside, I guess I'm just not sure that set.mm would read > very nicely if it needed to concern itself with decidability, apartness, > additional conditions on things like supremums and convergence, etc. Not > to mention topology which beyond a certain point falls apart unless you > switch from point-set topology to locales (or so I read, iset.mm hasn't > really gotten that far yet). > This is a fair criticism. For those areas like topology where it's still unclear how to intuitionize it, the whole thing would simply be classical. But I would expect a cover-to-cover reader of set.mm to already know that it is trying to simultaneously cover intuitionistic and classical logic, and the abstractions that work in intuitionistic logic are also interesting in their own way. I know I had to search far and wide for proofs about measure theory in the absence of the axiom of choice (thanks Fremlin!) so it wouldn't be the first time for proofs that go out of their way to avoid some axiom. > I'll also say that I do agree about the observations about how iset.mm > and set.mm are similar enough that it is also awkward, in different > ways, to keep them separate. There are a lot of theorems which can > simply be copy-pasted in one direction or the other. > And of course these copy-pasted theorems are a future maintenance issue, since people will have to remember to change them in tandem (or not! if the change needs classical logic) and this is hard to deal with without a global view of all the databases. -- 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/CAFXXJSt9UHdv%2BPAN0wYH-E%2BsN5XxQpmPTmS6DUUS9a5G%3DW7dew%40mail.gmail.com.
