Tarskian Geometry - move to main body?

[David A. Wheeler]

There's been a lot of work to define Tarskian geometry in set.mm.

In particular, Thierry Arnoux has defined ` TarskiG ` (the class of all spaces
that satisfy the Tarski axioms for geometry). This is the same approach as
earlier made by Scott Fenton, but this builds on generic structures.
There's also a proof that the Euclidean space ( EEG ` N ) is such a space.

Should this be moved to the main body and used as the primary
building block for geometry in set.mm? My understanding was that we wanted to
move to something that builds on generic structures, and this looks plausible.

I don't know all the pluses and minuses of doing that. However,
it's hard to work together on geometry until we agree on a starting point.

One issue: Tarski geometry includes Euclid's axiom
(parallel postulate), TarskiGE. It seems to me we should also define a set that
doesn't include that, so that we have a good starting point for both Euclidean and
non-Euclidean geometry. I presume that's richly covered in the literature.

--- David A. Wheeler

[Benoit]

I have a remark on this Tarski geometry part.

The two primitive notions in Tarski's treatment are the ternary predicate of betweenness and the quaternary predicate of congruence.  In the set.mm treatment, you use classes to emulate these.  This is pretty harmless, since classes are defined exactly for the purpose of emulating predicates: a class is the extension of a predicate (albeit a unary one, see below).  Maybe this difference from Tarski's treatment could be documented in the header comment of the Tarski geometry part?  Furthermore, there is a small glitch for the treatment of betweenness and a larger one for the treatment of congruence.

As for betweenness:

Using obvious notation, and putting Tarski's treatment on the left hand side and the set.mm treatment on the right (and sometimes ignoring functionality in the space, i.e. writing e.g. "Itv" in place of "(Itv ' e)").

The straightforward translation would have been

