Hi all, 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. See also the comments of the bounded version ~bj-bdfindis. I still have to add the unbounded equivalents of ~bj-bdfindisg and ~bj-bdfindes, but these are straightforward reformulations of ~bj-findis. Note that they are all in closed form.
Of course, this theorem relies on many theorems first proved in set.mm and whose proofs carry through, mostly proved by Norman Megill, and many theorems of intuitionistic logic proved by Jim Kingdon. The implementation in Metamath of the axiom system CZF relies on the implementation of bounded formulas, which I carried out in collaboration with Mario Carneiro and Jim Kingdon. Benoît -- 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/c34a967c-60a0-4136-b2f4-a75f8f5e738f%40googlegroups.com.
