The term "constructive", unfortunately, can be defined various ways. Oftentimes it is better to say "without excluded middle" or "predicative" or other such wordings (although predicative too has multiple definitions).
In this case, it is about IZF versus CZF. Induction for the former was added to iset.mm a while ago. CZF is newer to iset.mm and is in BJ's mathbox, and just now got induction. And yes, if you are having a reaction of "wait, there's not just one kind of mathematics without excluded middle?" this is discussed in the "Depression" section of the [Bauer] paper which we cite in mmil.html. On December 27, 2019 9:36:24 AM PST, "David A. Wheeler" <[email protected]> wrote: >On Fri, 27 Dec 2019 05:34:11 -0800 (PST), Benoit ><[email protected]> wrote: >> I recently added to iset.mm the first (to my knowledge) constructive >> Metamath proof of a theorem from the "100" list. More precisely, a >> Metamath proof from an axiom system widely considered as >constructive, that >> is, intuitionistic and predicative. The axiom system is Constructive > >> Zermelo--Fraenkel (CZF) and the theorem is the principle of induction >(on >> the natural numbers), see >http://us2.metamath.org/ileuni/bj-findis.html > >I'm glad to see your proof, but we already have constructive (iset.mm) >proofs for the Principle of Mathematical Induction, Metamath 100 #74, >listed here: > http://us.metamath.org/mm_100.html#74 > >Specifically we already list these for #74 in the intuitionistic logic >explorer: >* finds : http://us.metamath.org/ileuni/finds.html >* findes: http://us.metamath.org/ileuni/findes.html > >So I'm not sure you can claim "first", but you can certainly count >*more*. >I'd be happy to add this to that collection of proofs of mathematical >induction; >this particular theorem can be stated in a variety of ways, and it >makes sense to >point to multiple proofs. > >Also: I recommend that *not* using special name prefixes like "bj-..." >in mathboxes. Having special name prefixes makes it harder to move >theorems >from mathboxes into the main body later. Not everything gets moved, and >obviously >renaming is possible, but I want to make moving theorems relatively >*easy* or we >risk never getting around to it. If you're worried about collisions, >longer & clearer >names are (in my opinion) the better way. > >--- 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/E1iktXE-0006f9-Lf%40rmmprod07.runbox. -- 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/50B9AFB5-9B8E-4FF4-B8C3-BC44CA711E71%40panix.com.
