First constructive Metamath proof of a "100" theorem

[Benoit]

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

[Jim Kingdon]

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.

[David A. Wheeler]

On Fri, 27 Dec 2019 05:34:11 -0800 (PST), Benoit <benoit...@gmail.com> 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 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

I'm glad to see your proof, but we already have constructive (iset.mm)
proofs for the Principle of Mathematical Induction, Metamath 100 #74, listed here:
http://us.metamath.org/mm_100.html#74

Specifically we already list these for #74 in the intuitionistic logic explorer:
* finds : http://us.metamath.org/ileuni/finds.html
* findes: http://us.metamath.org/ileuni/findes.html

So I'm not sure you can claim "first", but you can certainly count *more*.
I'd be happy to add this to that collection of proofs of mathematical induction;
this particular theorem can be stated in a variety of ways, and it makes sense to
point to multiple proofs.

Also: I recommend that *not* using special name prefixes like "bj-..."
in mathboxes. Having special name prefixes makes it harder to move theorems
from mathboxes into the main body later. Not everything gets moved, and obviously
renaming is possible, but I want to make moving theorems relatively *easy* or we
risk never getting around to it. If you're worried about collisions, longer & clearer
names are (in my opinion) the better way.

--- David A. Wheeler

[Jim Kingdon]

The term "constructive", unfortunately, can be defined various ways. Oftentimes it is better to say "without excluded middle" or "predicative" or other such wordings (although predicative too has multiple definitions).

In this case, it is about IZF versus CZF. Induction for the former was added to iset.mm a while ago. CZF is newer to iset.mm and is in BJ's mathbox, and just now got induction.

And yes, if you are having a reaction of "wait, there's not just one kind of mathematics without excluded middle?" this is discussed in the "Depression" section of the [Bauer] paper which we cite in mmil.html.

[Benoit]

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.

Benoît

[David A. Wheeler]

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

[Benoit]

Thanks David.  I think there is no hurry in updating the mm100 page (although your proposal sounds good).  I would like to clean up some things first and I am away from my main computer this week.  As for your remark about labeling, I am starting a new topic.  It is true that it would be strange to mention "bj-findis" on the mm_100 page, since this looks like a temporary label.

Benoît

[Jim Kingdon]

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.