I am pleased to report the successful completion of the project to
formalize the equinumerosity of the rationals and the natural numbers in
iset.mm.[1] This project was begun in earnest in May 2022 with the
opening of a github issue[2] which quickly led to discussions and
partial results followed by steady progress leading to this result.
Some of the results along the way included:
* realizing that decomposing a natural number into a power of two and an
odd divisor could be an important part of the proof,[3]
* defining omniscient set notation and theorems
* defining disjoint union notation and theorems
* two impossibility proofs about the Schroeder-Bernstein theorem, the
full theorem (formalizing a 2019 paper) and a special case (we have an
impossibility proof of the special case but just how strong it is
appears to be an open problem[4]),
* a variety of theorems about countable sets ( for example [5]), and
* an example of a novel way (novel as far as I noticed, anyway) to use
the seq notation to define a family of functions both in terms of the
previous member of the family and the index within the collection[6]
Many thanks to everyone who collaborated on this, especially Mario
Carneiro, Thierry Arnoux, and Benoit Jubin (and probably others I'm
forgetting to mention). I never could have done something like this by
myself.
I'd also like to make a special acknowledgement to Peter Aczel[7] who
with a coauthor wrote the textbook which contained the key lemma for
this proof[8]. He died on August 1, 2023 and was a great mathematician
and person according to all the tributes I read on Mastodon from people
who had worked with him.
[1] https://us.metamath.org/ileuni/qnnen.html
[2] https://github.com/metamath/set.mm/issues/2595
[3] https://us.metamath.org/ileuni/oddpwdc.html
[4]
https://mathoverflow.net/questions/451785/how-strong-is-the-schr%c3%b6der-bernstein-theorem-where-one-set-is-the-natural-number
[5] https://us.metamath.org/ileuni/ctm.html
[6] https://us.metamath.org/ileuni/ennnfonelemen.html and other lemmas
using the hypotheses here
[7] https://en.wikipedia.org/wiki/Peter_Aczel
[8] https://us.metamath.org/ileuni/ennnfone.html , Corollary 8.1.13 in
the cited textbook
--
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/49b8898a-690c-6aeb-af03-b03b6346ab44%40panix.com.
