On Fri, 27 Dec 2019 11:37:24 -0800 (PST), Benoit <[email protected]> wrote: > Indeed, Jim is right, and I took the precaution of writing in my first > post: "widely considered as constructive, that is, intuitionistic and > predicative". You can see on its webpage that ~finds requires separation > and power sets.
Got it, thanks for the clarification. The Metamath 100 page at: http://us.metamath.org/mm_100.html#74 currently says: The intuitionistic logic explorer (iset.mm) database also includes <a href="http://us.metamath.org/ileuni/finds.html";>finds</a> and <a href="http://us.metamath.org/ileuni/findes.html";>findes</a>. I'd like to modify that text, but I want to get it right. How about this replacement?: The intuitionistic logic explorer (iset.mm) database includes <a href="http://us2.metamath.org/ileuni/bj-findis.html";>bj-findis</a>, the principle of induction (on the natural numbers), using Constructive Zermelo--Fraenkel (CZF) (an axiom system that is widely considered as constructive, that is, intuitionistic and predicative). The intuitionistic logic explorer (iset.mm) database also includes <a href="http://us.metamath.org/ileuni/finds.html";>finds</a> and <a href="http://us.metamath.org/ileuni/findes.html";>findes</a>, but these have additional requirements, e.g., <a href="http://us.metamath.org/ileuni/finds.html";>finds</a> requires separation and power sets. It's long, but this is a complicated subject that most people wouldn't even realize is complicated. Also, I'm hoping that bj-findis will get renamed eventually :-). --- 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/E1ikwh1-0006Hc-RH%40rmmprod07.runbox.
