Constructive axiomatization of plane hyperbolic geometry

Research output: Contribution to journalArticlepeer-review

5 Scopus citations


We provide a universal axiom system for plane hyperbolic geometry in a first-order language with two sorts of individual variables, 'points' (upper-case) and 'lines' (lower-case), containing three individual constants, A0, A1, A2, standing for three non-collinear points, two binary operation symbols, φ and ι, with φ(A, B) = ι to be interpreted as 'ι is the line joining A and B' (provided that A ≠ B, an arbitrary line, otherwise), and ι(g, h) = P to be interpreted as 'P is the point of intersection of g and h (provided that g and h are distinct and have a point of intersection, an arbitrary point, otherwise), and two binary operation symbols, π1(P, ι) and π2(P, ι), with πi(P, ι) = g (for i = 1, 2) to be interpreted as 'g is one of the two limiting parallel lines from P to ι (provided that P is not on ι, an arbitrary line, otherwise).

Original languageEnglish (US)
Pages (from-to)475-488
Number of pages14
JournalMathematical Logic Quarterly
Issue number4
StatePublished - Dec 1 2001


  • Constructive axiomatization
  • Hyperbolic geometry

ASJC Scopus subject areas

  • Logic


Dive into the research topics of 'Constructive axiomatization of plane hyperbolic geometry'. Together they form a unique fingerprint.

Cite this