Thanks for the compliments! To fully examine density in surreals, also take a look at ~ nodense and ~ nocvxmin . They give that there's a unique birthday-minimal element of any convex class of surreals. To recover Conway's simplicity theorem (the uniqueness of the surreal cut) you need to combine those theorems with ~ noeta . I'm actually working on that today.
As a side note, does anyone know any good references on recursion over weakly founded relationships (that is, where R Fr A as opposed to R We A)? I'm going to need that for the next step in surreals - defining addition and multiplication. -Scott On Wed, Dec 8, 2021 at 12:58 PM Jim Kingdon <[email protected]> wrote: > Oooh, awesome. For those who haven't been following, the result is "given > two sets of surreals such that one comes completely before the other, there > is a surreal lying strictly between the two. Furthermore, there is an > upper bound on the birthday of that surreal." My mental model of the > surreals had been "the real numbers glued to the ordinals" but clearly I > need to amend that with "yeah, but dense all the way" or something of the > sort. > > And agreed about it being cool to formalize new mathematics. Anyone want > to take a crack at proving in iset.mm that the Schroeder-Bernstein > theorem implies excluded middle (full excluded middle, not just a weaker > omniscience principle)? I've looked over the 2019 paper which proves it but > I think formalizing this might be beyond my abilities. > > Seeing that people were using provers to discover new theorems in type > theory and then only later writing them up informally in the HoTT Book was > another example of me being inspired about provers potential to be in the > thick of mathematics, not just a curiosity on the side. > > On December 8, 2021 8:04:41 AM PST, "David A. Wheeler" < > [email protected]> wrote: > >All: > > > >I wanted to publicly congratulate Scott Fenton on his work > >to formalize surreals. The merged pull request is here: > >https://github.com/metamath/set.mm/pull/2360 > > > >He defined surreals in Metamath 10 years ago, but now > >we have a Metamath formalization of their fundamental theorem. > > > >Especially interesting to me when I commented about it, he said, > >"It literally took a new proof coming out in the literature for > >it to get formal enough for Metamath!". I'm pretty sure he meant > >[Lipparini] Lipparini, Paolo, > ><I>A clean way to separate sets of surreals</I> arXiv:1712.03500 > (20-May-2018); > >available at <A HREF="https://arxiv.org/abs/1712.03500";> > >https://arxiv.org/abs/1712.03500</A> (retrieved 7 Dec 2021). > > > >I think that comment is telling. Significant parts of set.mm necessarily > formalizes > >"relatively old well-known mathematics". Here's a case where we're > >formalizing recent work. I know it's not the only case, but I find > >that encouraging. > > > >--- 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/387AEE25-86DC-4E0C-993A-DFD9CC09C94C%40panix.com > . > -- 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/CACKrHR_gvxtRUYo07-qoKSRe-Ob2JszH3_0XYTrV38Dt2SXDfQ%40mail.gmail.com.
