Thanks Thierry and David. I will probably submit it for publication, though I have not decided on the journal yet.
David: yes, some comments in set.mm and on mmset.html or award2003.html will have to be updated. I will propose something soon. On a related note, after exchanging on my paper, Norm made a few changes in set.mm last August and adopted the phrase "scheme completeness" instead of "metalogical completeness" (only a cosmetic change, but a nice mark of appreciation from him). Benoît On Monday, February 28, 2022 at 3:53:03 PM UTC+1 David A. Wheeler wrote: > > > > On Feb 27, 2022, at 9:51 PM, Mario Carneiro <[email protected]> wrote: > > > > The "classical classical" is deliberate, as explained in the footnote. > > Ah! Got it! Serves me right for just skimming :-). > > --- 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/b1067430-9379-4cea-936c-9afae4d7c6dan%40googlegroups.com.
