nLab Euclidean geometry




Differential geometry

synthetic differential geometry


from point-set topology to differentiable manifolds

geometry of physics: coordinate systems, smooth spaces, manifolds, smooth homotopy types, supergeometry



smooth space


The magic algebraic facts




infinitesimal cohesion

tangent cohesion

differential cohesion

graded differential cohesion

singular cohesion

id id fermionic bosonic bosonic Rh rheonomic reduced infinitesimal infinitesimal & étale cohesive ʃ discrete discrete continuous * \array{ && id &\dashv& id \\ && \vee && \vee \\ &\stackrel{fermionic}{}& \rightrightarrows &\dashv& \rightsquigarrow & \stackrel{bosonic}{} \\ && \bot && \bot \\ &\stackrel{bosonic}{} & \rightsquigarrow &\dashv& \mathrm{R}\!\!\mathrm{h} & \stackrel{rheonomic}{} \\ && \vee && \vee \\ &\stackrel{reduced}{} & \Re &\dashv& \Im & \stackrel{infinitesimal}{} \\ && \bot && \bot \\ &\stackrel{infinitesimal}{}& \Im &\dashv& \& & \stackrel{\text{étale}}{} \\ && \vee && \vee \\ &\stackrel{cohesive}{}& \esh &\dashv& \flat & \stackrel{discrete}{} \\ && \bot && \bot \\ &\stackrel{discrete}{}& \flat &\dashv& \sharp & \stackrel{continuous}{} \\ && \vee && \vee \\ && \emptyset &\dashv& \ast }


Lie theory, ∞-Lie theory

differential equations, variational calculus

Chern-Weil theory, ∞-Chern-Weil theory

Cartan geometry (super, higher)



Euclidean geometry (Euclid 300BC) studies the geometry of Euclidean spaces. These spaces come equipped with a canonical metric in the sense of analysis, in fact a Riemannian metric, and Euclidean geometry may be regarded as the local model for Riemannian geometry, in the sense of Cartan geometry.

In distinction from non-Euclidean geometry (hyperbolic geometry or elliptic geometry), Euclidean geometry is Riemannian geometry of Riemannian manifolds with zero sectional curvature.



Euclidean geometry in the sense of the Idea section makes# reference to the extrinsic notion of real number (to delineate the notion of Euclidean space) and whatever surrounding structure is used to found that notion, but it has also received more intrinsic axiomatic treatments in the spirit of synthetic geometry. Notable among these are Hilbert's axioms, as set out in his Grundlagen der Geometrie, and Tarski‘s axioms, which form a classical first-order axiomatic theory.

Hilbert’s axioms

Here we will just give an extremely sketchy description (for now, see Wikipedia for a fuller account). It should be said right away that two of the Hilbert axioms are not first-order.

Hilbert’s theory has

  • Three sorts: points, line, planes (or if you like: tables, chairs, and beer mugs1);
  • Six relations: betweenness (a ternary relation on points), three incidence relations (one for points and lines, one for points and planes, one for lines and planes), and two congruence relations (a relation L(a,b,c,d)L(a, b, c, d) on points whose intuitive meaning is that the the line segment aba b is congruent to the line segment cdc d, and a relation A(a,b,c,d,e,f)A(a, b, c, d, e, f) on points whose intuitive meaning is that the angle abca b c is congruent to the angle defd e f);

  • A bunch of axioms (20 or 21 depending on which specific edition or translation or exposition one is working with; Wikipedia says 20 but actually has, confusingly, 21 – see the Talk page for more information). They are organized as

    • Axioms of incidence (8),
    • Axioms of betweenness (4),
    • Axioms of congruence (6),
    • Axiom of parallels (the parallel postulate) (1),
    • Axioms of completeness (2), mirroring the archimedean property and the completeness properties of the real numbers. These are not first-order.

I (Todd Trimble) assume Hilbert’s theory is, or is at least intended to be, categorical in the model-theoretic sense, at least considered against a fixed set-theoretic background. In other words I assume the real numbers as complete ordered field would be a definable structure and the axioms are uniquely modeled by 3\mathbb{R}^3 with its Euclidean structure.

Tarski’s axioms

Tarski’s theory EPG (Elementary Plane [Euclidean] Geometry) is a one-sorted theory in classical first-order logic with equality, with variables representing points. There are no constants or operations in the signature, and just two relations:

  • A ternary relation BB (betweenness), with B(x,y,z)B(x, y, z) meaning yy is between xx and zz (yy is on the line segment between xx and zz) – we will write instead BxyzB x y z to conserve space;

  • A 4-ary relation CC (congruence), with C(x,y,z,w)C(x, y, z, w) meaning that a line segment xyx y is congruent (of the same length) as zwz w. For readability, we write this as xyzwx y \equiv z w.

