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.
