> On Aug 21, 2022, at 2:30 AM, Jim Kingdon <[email protected]> wrote:
>
> 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).
This is really cool. I've alerted Freek & asked him to add a link to this in:
https://www.cs.ru.nl/~freek/100#25
I have no idea how Freek will handle this. In this case we want *both* proofs to
be cited. Also, this is a proof of unprovability, not a proof in the usual
sense.
I'll let him figure out what he's going to do :-).
--- 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/4D8368B8-A69E-4BB6-8B72-1BE43FD0C421%40dwheeler.com.