The theory can be presented (in some sense very parsimoniously) by 10 axioms and one first-order axiom scheme. Axioms 8 and 9 constrain the dimension to n=2n = 2 (Euclidean plane geometry), but there are analogues of 8 and 9 that constrain the dimension to any chosen number. Axiom 10 is an extremely disguised version of the Parallel Postulate, with a complicated history behind it. The axiom scheme 11 plays the role of a Dedekind cut axiom expressed in first-order terms.

  1. abba\vdash \; a b \equiv b a,

  2. abpq,abrspqrsa b \equiv p q, a b \equiv r s \;\; \vdash \;\; p q \equiv r s,

  3. abcca=ba b \equiv c c \vdash a = b,

  4. (x)Bqaxaxbc\vdash \; (\exists x)\; B q a x \wedge a x \equiv b c (segment construction: given a line segment bcb c and a line segment from qq to aa, one can extend that line segment in that direction by a segment axa x congruent to bcb c),

  5. ab,Babc,Babc,abab,bcbc,adad,bdbdcdcda \neq b, B a b c, B a' b' c', a b \equiv a' b', b c \equiv b' c', a d \equiv a' d', b d \equiv b' d' \;\; \vdash \;\; c d \equiv c' d' (5 segment axiom),

  6. Babaa=bB a b a \; \vdash \; a = b,

  7. Bapc,Bbqc(x)BpxbBqxaB a p c, B b q c \;\; \vdash \;\; (\exists x)\; B p x b \wedge B q x a (Pasch axiom: roughly, if a line goes through one side of a triangle and not through a vertex, then it must go through another side),

  8. (a,b,c)¬(BabcBbcaBcab)\vdash \; (\exists a, b, c)\; \neg (B a b c \vee B b c a \vee B c a b) (there exist three non-collinear points: the dimension is at least 2),

  9. pq,apaq,bpbq,cpcqBabcBbcaBcabp \neq q, a p \equiv a q, b p \equiv b q, c p \equiv c q \;\; \vdash \;\; B a b c \vee B b c a \vee B c a b (if three points are each equidistant from two given distinct points pp and qq, then those three points are collinear: the dimension is at most 2),

  10. Badt,Bbdc,ad(x,y)BabxBacyBytxB a d t, B b d c, a \neq d \;\; \vdash \;\; (\exists x, y)\; B a b x \wedge B a c y \wedge B y t x (Parallel Postulate (!)),

  11. (Cut schema) Let ϕ(x)\phi(x) be a formula in which variables a,b,ya, b, y do not occur freely, and let ψ(y)\psi(y) be a formula in which a,b,xa, b, x do not occur freely. Then

    (x,y)(ϕ(x)ψ(y)Baxy)(b)(x,y)(ϕ(x)ψ(y)Bxby)(\forall x, y)\; (\phi(x) \wedge \psi(y) \Rightarrow B a x y) \;\; \vdash \;\; (\exists b)(\forall x, y)\; (\phi(x) \wedge \psi(y) \Rightarrow B x b y)

    (if every element yy in the set defined by ψ\psi lies beyond every element xx in the set defined by ϕ\phi as seen from the perspective of aa, then there is some bb between every such xx and every such yy).

See Tarski-Givant for a thorough discussion of this and related axiom systems, and an extensive bibliography.

One important aspect of the meta-theory lies in the relation of models of this theory to real closed fields. If RR is a real closed field, then there is a corresponding model of EPG whose underlying set is R×RR \times R and where the relations BB and CC are interpreted by expected conditions:

C(x,y,z,w)iff(x 1y 1) 2+(x 2y 2) 2=(z 1w 1) 2+(z 2w 2) 2C(x, y, z, w) \;\;\; iff \;\;\; (x_1 - y_1)^2 + (x_2 - y_2)^2 = (z_1 - w_1)^2 + (z_2 - w_2)^2
B(x,y,z)iff(x 1y 1)(y 2z 2)=(x 2y 2)(y 1z 1)0(x 1y 1)(y 1z 1)0(x 2y 2)(y 2z 2).B(x, y, z) \;\;\; iff \;\;\; (x_1 - y_1)(y_2 - z_2) = (x_2 - y_2)(y_1 - z_1) \; \wedge \; 0 \leq (x_1 - y_1)(y_1 - z_1) \; \wedge \; 0 \leq (x_2 - y_2)(y_2 - z_2).

It is mostly straightforward to verify that this structure on R×RR \times R satisfies the EPG axioms (all but the cut schema hold for any ordered field). More importantly,


For every model MM of EPG there is a real closed field RR such that MR×RM \cong R \times R as models.

Of course there is some arbitrariness involved in the choice of isomorphism; for example, any line segment xyx y can be used to stipulate a unit length and a coordinate axis. The proof is lightly sketched in Tarski; again only the first ten axioms are needed to produce an ordered field structure on RR, with the cut schema being used to verify the real closure.

The significance of this result is that EPG is a complete and decidable theory, just as the theory of real closed fields is complete and decidable. Hence there exists an algorithm which, on being fed a sentence in the language of Elementary Plane Geometry, will produce a proof of the sentence or a proof of its negation in the theory.

