On 12/27/19 5:34 AM, Benoit 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 . . . Constructive Zermelo--Fraenkel (CZF)
Congratulations! CZF had always seemed out of reach for me, but Benoît has made it a reality. This is a significant effort, both in terms of the number of theorems to be proved, but also the ingenuity involved in encoding bounded formulas in metamath.
Here's to many more proofs from the 100 list (whether in ZFC, IZF, CZF, or whatever other systems people work with)!
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.
What keeps me coming back to metamath is the quality of the collaboration here. I never would have proved those theorems without help (especially at a few key points), and there is a long tail of other people who have also contributed. Even something as small as more consistent naming of a few theorems, or the right convenience theorems here and there, make this work much more doable and enjoyable.
-- 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/b00ee4ca-b646-c3c5-9332-c8cc7d898fe9%40panix.com.
