I mentionned it in https://groups.google.com/d/msg/metamath/BSOOYEw2sjU/TmHaccI5AwAJ and I think Thierry took it into account in his treatment (he was part of that discussion in the fall).
Benoit On Thursday, June 27, 2019 at 3:24:45 PM UTC+2, David A. Wheeler wrote: > > The paper "A further simplification of Tarski's axioms of geometry" by > Timothy Makarios is at: > https://arxiv.org/abs/1306.0066 . It tweaks the axioms to allow "another > of the axioms to be omitted from the set of axioms and proven as a > theorem." In particular, by tweaking one axiom, another axiom turns into a > provable theorem. > > Would it be useful to do this in set.mm? > > --- 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/dacd448d-a2a7-4b9f-9483-9b1395147c07%40googlegroups.com.
