<abstract xmlns="http://www.w3.org/1999/xhtml">Tim 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” [<xref ref-type="bibr" rid="j_forma-2018-0003_ref_003_w2aab3b7b2b1b6b1ab1ab3Aa">3</xref>], [<xref ref-type="bibr" rid="j_forma-2018-0003_ref_004_w2aab3b7b2b1b6b1ab1ab4Aa">4</xref>], [<xref ref-type="bibr" rid="j_forma-2018-0003_ref_014_w2aab3b7b2b1b6b1ab1ac14Aa">14</xref>], [<xref ref-type="bibr" rid="j_forma-2018-0003_ref_005_w2aab3b7b2b1b6b1ab1ab5Aa">5</xref>].With the Mizar system [<xref ref-type="bibr" rid="j_forma-2018-0003_ref_002_w2aab3b7b2b1b6b1ab1ab2Aa">2</xref>], [<xref ref-type="bibr" rid="j_forma-2018-0003_ref_007_w2aab3b7b2b1b6b1ab1ab7Aa">7</xref>] we use some ideas are taken from Tim Makarios’ MSc thesis [<xref ref-type="bibr" rid="j_forma-2018-0003_ref_013_w2aab3b7b2b1b6b1ab1ac13Aa">13</xref>] 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 [<xref ref-type="bibr" rid="j_forma-2018-0003_ref_006_w2aab3b7b2b1b6b1ab1ab6Aa">6</xref>]. Note that the model presented here, may also be called “Beltrami-Klein Model”, “Klein disk model”, and the “Cayley-Klein model” [<xref ref-type="bibr" rid="j_forma-2018-0003_ref_001_w2aab3b7b2b1b6b1ab1ab1Aa">1</xref>].</abstract>

Tim 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” [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].

Klein-Beltrami Model. Part I

Formalized Mathematics

This work is licensed under the Creative Commons Attribution-NonCommercial-NoDerivatives 3.0 License.

{"article-title":"Klein-Beltrami Model. Part I"}

Tim 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...

Klein-Beltrami Model. Part I

Published Online: Jul 28, 2018

Page range: 21 - 32

Received: Mar 27, 2018

DOI: https://doi.org/10.2478/forma-2018-0003

Keywords
Tarski’s geometry axioms, foundations of geometry, Klein-Beltrami model

© 2018 Roland Coghetto, published by Sciendo

This work is licensed under the Creative Commons Attribution-NonCommercial-NoDerivatives 3.0 License.

Klein-Beltrami Model. Part I

Published Online: Jul 28, 2018

Page range: 21 - 32

Received: Mar 27, 2018

DOI: https://doi.org/10.2478/forma-2018-0003

KeywordsTarski’s geometry axioms, foundations of geometry, Klein-Beltrami model

© 2018 Roland Coghetto, published by Sciendo

This work is licensed under the Creative Commons Attribution-NonCommercial-NoDerivatives 3.0 License.

Keywords
Tarski’s geometry axioms, foundations of geometry, Klein-Beltrami model