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.
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). > > 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/2XIGEC7PMJVHG.32IXF4AMAZ4OF%40wilsonb.com.
