Although it has long been known that the Schroeder-Bernstein theorem (
https://us.metamath.org/mpeuni/sbth.html in set.mm) is not provable in
set theories such as IZF, it is only in the last decade or less that it
has been known that Schroeder-Bernstein is equivalent to excluded middle
(rather than a lesser principle such as the Lesser Principle of
Omniscience or one of the others). I am pleased to report that this
proof is now formalized in iset.mm as
https://us.metamath.org/ileuni/exmidsbth.html . This is the sixth
Metamath 100 problem to be formalized in iset.mm (as noted in
https://us.metamath.org/mm_100.html the current proof constitutes a
negative answer, for iset.mm, to the posed problem of Schroeder-Bernstein).
Incidentally, this result is one which was first proved in a formal
proof system[1] (by Pierre Pradic, and separately by Martin Escardó[2])
and only later informalized and published in a paper in 2019 -
https://arxiv.org/abs/1904.09193 . So metamath isn't doing badly to
prove this only three years after it was published, but these other
proof systems proved it before it even was published.
I didn't do this alone - in particular I'd like to thank Mario Carneiro
and Benoit Jubin for help in formalizing, especially for NN+oo and the
disjoint union notation/theorems that exmidsbth relies on.
[1] Pierre Pradic, personal communication
[2] https://cs-web.swan.ac.uk/~pierrepradic/cb-coq.tar.gz and
https://www.cs.bham.ac.uk/%7Emhe/TypeTopology/index.html , respectively
--
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/7d6d61f2-0cb7-7bd9-90b0-077c507cef2f%40panix.com.
