On 3/11/24 04:32, Mario Carneiro wrote:
Given a free choice I think that developing in the same database is better since then intuitionistic proofs can be used in classical theorems (and vice versa, when the classical theorem was not actually using classical logic on accident or because of a refactor).
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. The examples which come to mind are summation (where the iset.mm DEFINITION has a decidability condition and other changes), the recursion theorem, and Bézout's theorem, but there probably are others. Note that because these are foundational results which a lot of other things build on, if you want the list of axioms used to be informative, you need the main proof to be the longer intuitionistic one.
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).
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.
-- 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/8ebce18e-16b4-4b3b-8480-c5262be28f5a%40panix.com.
