Contrary to traditional works on axiomatic foundations of
geometry, the object of this section is not just to show that some
axiomatic formalization of Euclidean geometry exists, but to
provide an effectively useful way to formalize geometry; and not
only Euclidean geometry but other geometries as well.

Precisely, this section aims to combine the following goals:

- Give a nice and useful axiomatic expression of Euclidean
geometry

- Also provide nice axiomatic foundations of other (non-Euclidean) geometries
- Show the deep similarities between these diverse geometries, right from their axiomatic foundations
- Let this be a good start towards higher theories of physics

We may say that affine and vector spaces were already cases of geometrical spaces, however they still did not look so much like our usual Euclidean space. Now finally we are coming to this familiar geometry, as a particular case of a diversity of similar geometries (somehow more similar to the Euclidean one than vector or affine spaces were).

- Types
- Structures
- Axioms

- ℝ = the field of real numbers, with its usual structures (0,1, +,-,⋅), and axioms.
*S*= a 1-dimensional ℝ-vector space (meant as the type of surface densities, i.e. lengths to the power -2), thus with its structures 0,+,-, and the multiplication by real numbers.*E*= a finite-dimensional ℝ-vector space, whose elements may be called "coordinates", "affine forms"*M*= the set of points

and the following common list of structures and axioms:

- An operation from
*E*×*M*to ℝ, that makes the pair (*P*,*E*) form an ℝ-duality system and identifies*M*as a subset of the dual*E** of*E*; equivalently,*E*is identified as an ℝ-subspace of ℝ^{M}. Formally, this means the axioms

- : ∀
*x,y*∈*E*, (∀*u*∈*M*,*x*(*u*) =*y*(*u*)) ⇒*x*=*y*(Separation of*E*by*M*) - ∀
*u,v*∈*M*, (∀*x*∈*E*,*u*(*x*) =*v*(*x*)) ⇒*u*=*v*(Separation of*M*by*E*) - ∀
*x,y*∈*E*,∀*u*∈*M*,*u*(*x*+*y*) =*u*(*x*) +*u*(*y*) - ∀
*x*∈*E*,∀*a*∈ℝ,∀*u*∈*M*, (*ax*)(*u*) =*a**x*(*u*)

- A bilinear, symmetric operation ⋅ from
*E*×*E*to*S*, called the*metric*: - ∀
*x,y*∈*E*,*x*⋅*y*=*y*⋅*x*∈*S* - ∀
*x,y*,z∈*E*, (*x*+*y*)⋅*z*=*x*⋅*z*+*y*⋅*z* - ∀
*x**,y*∈*E*,∀*a*∈ℝ, (*ax*)⋅*y*,=*a*(*x*⋅*y*)

The next structures and axioms will vary between geometries.

*m*≠ 0_{E}- ∀
*x*∈*E*,*m*⋅*x*= 0 *M*={*u*∈*E**|*m*(*u*)=1}, i.e.∀*u*∈*E**,*m*(*u*)=1 ⇔*u*∈*M*

We can define the set of *vectors*, as *V*={*u*∈
*E**| *m*(*u*)=0}.

- ∀
*x*∈*E*, (∀*a*∈ℝ,*x*≠*am*)⇒(∃*y*∈*E*,*x*⋅*y*≠ 0)

that may also be written in the contrapositive form ∀*x*∈*E*,
(∀*y*∈*E*, *x*⋅*y* = 0)⇒(∃*a*∈ℝ, *x*
= *am*)

and may be condensed with the above axiom *m*⋅*x* = 0,
to form a single axiom

- ∀
*x*∈*E*, (∀*y*∈*E*,*x*⋅*y*= 0)⇔(∃*a*∈ℝ,*x*=*am*)

The Euclidean geometry is specified by the more precise axiom

∀*x*∈*E*, (∃*a*∈ℝ, *x* = *am*)⇔( *x*⋅*x*
= 0)

which more precisely implies that the sign of *x*⋅*x*
is fixed (for topological reasons : it cannot switch sign without
cancelling somewhere), and thus may be held as positive (defining
the order in *S*).

The below is a draft being
reworked from old versions. Not sure when it will be
ready... |

In this case, the mass is replaced by a relative mass, that is a
function from *M* to *E*, with a constant *c*∈*S*
called the *curvature* of this geometry, with the axioms

- ∀
*u*∈*M*,*m*(_{u}*u*)=1

- ∀
*x*∈*E*, ∀*u*∈*M*,*m*⋅_{u}*x*=*x*(*u*)*c*

- (one more axiom, to be completed)

Note that flat geometry comes as the particular case where *c*=0.

(This page will be completed later)

The metric may also be expressed in its curried form as the *slope*
function s∈Mor (*E*,*E**)...

Back to Set theory and foundations homepage