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/E1hgUOJ-0005f3-VA%40rmmprod07.runbox.
