Constructive Axiomatization of Plane Hyperbolic Geometry

We provide a universal axiom system for plane hyperbolic geometry in a firstorder language with two sorts of individual variables, ‘points’ (upper‐case) and ‘lines’ (lowercase), containing three individual constants, A₀, A₁, A₂, standing for three non‐collinear points, two binary operation symbols, φ and ι, with φ(A, B) = l 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, π₁(P, 𝓁) and —₂(P, 𝓁), with π_i(P, 𝓁) = g (for i = 1, 2) to be interpreted as ‘g is one of the two limiting paralle lines from P to 𝓁 (provided that P is not on 𝓁, an arbitrary line, otherwise).