2026-09-22 20:52 UTC
@soaproot@sfba.social There are two cursed variants of IZF that show up around these problems: IZF w/ Replacement instead of Collection, and negative IZF (IZF w/ Separation for double negated formulas and Power Set for elements with stable membership).
Replies (1)
-
@soaproot@sfba.social 2026-09-22 21:28
@zwarich@hachyderm.io I dutifully defined collection[1] because I was supposed to, but nine years in we have only used it to prove replacement [2], so I guess this matters but not for anything we have done yet in the Intuitionistic Logic Explorer. [1] https://us.metamath.org/ileuni/ax-coll.html [2] https://us.metamath.org/ileuni/repizf.html