\documentclass[12pt,titlepage]{article}

\usepackage{amsmath}
\usepackage{mathrsfs}
\usepackage{amsfonts}
\usepackage{amssymb}
\usepackage{amsthm}
\usepackage{mathtools}
\usepackage{graphicx}
\usepackage{color}
\usepackage{ucs}
\usepackage[utf8x]{inputenc}
\usepackage{xparse}
\usepackage{hyperref}

%----Macros----------
%
% Unresolved issues:
%
%  \righttoleftarrow
%  \lefttorightarrow
%
%  \color{} with HTML colorspec
%  \bgcolor
%  \array with options (without options, it's equivalent to the matrix environment)

% Of the standard HTML named colors, white, black, red, green, blue and yellow
% are predefined in the color package. Here are the rest.
\definecolor{aqua}{rgb}{0, 1.0, 1.0}
\definecolor{fuschia}{rgb}{1.0, 0, 1.0}
\definecolor{gray}{rgb}{0.502, 0.502, 0.502}
\definecolor{lime}{rgb}{0, 1.0, 0}
\definecolor{maroon}{rgb}{0.502, 0, 0}
\definecolor{navy}{rgb}{0, 0, 0.502}
\definecolor{olive}{rgb}{0.502, 0.502, 0}
\definecolor{purple}{rgb}{0.502, 0, 0.502}
\definecolor{silver}{rgb}{0.753, 0.753, 0.753}
\definecolor{teal}{rgb}{0, 0.502, 0.502}

% Because of conflicts, \space and \mathop are converted to
% \itexspace and \operatorname during preprocessing.

% itex: \space{ht}{dp}{wd}
%
% Height and baseline depth measurements are in units of tenths of an ex while
% the width is measured in tenths of an em.
\makeatletter
\newdimen\itex@wd%
\newdimen\itex@dp%
\newdimen\itex@thd%
\def\itexspace#1#2#3{\itex@wd=#3em%
\itex@wd=0.1\itex@wd%
\itex@dp=#2ex%
\itex@dp=0.1\itex@dp%
\itex@thd=#1ex%
\itex@thd=0.1\itex@thd%
\advance\itex@thd\the\itex@dp%
\makebox[\the\itex@wd]{\rule[-\the\itex@dp]{0cm}{\the\itex@thd}}}
\makeatother

% \tensor and \multiscript
\makeatletter
\newif\if@sup
\newtoks\@sups
\def\append@sup#1{\edef\act{\noexpand\@sups={\the\@sups #1}}\act}%
\def\reset@sup{\@supfalse\@sups={}}%
\def\mk@scripts#1#2{\if #2/ \if@sup ^{\the\@sups}\fi \else%
  \ifx #1_ \if@sup ^{\the\@sups}\reset@sup \fi {}_{#2}%
  \else \append@sup#2 \@suptrue \fi%
  \expandafter\mk@scripts\fi}
\def\tensor#1#2{\reset@sup#1\mk@scripts#2_/}
\def\multiscripts#1#2#3{\reset@sup{}\mk@scripts#1_/#2%
  \reset@sup\mk@scripts#3_/}
\makeatother

% \slash
\makeatletter
\newbox\slashbox \setbox\slashbox=\hbox{$/$}
\def\itex@pslash#1{\setbox\@tempboxa=\hbox{$#1$}
  \@tempdima=0.5\wd\slashbox \advance\@tempdima 0.5\wd\@tempboxa
  \copy\slashbox \kern-\@tempdima \box\@tempboxa}
\def\slash{\protect\itex@pslash}
\makeatother

% math-mode versions of \rlap, etc
% from Alexander Perlis, "A complement to \smash, \llap, and lap"
%   http://math.arizona.edu/~aprl/publications/mathclap/
\def\clap#1{\hbox to 0pt{\hss#1\hss}}
\def\mathllap{\mathpalette\mathllapinternal}
\def\mathrlap{\mathpalette\mathrlapinternal}
\def\mathclap{\mathpalette\mathclapinternal}
\def\mathllapinternal#1#2{\llap{$\mathsurround=0pt#1{#2}$}}
\def\mathrlapinternal#1#2{\rlap{$\mathsurround=0pt#1{#2}$}}
\def\mathclapinternal#1#2{\clap{$\mathsurround=0pt#1{#2}$}}

