Additional Metamath 100 proof in iset.mm: Bézout's identity

[Jim Kingdon]

For those who have been keeping score, set.mm is up to 74 theorems from
the Metamath 100 list.

iset.mm on the other hand has been stuck at one (which is induction over
natural numbers) for some time (despite much progress in constructing
real numbers, sequence convergence, existence of square roots, and other
topics, they didn't hit Metamath 100 theorems).

I am pleased to report that we can now report that we have a second
Metamath 100 theorem in iset.mm. This is "bezout" which is stated as in
http://us.metamath.org/mpeuni/bezout.html but proved using a
constructive proof (we cannot just assert the existence of an infimum of
nonnegative integers; instead we apply the Extended Euclidean Algorithm
to compute the greatest common divisor and also show that it satisfies
the Bézout property). For more details I suppose the informal proof at
https://github.com/metamath/set.mm/issues/2399 is probably the most
readable place to start (although the proof there is spread over several
comments and not quite written out with consistent notation and dead
ends removed), or browse through bezout and all its lemmas in iset.mm.

Although I did the mmj2 formalization, I want to also acknowledge Mario
Carneiro's essential contributions to this effort. I was very much
stumbling through "how do you even turn the Extended Euclidean Algorithm
into metamath proofs?" when his informal (but detailed) proofs paved the
way for a much simpler and clearer approach than anything I might have
eventually come up with. Most of his proofs in the github issue linked
above translated pretty directly into the formalization which was just
merged.

What's next? My own plan is to continue formalizing number theory
(working towards https://github.com/metamath/set.mm/issues/2298 -
another Metamath 100 theorem) (well or summation -
https://github.com/metamath/set.mm/issues/2167 - if I ever get back to
that). But other contributions are welcome! We've already seen some
great CZF work from Benoit and a few contributions from others, so
please do send in proofs, or open an issue or otherwise get in touch if
you want advice or help. iset.mm has gotten to the point where it is
both a treatment of how logic and set theory are affected by the absence
of excluded middle, but also covers other topics like complex numbers,
square roots, and absolute value, including issues which are different
without excluded middle such as sequence convergence, apartness, or
supremums. So there's plenty to work on if you don't want to have to
start from the beginning.

[Benoit]

Even though I already reacted on github, I'll extend my congratulations to Jim here, and also to Mario for the informal proof.  As important as Bézout's identity is the extended Euclidean algorithm, and having formalized it completely constructively is an achievement.  I hope you'll update the Metamath 100 page.  I think one can say without too much of a stretch that the proof is in Heyting arithmetic (Peano's axioms do not appear as axioms in iset.mm, but if one traces back your proofs, one can probably convince oneself that this is the case) so there are no questions about its constructive nature (I mean: there is no issue about predicativity or IZF versus CZF).

Benoît

[Jim Kingdon]

On January 11, 2022 8:11:02 AM PST, Benoit <benoit...@gmail.com> wrote:
> I think one can say without too much of a
>stretch that the proof is in Heyting arithmetic (Peano's axioms do not
>appear as axioms in iset.mm, but if one traces back your proofs, one can
>probably convince oneself that this is the case) so there are no questions
>about its constructive nature (I mean: there is no issue about
>predicativity or IZF versus CZF).

Hmm my assumption is that this sort of proof works in CZF or Heyting
arithmetic but I'm not sure that the iset.mm proof convinces us of that.
If you look at the "This theorem was proved from axioms" list at the
bottom of the page for bezout you see ax-caucvg and I assume that's not
because ax-caucvg is needed to prove results about integers, but because
we somehow drag in absolute value or something else (and I think if we
wanted to avoid it we probably could prove some absolute value theorems
for rationals without ax-caucvg).

If people are interested in this sort of thing, there's definitely work
that can be done in iset.mm similar to the work that has been done in
the past for set.mm - reducing the use of axioms where not needed. I'm
not exactly the expert on what axioms are needed for what, much less
what would be needed to make iset.mm more realistically cover systems
smaller than IZF (whether CZF - outside the section where it currently
lives in iset.mm - or the various systems of second-order arithmetic or
even first-order arithmetic). So some of this would probably be best
done by totally restating some of the axioms (or even switching away
from something built on propositional and predicate logic and sets, as
iset.mm is), but I'm being quite vague about "some of this" simply
because I don't know.

[Benoit]

Hmm my assumption is that this sort of proof works in CZF or Heyting
arithmetic but I'm not sure that the iset.mm proof convinces us of that.
If you look at the "This theorem was proved from axioms" list at the
bottom of the page for bezout you see ax-caucvg and I assume that's not
because ax-caucvg is needed to prove results about integers, but because
we somehow drag in absolute value or something else (and I think if we
wanted to avoid it we probably could prove some absolute value theorems
for rationals without ax-caucvg).

I wasn't clear but that's what I meant.  We have no formal proof in Heyting arithmetic, but since the logic is intuitionistic, we have to trace back the use of only a few axioms and "see" that they are "artefacts" of earlier contructions which are more general than needed for the present purposes.  It'll be easier when the website is updated (I guess the page you're talking about was locally generated on your computer, since I can't access http://us2.metamath.org/ileuni/bezout.html ?).

If people are interested in this sort of thing, there's definitely work
that can be done in iset.mm similar to the work that has been done in
the past for set.mm - reducing the use of axioms where not needed. I'm
not exactly the expert on what axioms are needed for what, much less
what would be needed to make iset.mm more realistically cover systems
smaller than IZF (whether CZF - outside the section where it currently
lives in iset.mm - or the various systems of second-order arithmetic or
even first-order arithmetic). So some of this would probably be best
done by totally restating some of the axioms (or even switching away
from something built on propositional and predicate logic and sets, as
iset.mm is), but I'm being quite vague about "some of this" simply
because I don't know.

Yes, there is some work to do toward modularity of databases.  With Norm's addition of the command WRITE SOURCE <file> /SPLIT, and provided we have the good tags in iset.mm, we can produce a file ifol.mm that can then be included by $[ ifol.mm $] at the beginning of other databases.  On top of that, one can state for instance Peano's axioms, or Tarski's axioms of elementary geometry, etc.  (One caveat is that we will want a logic with terms, which are not provided anymore since there are no class terms, so we'll need to strengthen the "denotation axiom" E. x x = y to E. x x = A, but this can be added as an intermediate layer ifol-terms.mm which includes ifol.mm).

Benoît

[Jim Kingdon]

On 1/11/22 1:22 PM, Benoit wrote:

It'll be easier when the website is updated (I guess the page you're talking about was locally generated on your computer, since I can't access http://us2.metamath.org/ileuni/bezout.html ?).

Yeah, I ran SHOW STATEMENT bezout/ALT_HTML from within metamath.exe which created the file bezout.html.

I think maybe sometime in the distant past I downloaded some files (fonts or whatever it was) which were needed (either to generate this file, or display it nicely in the browser), but hopefully it is relatively clear where to find those on metamath.org because I don't really remember what I did (and I only had to do that part once).