Abstract: 
Tarski's axioms of plane geometry are formalized and, using the standard
real Cartesian model, shown to be consistent. A substantial theory of
the projective plane is developed. Building on this theory, the
KleinBeltrami model of the hyperbolic plane is defined and shown to
satisfy all of Tarski's axioms except his Euclidean axiom; thus Tarski's
Euclidean axiom is shown to be independent of his other axioms of plane
geometry.
An earlier version of this work was the subject of the author's
MSc thesis,
which contains naturallanguage explanations of some of the
more interesting proofs.

BibTeX: 
@article{Tarskis_GeometryAFP,
author = {T. J. M. Makarios},
title = {The independence of Tarski's Euclidean axiom},
journal = {Archive of Formal Proofs},
month = oct,
year = 2012,
note = {\url{http://afp.sf.net/entries/Tarskis_Geometry.shtml},
Formal proof development},
ISSN = {2150914x},
}
