@article{f052378d3fdb4a41b4ac86970c5de97c,
title = "Axiomatizations of hyperbolic geometry: A comparison based on language and quantifier type complexity",
abstract = "Hyperbolic geometry can be axiomatized using the notions of order and congruence (as in Euclidean geometry) or using the notion of incidence alone (as in projective geometry). Although the incidence-based axiomatization may be considered simpler because it uses the single binary point-line relation of incidence as a primitive notion, we show that it is syntactically more complex. The incidence-based formulation requires some axioms of the quantifier-type ∀∃∀, while the axiom system based on congruence and order can be formulated using only ∀∃-axioms.",
author = "Victor Pambuccian",
note = "Funding Information: ∗ This paper was written during a stay, supported by a DAAD study visit grant, at the Mathematics Institute of the University of W{\"u}rzburg. I thank the DAAD for its financial support and the Mathematics Institute for its hospitality. 1 For the history and variants of the axiom system, cf. Tarski and Givant (1999). 2 For universal axioms we shall omit to write the universal quantifiers. 3 Zeuthen (1896) went so far as claiming that the geometric construction was the only means of establishing the existence of a geometric object, a claim refuted in this strong form by Knorr (1983) (cf. also Knorr (1986)). 4 However, both Euclidean and hyperbolic n-dimensional geometry can be axiomatized in a first order language with variables to be interpreted as spheres (circles for n = 2, spheres for n = 3, etc.) with a single binary relation τ standing for {\textquoteleft}sphere tangency{\textquoteright}, i.e., τ(ab) stands for {\textquoteleft}a is tangent to b{\textquoteright}, as was shown in Pambuccian (200?).",
year = "2002",
month = dec,
doi = "10.1023/A:1021294808742",
language = "English (US)",
volume = "133",
pages = "331--341",
journal = "Synthese",
issn = "0039-7857",
publisher = "Springer Netherlands",
number = "3",
}