Klein-Beltrami model. Part IV

Abstract

Timothy Makarios (with Isabelle/HOL1) and John Harrison (with HOL-Light2) shown that “the Klein-Beltrami model of the hyperbolic plane satisfy all of Tarski’s axioms except his Euclidean axiom” [2],[3],[4, 5]. With the Mizar system [1] we use some ideas taken from Tim Makarios’s MSc thesis [10] to formalize some definitions and lemmas necessary for the verification of the independence of the parallel postulate. In this article, which is the continuation of [8], we prove that our constructed model satisfies the axioms of segment construction, the axiom of betweenness identity, and the axiom of Pasch due to Tarski, as formalized in [11] and related Mizar articles.