% Renames \sqrt as \oldsqrt and redefine root to result in \sqrt[#1]{#2}
\let\oldroot\root
\def\root#1#2{\oldroot #1 \of{#2}}
\renewcommand{\sqrt}[2][]{\oldroot #1 \of{#2}}

% Manually declare the txfonts symbolsC font
\DeclareSymbolFont{symbolsC}{U}{txsyc}{m}{n}
\SetSymbolFont{symbolsC}{bold}{U}{txsyc}{bx}{n}
\DeclareFontSubstitution{U}{txsyc}{m}{n}

% Manually declare the stmaryrd font
\DeclareSymbolFont{stmry}{U}{stmry}{m}{n}
\SetSymbolFont{stmry}{bold}{U}{stmry}{b}{n}

% Manually declare the MnSymbolE font
\DeclareFontFamily{OMX}{MnSymbolE}{}
\DeclareSymbolFont{mnomx}{OMX}{MnSymbolE}{m}{n}
\SetSymbolFont{mnomx}{bold}{OMX}{MnSymbolE}{b}{n}
\DeclareFontShape{OMX}{MnSymbolE}{m}{n}{
    <-6>  MnSymbolE5
   <6-7>  MnSymbolE6
   <7-8>  MnSymbolE7
   <8-9>  MnSymbolE8
   <9-10> MnSymbolE9
  <10-12> MnSymbolE10
  <12->   MnSymbolE12}{}

% Declare specific arrows from txfonts without loading the full package
\makeatletter
\def\re@DeclareMathSymbol#1#2#3#4{%
    \let#1=\undefined
    \DeclareMathSymbol{#1}{#2}{#3}{#4}}
\re@DeclareMathSymbol{\neArrow}{\mathrel}{symbolsC}{116}
\re@DeclareMathSymbol{\neArr}{\mathrel}{symbolsC}{116}
\re@DeclareMathSymbol{\seArrow}{\mathrel}{symbolsC}{117}
\re@DeclareMathSymbol{\seArr}{\mathrel}{symbolsC}{117}
\re@DeclareMathSymbol{\nwArrow}{\mathrel}{symbolsC}{118}
\re@DeclareMathSymbol{\nwArr}{\mathrel}{symbolsC}{118}
\re@DeclareMathSymbol{\swArrow}{\mathrel}{symbolsC}{119}
\re@DeclareMathSymbol{\swArr}{\mathrel}{symbolsC}{119}
\re@DeclareMathSymbol{\nequiv}{\mathrel}{symbolsC}{46}
\re@DeclareMathSymbol{\Perp}{\mathrel}{symbolsC}{121}
\re@DeclareMathSymbol{\Vbar}{\mathrel}{symbolsC}{121}
\re@DeclareMathSymbol{\sslash}{\mathrel}{stmry}{12}
\re@DeclareMathSymbol{\bigsqcap}{\mathop}{stmry}{"64}
\re@DeclareMathSymbol{\biginterleave}{\mathop}{stmry}{"6}
\re@DeclareMathSymbol{\invamp}{\mathrel}{symbolsC}{77}
\re@DeclareMathSymbol{\parr}{\mathrel}{symbolsC}{77}
\makeatother

% \llangle, \rrangle, \lmoustache and \rmoustache from MnSymbolE
\makeatletter
\def\Decl@Mn@Delim#1#2#3#4{%
  \if\relax\noexpand#1%
    \let#1\undefined
  \fi
  \DeclareMathDelimiter{#1}{#2}{#3}{#4}{#3}{#4}}
\def\Decl@Mn@Open#1#2#3{\Decl@Mn@Delim{#1}{\mathopen}{#2}{#3}}
\def\Decl@Mn@Close#1#2#3{\Decl@Mn@Delim{#1}{\mathclose}{#2}{#3}}
\Decl@Mn@Open{\llangle}{mnomx}{'164}
\Decl@Mn@Close{\rrangle}{mnomx}{'171}
\Decl@Mn@Open{\lmoustache}{mnomx}{'245}
\Decl@Mn@Close{\rmoustache}{mnomx}{'244}
\makeatother

% Widecheck
\makeatletter
\DeclareRobustCommand\widecheck[1]{{\mathpalette\@widecheck{#1}}}
\def\@widecheck#1#2{%
    \setbox\z@\hbox{\m@th$#1#2$}%
    \setbox\tw@\hbox{\m@th$#1%
       \widehat{%
          \vrule\@width\z@\@height\ht\z@
          \vrule\@height\z@\@width\wd\z@}$}%
    \dp\tw@-\ht\z@
    \@tempdima\ht\z@ \advance\@tempdima2\ht\tw@ \divide\@tempdima\thr@@
    \setbox\tw@\hbox{%
       \raise\@tempdima\hbox{\scalebox{1}[-1]{\lower\@tempdima\box
\tw@}}}%
    {\ooalign{\box\tw@ \cr \box\z@}}}
\makeatother

% \mathraisebox{voffset}[height][depth]{something}
\makeatletter
\NewDocumentCommand\mathraisebox{moom}{%
\IfNoValueTF{#2}{\def\@temp##1##2{\raisebox{#1}{$\m@th##1##2$}}}{%
\IfNoValueTF{#3}{\def\@temp##1##2{\raisebox{#1}[#2]{$\m@th##1##2$}}%
}{\def\@temp##1##2{\raisebox{#1}[#2][#3]{$\m@th##1##2$}}}}%
\mathpalette\@temp{#4}}
\makeatletter

% udots (taken from yhmath)
\makeatletter
\def\udots{\mathinner{\mkern2mu\raise\p@\hbox{.}
\mkern2mu\raise4\p@\hbox{.}\mkern1mu
\raise7\p@\vbox{\kern7\p@\hbox{.}}\mkern1mu}}
\makeatother

%% Fix array
\newcommand{\itexarray}[1]{\begin{matrix}#1\end{matrix}}
%% \itexnum is a noop
\newcommand{\itexnum}[1]{#1}

%% Renaming existing commands
\newcommand{\underoverset}[3]{\underset{#1}{\overset{#2}{#3}}}
\newcommand{\widevec}{\overrightarrow}
\newcommand{\darr}{\downarrow}
\newcommand{\nearr}{\nearrow}
\newcommand{\nwarr}{\nwarrow}
\newcommand{\searr}{\searrow}
\newcommand{\swarr}{\swarrow}
\newcommand{\curvearrowbotright}{\curvearrowright}
\newcommand{\uparr}{\uparrow}
\newcommand{\downuparrow}{\updownarrow}
\newcommand{\duparr}{\updownarrow}
\newcommand{\updarr}{\updownarrow}
\newcommand{\gt}{>}
\newcommand{\lt}{<}
\newcommand{\map}{\mapsto}
\newcommand{\embedsin}{\hookrightarrow}
\newcommand{\Alpha}{A}
\newcommand{\Beta}{B}
\newcommand{\Zeta}{Z}
\newcommand{\Eta}{H}
\newcommand{\Iota}{I}
\newcommand{\Kappa}{K}
\newcommand{\Mu}{M}
\newcommand{\Nu}{N}
\newcommand{\Rho}{P}
\newcommand{\Tau}{T}
\newcommand{\Upsi}{\Upsilon}
\newcommand{\omicron}{o}
\newcommand{\lang}{\langle}
\newcommand{\rang}{\rangle}
\newcommand{\Union}{\bigcup}
\newcommand{\Intersection}{\bigcap}
\newcommand{\Oplus}{\bigoplus}
\newcommand{\Otimes}{\bigotimes}
\newcommand{\Wedge}{\bigwedge}
\newcommand{\Vee}{\bigvee}
\newcommand{\coproduct}{\coprod}
\newcommand{\product}{\prod}
\newcommand{\closure}{\overline}
\newcommand{\integral}{\int}
\newcommand{\doubleintegral}{\iint}
\newcommand{\tripleintegral}{\iiint}
\newcommand{\quadrupleintegral}{\iiiint}
\newcommand{\conint}{\oint}
\newcommand{\contourintegral}{\oint}
\newcommand{\infinity}{\infty}
\newcommand{\bottom}{\bot}
\newcommand{\minusb}{\boxminus}
\newcommand{\plusb}{\boxplus}
\newcommand{\timesb}{\boxtimes}
\newcommand{\intersection}{\cap}
\newcommand{\union}{\cup}
\newcommand{\Del}{\nabla}
\newcommand{\odash}{\circleddash}
\newcommand{\negspace}{\!}
\newcommand{\widebar}{\overline}
\newcommand{\textsize}{\normalsize}
\renewcommand{\scriptsize}{\scriptstyle}
\newcommand{\scriptscriptsize}{\scriptscriptstyle}
\newcommand{\mathfr}{\mathfrak}
\newcommand{\statusline}[2]{#2}
\newcommand{\tooltip}[2]{#2}
\newcommand{\toggle}[2]{#2}

% Theorem Environments
\theoremstyle{plain}
\newtheorem{theorem}{Theorem}
\newtheorem{lemma}{Lemma}
\newtheorem{prop}{Proposition}
\newtheorem{cor}{Corollary}
\newtheorem*{utheorem}{Theorem}
\newtheorem*{ulemma}{Lemma}
\newtheorem*{uprop}{Proposition}
\newtheorem*{ucor}{Corollary}
\theoremstyle{definition}
\newtheorem{defn}{Definition}
\newtheorem{example}{Example}
\newtheorem*{udefn}{Definition}
\newtheorem*{uexample}{Example}
\theoremstyle{remark}
\newtheorem{remark}{Remark}
\newtheorem{note}{Note}
\newtheorem*{uremark}{Remark}
\newtheorem*{unote}{Note}

%-------------------------------------------------------------------

\begin{document}

%-------------------------------------------------------------------


\section*{Euclidean geometry}

\hypertarget{context}{}\subsubsection*{{Context}}\label{context}

\hypertarget{geometry}{}\paragraph*{{Geometry}}\label{geometry}

[[!include higher geometry - contents]]

\hypertarget{differential_geometry}{}\paragraph*{{Differential geometry}}\label{differential_geometry}

[[!include synthetic differential geometry - contents]]

\hypertarget{contents}{}\section*{{Contents}}\label{contents}

\noindent\hyperlink{idea}{Idea}\dotfill \pageref*{idea} \linebreak
\noindent\hyperlink{properties}{Properties}\dotfill \pageref*{properties} \linebreak
\noindent\hyperlink{Axiomatizations}{Axiomatizations}\dotfill \pageref*{Axiomatizations} \linebreak
\noindent\hyperlink{hilberts_axioms}{Hilbert's axioms}\dotfill \pageref*{hilberts_axioms} \linebreak
\noindent\hyperlink{TarskiAxioms}{Tarski's axioms}\dotfill \pageref*{TarskiAxioms} \linebreak
\noindent\hyperlink{related_concepts}{Related concepts}\dotfill \pageref*{related_concepts} \linebreak
\noindent\hyperlink{references}{References}\dotfill \pageref*{references} \linebreak


\hypertarget{idea}{}\subsection*{{Idea}}\label{idea}

\emph{Euclidean geometry} (\hyperlink{Euclid300BC}{Euclid 300BC}) studies the [[geometry]] of [[Euclidean spaces]]. These spaces come equipped with a canonical [[metric space|metric]] in the sense of [[analysis]], in fact a [[Riemannian metric]], and Euclidean geometry may be regarded as the \emph{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]].

\hypertarget{properties}{}\subsection*{{Properties}}\label{properties}

\begin{itemize}%
\item [[Pythagorean theorem]]


\item [[pentagon decagon hexagon identity]]


\item [[conic section]]


\item [[Hadwiger's theorem]]


\item [[Non-Euclidean geometry]]



\end{itemize}
\hypertarget{Axiomatizations}{}\subsection*{{Axiomatizations}}\label{Axiomatizations}

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 [[axiom|axiomatic]] treatments in the spirit of [[synthetic geometry]]. Notable among these are [[Hilbert|Hilbert's]] axioms, as set out in his \emph{Grundlagen der Geometrie}, and [[Alfred Tarski|Tarski]]`s axioms, which form a first-order axiomatic theory.

\hypertarget{hilberts_axioms}{}\subsubsection*{{Hilbert's axioms}}\label{hilberts_axioms}

Here we will just give an extremely sketchy description (for now, see \href{http://en.wikipedia.org/wiki/Hilbert%27s_axioms}{Wikipedia} for a fuller account). It should be said right away that two of the Hilbert axioms are \emph{not} first-order.

Hilbert's [[theory]] has

\begin{itemize}%
\item Three sorts: points, line, planes (or if you like: tables, chairs, and beer mugs\footnote{After a famous saying attributed to Hilbert which in some sense heralds the axiomatic spirit: `\emph{Man mu\ss{} jederzeit an Stelle von ``Punkte, Geraden, Ebenen'' ``Tische, St\"u{}hle, Bierseidel'' sagen k\"o{}nnen}'. The 1891 anecdote is reported by O. Blumenthal in Hilbert, \emph{Gesammelte Abhandlungen III. Band} , Springer Berlin 1935, p.403. The three classes became `\emph{Liebe, Gesetz, Schornsteinfeger}' (love, law, chimney-sweep) in Hilbert's letter to [[Gottlob Frege|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.} );

\end{itemize}
\begin{itemize}%
\item 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)$ on points whose intuitive meaning is that the the line segment $a b$ is congruent to the line segment $c d$, and a relation $A(a, b, c, d, e, f)$ on points whose intuitive meaning is that the angle $a b c$ is congruent to the angle $d e f$);


\item 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

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

\end{itemize}


\end{itemize}
I ([[Todd Trimble]]) assume Hilbert's theory is, or is at least intended to be, [[categoricity|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 $\mathbb{R}^3$ with its Euclidean structure.

\hypertarget{TarskiAxioms}{}\subsubsection*{{Tarski's axioms}}\label{TarskiAxioms}

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

\begin{itemize}%
\item A ternary relation $B$ (betweenness), with $B(x, y, z)$ meaning $y$ is between $x$ and $z$ ($y$ is on the line segment between $x$ and $z$) -- we will write instead $B x y z$ to conserve space;


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



\end{itemize}
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 = 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|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.

\begin{enumerate}%
\item $\vdash \; a b \equiv b a$,


\item $a b \equiv p q, a b \equiv r s \;\; \vdash \;\; p q \equiv r s$,


\item $a b \equiv c c \vdash a = b$,


\item $\vdash \; (\exists x)\; B q a x \wedge a x \equiv b c$ (segment construction: given a line segment $b c$ and a line from $q$ to $a$, one can extend that line in that direction by a segment $a x$ congruent to $b c$),


\item $a \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),


\item $B a b a \; \vdash \; a = b$,


\item $B 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),


\item $\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),


\item $p \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 $p$ and $q$, then those three points are collinear: the dimension is at most 2),


\item $B 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 (!)),


\item (Cut schema) Let $\phi(x)$ be a formula in which variables $a, b, y$ do not occur freely, and let $\psi(y)$ be a formula in which $a, b, x$ do not occur freely. Then

\begin{displaymath}
(\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)
\end{displaymath}
(if every element $y$ in the set defined by $\psi$ lies beyond every element $x$ in the set defined by $\phi$ as seen from the perspective of $a$, then there is some $b$ between every such $x$ and every such $y$).



\end{enumerate}
See \hyperlink{TG}{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 $R$ is a real closed field, then there is a corresponding model of EPG whose underlying set is $R \times R$ and where the relations $B$ and $C$ are interpreted by expected conditions:

\begin{displaymath}
C(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
\end{displaymath}
\begin{displaymath}
\,
\end{displaymath}
\begin{displaymath}
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).
\end{displaymath}
It is mostly straightforward to verify that this structure on $R \times R$ satisfies the EPG axioms (all but the cut schema hold for any ordered field). More importantly,

\begin{theorem}
\label{}\hypertarget{}{}
For every model $M$ of EPG there is a real closed field $R$ such that $M \cong R \times R$ as models.

\end{theorem}
Of course there is some arbitrariness involved in the choice of isomorphism; for example, any line segment $x y$ can be used to stipulate a unit length and a coordinate axis. The proof is lightly sketched in \hyperlink{Tar}{Tarski}; again only the first ten axioms are needed to produce an ordered field structure on $R$, 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.

\hypertarget{related_concepts}{}\subsection*{{Related concepts}}\label{related_concepts}

\begin{tabular}{l}
[[synthetic geometry]]\\
\hline 
[[Euclidean geometry]]\\
[[hyperbolic geometry]]\\
[[elliptic geometry]]\\
\end{tabular}

\begin{itemize}%
\item [[parallel postulate]]


\item [[trigonometry]]


\item [[space form]]


\item [[Riemannian geometry]]



\end{itemize}
[[!include local and global geometry - table]]

\hypertarget{references}{}\subsection*{{References}}\label{references}

\begin{itemize}%
\item [[Euclid]], \emph{[[Elements]]}, 300BC


\item [[Alfred Tarski]], \emph{What is elementary geometry?}, in \emph{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. (\href{http://www.geographicknowledge.de/SeminarLFG/Tarski_Whatiselementarygeometry.pdf}{pdf})


\item [[Alfred Tarski]] and Steven Givant, \emph{Tarski's system of geometry}, Bull. Symb. Logic, Vol. 5 No. 2 (1999), 175--214. (\href{http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.27.9012}{web})



\end{itemize}
Textbook account:

\begin{itemize}%
\item [[Elmer Rees]], \emph{Notes on Geometry}, Springer 2005

\end{itemize}
Expository lecture notes:

\begin{itemize}%
\item Drew Armstrong, \emph{Introduction to Geometry}, 2017 (\href{http://www.math.miami.edu/~armstrong/daVinci/HGnotes.pdf}{pdf})

\end{itemize}
Textbook accounts of the axiomatization of Euclidean geometry include these:

\begin{itemize}%
\item [[Wolfram Schwabhäuser]], [[Wanda Szmielew]], [[Alfred Tarski]], \emph{Mathematische Methoden in der Geometrie}, Springer 1983


\item [[Anton Petrunin]], \emph{Euclidean Plane and its Relatives; a minimalistic introduction}, (\href{https://arxiv.org/abs/1302.1630}{arXiv:1302.1630})



\end{itemize}
Full formalization of this book in [[Coq]] (as [[synthetic geometry]] but following Tarski's work) is discussed at

\begin{itemize}%
\item [[Gabriel Braun]], [[Pierre Boutry]], [[Julien Narboux]], \emph{\href{http://geocoq.github.io/GeoCoq/}{GeoCoq}}, \emph{\href{http://gabrielbraun.free.fr/Geometry/Tarski/}{La g\'e{}om\'e{}trie de Tarski en Coq}}

\end{itemize}
A formalisation of Euclid using diagrammatic reasoning is in

\begin{itemize}%
\item J. Avigad, E. Dean, J. Mumma, \emph{A formal system for Euclid's Elements} , \href{http://arxiv.org/abs/0810.4315v3}{arXiv:0810.4315} (2009).

\end{itemize}
[[!redirects Euclidean geometry]] [[!redirects Euclidean geometries]]



\end{document}