Mac Lane’s axioms

To be written, see Mac Lane (1959) for details.

Basic notions and facts in ( differential) Euclidean geometry (see also at: differential geometry of curves and surfaces)

Other flavors of geometry

synthetic geometry
Euclidean geometry
hyperbolic geometry
elliptic geometry

Riemannian geometry, Cartan geometry:

geometric contextgauge groupstabilizer subgrouplocal model spacelocal geometryglobal geometrydifferential cohomologyfirst order formulation of gravity
differential geometryLie group/algebraic group GGsubgroup (monomorphism) HGH \hookrightarrow Gquotient (“coset space”) G/HG/HKlein geometryCartan geometryCartan connection
examplesEuclidean group Iso(d)Iso(d)rotation group O(d)O(d)Cartesian space d\mathbb{R}^dEuclidean geometryRiemannian geometryaffine connectionEuclidean gravity
Poincaré group Iso(d1,1)Iso(d-1,1)Lorentz group O(d1,1)O(d-1,1)Minkowski spacetime d1,1\mathbb{R}^{d-1,1}Lorentzian geometrypseudo-Riemannian geometryspin connectionEinstein gravity
anti de Sitter group O(d1,2)O(d-1,2)O(d1,1)O(d-1,1)anti de Sitter spacetime AdS dAdS^dAdS gravity
de Sitter group O(d,1)O(d,1)O(d1,1)O(d-1,1)de Sitter spacetime dS ddS^ddeSitter gravity
linear algebraic groupparabolic subgroup/Borel subgroupflag varietyparabolic geometry
conformal group O(d,t+1)O(d,t+1)conformal parabolic subgroupMöbius space S d,tS^{d,t}conformal geometryconformal connectionconformal gravity
supergeometrysuper Lie group GGsubgroup (monomorphism) HGH \hookrightarrow Gquotient (“coset space”) G/HG/Hsuper Klein geometrysuper Cartan geometryCartan superconnection
examplessuper Poincaré groupspin groupsuper Minkowski spacetime d1,1|N\mathbb{R}^{d-1,1\vert N}Lorentzian supergeometrysupergeometrysuperconnectionsupergravity
super anti de Sitter groupsuper anti de Sitter spacetime
higher differential geometrysmooth 2-group GG2-monomorphism HGH \to Ghomotopy quotient G//HG//HKlein 2-geometryCartan 2-geometry
cohesive ∞-group∞-monomorphism (i.e. any homomorphism) HGH \to Ghomotopy quotient G//HG//H of ∞-actionhigher Klein geometryhigher Cartan geometryhigher Cartan connection
examplesextended super Minkowski spacetimeextended supergeometryhigher supergravity: type II, heterotic, 11d


  • Euclid, Elements, 300BC

  • Alfred Tarski, What is elementary geometry?, in The axiomatic method. With special reference to geometry and physics Proceedings of an International Symposium held at the Univ. of Calif., Berkeley, Dec. 26, 1957-Jan. 4, 1958 (ed. L. Henkin, P. Suppes, and A. Tarski), Studies in Logic and the Foundations of Mathematics, Amsterdam: North-Holland (1959), pp. 16–29. (pdf)

  • Alfred Tarski and Steven Givant, Tarski’s system of geometry, Bull. Symb. Logic, Vol. 5 No. 2 (1999), 175–214. (web)

  • Saunders Mac Lane, Metric postulates for plane geometry, American Mathematical Monthly, Vol. 66 No. 7 (1959), 543–555. (doi:10.2307/2309851, web)

Textbook account:

Expository lecture notes:

  • Drew Armstrong, Introduction to Geometry, 2017 (pdf)

Textbook accounts of the axiomatization of Euclidean geometry include these:

Full formalization of this book in Coq (as synthetic geometry but following Tarski’s work) is discussed at

A formalisation of Euclid using diagrammatic reasoning is in

  • J. Avigad, E. Dean, J. Mumma, A formal system for Euclid’s Elements , arXiv:0810.4315 (2009).

Another formalization of Euclidean geometry in Coq:

  • Evgeny V. Ivashkevich, On Constructive-Deductive Method For Plane Euclidean Geometry (arXiv:1903.05175)

  1. After a famous saying attributed to Hilbert which in some sense heralds the axiomatic spirit: ‘Man muß jederzeit an Stelle von “Punkte, Geraden, Ebenen” “Tische, Stühle, Bierseidel” sagen können’. The 1891 anecdote is reported by O. Blumenthal in Hilbert, Gesammelte Abhandlungen III. Band , Springer Berlin 1935, p.403. The three classes became ‘Liebe, Gesetz, Schornsteinfeger’ (love, law, chimney-sweep) in Hilbert’s letter to Frege (Dec. 29th 1899). The question raised in Frege’s rejoinder (Jan. 6th 1900) whether his pocket watch is a point is still an open problem.

Last revised on May 17, 2022 at 18:09:18. See the history of this page for a list of all contributions to it.