Announcing the proof that Schroeder-Bernstein is equivalent to excluded middle (over IZF)

[Jim Kingdon]

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

[heiph...@wilsonb.com]

This is absolutely beautiful. Congratulations!

Incidentally, I just recently re-discovered Schroeder-Bernstein, realizing that
I have thoroughly internalized the result without ever attempting a proof.
Poking at the latter gave me whiffs of some deeper foundational links, but I
just assumed it was some AoC connection. This is way cooler.

[David A. Wheeler]

> On Aug 21, 2022, at 2:30 AM, Jim Kingdon <kin...@panix.com> 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

[Jim Kingdon]

On 8/22/22 07:33, David A. Wheeler wrote:

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 :-).

Yeah, he has a convention of putting constructive proofs in italics but doesn't define what "constructive" means. For irrationality of the square root of two the italicized proof is for the equivalent of https://us.metamath.org/ileuni/sqrt2irr.html but I (and wikipedia) interpret "constructive" in the context of this problem as meaning something stronger - https://us.metamath.org/ileuni/sqrt2irrap.html .

I suppose the exmidsbth result may fall under the "does not keep track of all formalizations" disclaimer at the top of the page, but we can let him worry about that sort of thing.

If the goal for iset.mm (supposing it were tracked separately from set.mm) is to get above the lowest-ranked prover on the list, we need three more proofs (iset.mm is at 6 and the lowest prover on the list is at 8). Fortunately, after a dry spell I am finally starting to make some progress on https://github.com/metamath/set.mm/issues/2575 which is a blocker for most of the Metamath 100 theorems (because they rely on summation one way or another).

On a personal note I won't rest until I have https://us.metamath.org/mpeuni/taupi.html in iset.mm.

Which also relies on summation.

[David A. Wheeler]

> On Aug 23, 2022, at 12:41 AM, Jim Kingdon <kin...@panix.com> wrote:
> If the goal for iset.mm (supposing it were tracked separately from set.mm) is to get above the lowest-ranked prover on the list, we need three more proofs (iset.mm is at 6 and the lowest prover on the list is at 8). Fortunately, after a dry spell I am finally starting to make some progress on https://github.com/metamath/set.mm/issues/2575 which is a blocker for most of the Metamath 100 theorems (because they rely on summation one way or another).
>
> On a personal note I won't rest until I have https://us.metamath.org/mpeuni/taupi.html in iset.mm.
> Which also relies on summation.

We could ask him to track "Metamath (intuitionistic)" separately from "Metamath".
and use the former for entries in set.mm. It's up to him if he does that.

Should we ask?

--- David A. Wheeler

[Benoit]

That's a real achievement, congratulations to Jim !

As for Wiedijk's list, I think the first principle would be to find a method that minimizes his work.  He's maintaining the list out of goodwill and we do not want him to associate Metamath with extra work nor the Metamath community with lobbyists who try to overpublicize their work (I know it's not the case: I'm only speaking of the impression that this might give, and I may very well be misguided).

There are probably other formal systems with some top-100 theorems proved in multiple databases(?), so I do not know if we can ask for a special treatment for Metamath and have both versions linked. (This is not rhetorical: I really "do not know" if this is justified or not.)

In any case, it would be nice to have cross-links between the comments in https://us.metamath.org/mpeuni/sbth.html and https://us.metamath.org/ileuni/exmidsbth.html, so that if only one version is referenced from the outside, the visitor can be informed of both versions by visiting any one of them.

Benoît

[David A. Wheeler]

> On Aug 24, 2022, at 9:09 AM, Benoit <benoit...@gmail.com> wrote:
> ...

> In any case, it would be nice to have cross-links between the comments in https://us.metamath.org/mpeuni/sbth.html and https://us.metamath.org/ileuni/exmidsbth.html, so that if only one version is referenced from the outside, the visitor can be informed of both versions by visiting any one of them.

Good idea. Your wish is my command:

https://github.com/metamath/set.mm/pull/2793

--- David A. Wheeler

[Jim Kingdon]

I don't know but I was thinking of making such a request, if any, after we have 9 theorems for iset.mm (above the lowest ranking prover currently on the list). Currently we are at 6.

Now it is up to him how to categorize and the field is a bit of a wild west in terms of what axioms/libraries/etc each of the proofs on the list depend on, so that's why I'm at least as worried about our own tracking as I am about how we are able to present it on that list.