It is clear to me that a surface of constant negative Gaussian curvature satisfies the hyperbolic axiom (more than one 'straight' line not meeting a given 'straight' line). Hartshorne (Geometry: Euclid and Beyond p. 374) defines the hyperbolic plane as the Hilbert plane + the hyperbolic axiom.
I'd like a proof that this axiomatic definition of the hyperbolic plane implies a surface of constant negative Gaussian curvature.
Usually answers arrive quickly to my questions on Math Stack Exchange. This one didn't so I asked a friend who is a professor of mathematics about it. His response is included in quotes -- clearly the problem was a lot harder than I thought. EVEN THOUGH I AM ANSWERING MY OWN QUESTION THIS IS NOT MY ANSWER BUT HIS.
" Proving that the axiomatic definition of hyperbolic geometry implies constant negative curvature can be done but requires a lot of work. The first thing you have to do is prove that given any two points p and q in the hyperbolic plane, there is an isometry that takes p to q. By a basic theorem of Gauss, this implies that the Gaussian curvature K is the same at p and q. Hence K is constant. Then the Gauss-Bonnet Theorem says that if you have a geodesic triangle T with angles A, B, C, you have
since K is constant. This implies K area(T) = A+B+C-pi < 0 by a basic result in hyperbolic geometry. Hence K must be negative, so we have constant negative curvature.
To get real numbers into the HIlbert plane H, you need to impose "rulers" on the lines of H. The idea is that you pick one line L in H and mark two points on it. The axioms then give a bijection from L to the real numbers R that takes the two points to 0 and 1, and then every line in H gets a similar bijection which gives a "ruler" for each line. This allows you to assign lengths to all line segments, which gives a metric. With more work, you get a setup that allows you to get a Riemannian metric on H, hence a curvature, and the lines in H become geodesics in this metric since they minimize distance. All of this takes a LOT of work.
It is a lot easier to build a model that satisfies the axioms. Since the axioms are categorical (all models are isomorphic), you can prove theorems in the model. Doing axiomatic proofs in geometry can be grueling if you insist on justifying every step by an axiom or previous result. When I teach geometry, I try to treat the axioms with a light touch."
I responded to this
"Thanks a lot. It certainly explains why I couldn’t figure this out on my own. An isometry of the hyperbolic plane implies the existence a metric on it. Where does the metric come from? In my reading the formula for the metric seems very ad hoc. "
He got back saying --
"Pick two points on a line and call one 0 and the other 1. By ruler and compass, you can then mark off points on the line that correspond to all rational numbers. But Hilbert also has an axiom of completeness, which gives a bijection between the line and the set of real numbers.
The crucial thing about the isometry group of the plane is that it transitive in the sense of group actions, so that if something happens at one point, then the same thing happens at any other point.
The method explained in my previous email gives a metric on the plane which seems a bit ad-hoc. But one can prove that any two metrics constructed this way are positive real number multiples of each other. "