Klein-Beltrami Model. Part I

Tim Makarios (with Isabelle/HOL¹) and John Harrison (with HOL-Light²) shown that “the Klein-Beltrami model of the hyperbolic plane satisfy all of Tarski’s axioms except his Euclidean axiom” [3], [4], [14], [5].

With the Mizar system [2], [7] we use some ideas are taken from Tim Makarios’ MSc thesis [13] for the formalization of some definitions (like the absolute) and lemmas necessary for the verification of the independence of the parallel postulate. This work can be also treated as further development of Tarski’s geometry in the formal setting [6]. Note that the model presented here, may also be called “Beltrami-Klein Model”, “Klein disk model”, and the “Cayley-Klein model” [1].