Tweak set.mm using "A further simplification of Tarski's axioms of geometry" by Timothy Makarios?

David A. Wheeler

unread,

Jun 27, 2019, 9:24:45 AM6/27/19

to metamath

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

Benoit

unread,

Jun 27, 2019, 9:55:45 AM6/27/19

to Metamath

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

David A. Wheeler

unread,

Jun 27, 2019, 10:06:24 AM6/27/19

to Benoit, Metamath

On June 27, 2019 9:55:44 AM EDT, Benoit <benoit...@gmail.com> wrote:
>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).

If it was used, we should cite it. If it wasn't used, maybe we should...!

--- David A.Wheeler

Thierry Arnoux

unread,

Jun 27, 2019, 7:19:51 PM6/27/19

to meta...@googlegroups.com, David A. Wheeler, Benoit

Actually I did *not* take it into account, so as mentioned by David, we
shall use it!

David A. Wheeler

unread,

Jul 1, 2019, 7:00:43 PM7/1/19

to Thierry Arnoux, metamath, Benoit

On Fri, 28 Jun 2019 07:19:46 +0800, Thierry Arnoux <thierry...@gmx.net> wrote:
> Actually I did *not* take it into account, so as mentioned by David, we
> shall use it!

Good! To prevent this from being forgotten, I've created an issue to track it:

https://github.com/metamath/set.mm/issues/976

Reply all

Reply to author

Forward