That wording is fine with me.
I could imagine different ways to revise this further down the road
(using, I suppose, the treatment of Choice and Tarski-Grothendieck in
set.mm as the guide), but there would be no harm in putting in this text
for now.
On December 27, 2019 12:58:43 PM PST, "David A. Wheeler"
<[email protected]> wrote:
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/c4b5581d-6972-d83e-528b-ceb17bbc6bfa%40panix.com.