( ( Btw a x b ) <-> (a, x, b) e. Seg )   [here, each (Seg ' e) is a subset of e^3]

but you use

( ( Btw a x b ) <-> x e. ( a Itv b ) ).

This is harmless since a product determines and is determined by its slices.  But maybe it could be documented.

As for congruence:

The straightforward translation would have been

( ( Cong a b c d ) <-> (a, b, c, d) \in Congr )   [here, each (Congr ' e) is a subset of e^4]

but you use

( ( Cong a b c d ) <-> a dist b = c dist d ).

This is a little further away from Tarski's treatment.  And as you say, it modifies a bit the associated axioms (e.g. transitivity is not needed anymore in the set.mm treatment).  (Side note: the other axioms are not really reflexivity and identity, as you say, but are closer to symmetry and separatedness.)  Again, the treatments are equivalent, as I now prove (I switch to pseudoTeX).  Given Congr \subseteq X^4, one can define a function Dist : X^2 \to X^2 by Dist(a, b) := \{ (c, d) \mid (a, b, c, d) \in Congr \}.  If Congr satisfies Tarski's axioms, then Dist satisfies your axioms.  Conversely, given Dist : X^2 \to Y, define the set Congr := \{ (a, b, c, d) \in X^4 \mid Dist(a, b) = Dist(c, d) \}.  If Dist satisfies your axioms, then Congr satisfies Tarski's axioms.

This was probably your reasoning behind the choice of your treatment (and sorry if it was already laid out somewhere in this discussion group or a github issue), but maybe, as trivial as it may be, it could be documented in the header comment?

Actually, I prefer the version with (Seg ' e) \subseteq e^3 and (Congr ' e) \subseteq e^4, since they are closer to Tarski's treatment.  Too late to change?  Or does it have too many drawbacks?  Any thoughts?

A side remark: why did you rename "segment" to "interval"?  In my opinion, "segment" is less ambiguous since a segment always contains its endpoints, whereas an interval may or may not.  I also think that "segment" is much more common in the context of elementary geometry (actually, I don't recall having ever seen "interval" used in that context: it was always "segment").

Needless to say, this is great work: congratulations to Thierry and earlier contributors Scott and Mario.

Benoît

[Thierry Arnoux]

Hi David,

Note that with the current setup, it's still possible to define
non-Euclidean geometry as ` ( TarskiG \ TarskiGE ) ` .

But I think you're right: until now all theorems in geometry also apply
to non-Euclidean geometries, so I could redefine TarskiG without
requiring Euclid's axiom, and then use ` ( TarskiG i^i TarskiGE ) ` when
Euclid's axiom / the parallel postulate is required.

Besides this change, I would like to define a " Line " slot for
geometric lines. Mario then suggested that this slot is defined by the
other slots for Tarski Geometries, but it could be used for axioms of
other geometry definitions (Hilbert's axioms, or Incidence geometry).

BR,

_
Thierry

[Thierry Arnoux]

Hi Benoît,

I feel it's a bit late to change the definitions, but we shall certainly document this in the header comment of the geometry part.

Would you like to suggest the complete text?

Changing interval into segment would not be very impacting, it's a matter of a global replace. I had initially chosen this name because it was Mario's suggestion. To me also, interval relates more to real number intervals, while segment is what I was used to hear in geometry. Any other opinions about this?

BR,
_
Thierry

Benoît --
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 metamath+u...@googlegroups.com.
To post to this group, send email to meta...@googlegroups.com.
Visit this group at https://groups.google.com/group/metamath.
For more options, visit https://groups.google.com/d/optout.

[Benoit]

Thanks Thierry.  Below is my proposal.  I'd be happy to change everywhere Itv --> Seg and interval --> segment.  Apparently, so do you.  Other opinions?

Note: the introduction below is voluntarily informal.  I find this more disgestible on a first reading.  This passes "MM> verify markup */file" (except for the references to ~ df-tarskg... ).

$(
#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#
                ELEMENTARY GEOMETRY (TARSKI'S AXIOMS)
#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#
This part develops elementary geometry based on Tarski's axioms, following
[Schwabhauser].  Tarski's geometry is a first-order theory with one sort, the
"points".  It has two primitive notions, the ternary predicate of "betweenness"
and the quaternary predicate of "congruence".  To adapt this theory to the
framework of set.mm, and to be able to talk of *a* Tarski structure as a space
satisfying the given axioms, we use the following definition, stated
informally:

A Tarski structure ` f ` is a set (of points) ` ( Base `` f ) ` together with
functions ` ( Itv `` f ) ` and ` ( dist `` f ) ` on
` ( ( Base `` f ) X. ( Base `` f ) ) ` satisfying certain axioms (given in the
definitions ~ df-tarskg... _et sequentes_).  This allows us to treat a Tarski
structure as a special kind of extensible structure (see ~ df-struct ).

The translation to and from Tarski's treatment is as follows (given, again,
informally).

Suppose that one is given an extensible structure ` f ` .  One defines a
betweenness ternary predicate Btw by positing that, for any
` x , y , z e. ( Base `` f ) ` , one has "Btw ` x y z ` " if and only if
` y e. x ( Itv `` f ) z ` , and a congruence quaternary predicate Congr by
positing that, for any ` x , y , z , t e. ( Base `` f ) ` , one has
"Congr ` x y z t ` " if and only if ` x ( dist `` f ) y = z ( dist `` f ) t ` .
It is easy to check that if ` f ` satisfies our Tarski axioms, then Btw and
Congr satisfy Tarki's Tarski axioms when ` ( Base `` f ) ` is interpreted as
the universe of discourse.

Conversely, suppose that one is given a set ` a ` , a ternary predicate Btw and
quaternary predicate Congr.  One defines the extensible structure ` f `
such that ` ( Base `` f ) ` is ` a ` , and ` ( Itv `` f ) ` is the function
which associates with each ` <. x , y >. e. ( a X. a ) ` the set of points
` z e. a ` such that "Btw ` x z y ` ", and ` ( dist `` f ) ` is the function
which associates with each ` <. x , y >. e. ( a X. a ) ` the set of ordered
pairs ` <. z , t >. e. ( a X. a ) ` such that "Congr ` x y z t ` ".  It is easy
to check that if Btw and Congr satisfy Tarski's Tarski axioms when ` a ` is
interpreted as the universe of discourse, then ` f ` satisfies our Tarski
axioms.

For descriptions of individual axioms, we refer to the specific definitions
below.  A particular feature of Tarski's axioms is modularity, so by using
various subsets of the set of axioms, we can define the classes of "absolute
dimensionless Tarski structures" ( ~ df-tarskg... ), of "Euclidean
dimensionless Tarski structures" ( ~df-tarskg... ) and of "plane Euclidean
Tarski structures"( ~ df-tarskg... ).

The first section is devoted to the definitions of these various structures.
The second section ("Tarskian geometry") develops the synthetic treatment of
geometry.  The remaining sections prove that the real Euclidean spaces and
complex Hilbert spaces, with intended interpretations, are Euclidean Tarski
structures.

Most of the work in this part is due to Thierry Arnoux, with ealier groundwork
by Mario Carneiro and Scott Fenton.  See also the credits in the comment of
each statement.
$)

[Jim Kingdon]

"segment" (in place of "interval") sounds good to me. That's pretty much universal terminology in this context, as far as I've noticed.

[David A. Wheeler]

In case people haven't noticed, the set.mm main body now has a major new section:

"ELEMENTARY GEOMETRY".

Much of this is due toThierry Arnoux, with earlier groundwork

by Mario Carneiro and Scott Fenton.

My SINCERE THANKS to ALL!

There's a special satisfaction in this case because Whitehead and Russell

had originally planned for their Principia Mathematica to include a geometry section

("A fourth volume on the foundations of geometry had been planned, but the authors

admitted to intellectual exhaustion upon completion of the third."

https://en.wikipedia.org/wiki/Principia_Mathematica ).

I think of set.mm in some sense as a "modern Principia Mathematica" -

but this modern version uses more common notation, ZFC, and is now starting to

cover that previously-missing area.... geometry.

--- David A. Wheeler