Re: [isabelle] A general TP/logic question



On Thu, 24 Mar 2011 13:38:35 you wrote:
> > Only my work on the hyperbolic plane is necessary to
> > establish that Euclid's axiom is unprovable in Tarski's
> > theory of the absolute plane, but my work on the Cartesian
> > plane establishes that the negation of Euclid's axiom is
> > also unprovable from that theory.
> 
> I see. Do you know where I can find the proof that shows that
> it's unprovable?

I'm not sure exactly what you're looking for.  Are you after the 
proof that Euclid's axiom is unprovable from Tarski's other axioms 
of the plane?  This is surprisingly difficult to find.

The version of Tarski's axioms I'm using is from Metamathematische 
Methoden in der Geometrie by Schwabhäuser, Szmielew, and Tarski 
(which is made slightly more difficult by the fact that I don't 
speak German --- not yet, anyway).  I'm told that the first 
published version of Tarski's axioms was in The Axiomatic Method 
(1959); from memory it was the second paper.

The following paper in The Axiomatic Method was Some 
Metamathematical Problems Concerning Elementary Hyperbolic 
Geometry, by Szmielew.  She used a modified version of Tarski's 
axioms, where Euclid's axiom was replaced with a hyperbolic axiom, 
stronger than the negation of Euclid's axiom.  Her theorem 2.15 
states that a system is a model of these axioms of hyperbolic 
space if and only if it's isomorphic with the Klein space of 
appropriate dimension.

Unfortunately for me, her proof begins by asserting that it's 
"well known" that the Klein space satisfies the hyperbolic version 
of Tarski's axioms.  It's a little difficult to see how it could 
already be well known as soon as the axioms were first published.  
(The proof goes on to show in more detail that every model of the 
hyperbolic version of Tarski's axioms must be isomorphic to the 
Klein space, which isn't the direction I need.)

Other publications (including Metamathematische Methoden in der 
Geometrie) that state the result I want, or something closely 
related, generally refer the reader to Szmielew's paper for the 
"proof", which is frustrating.

Szmielew did partly make up for it, though.  The book I'm finding 
most useful in formalizing this independence result is Foundations 
of Geometry by Borsuk & Szmielew (which I am grateful was 
translated into English from the original Polish).  It uses a 
different set of axioms from Tarski's, but they're similar enough 
to be helpful. The book describes the Klein-Beltrami model of the 
hyperbolic plane, starting on page 245, and then checks that it 
satisfies their axioms, starting on page 250.

In the process of formalizing the independence result in Isabelle, 
I've found a few errors in Borsuk & Szmielew, but I guess this is 
likely in any similar publication.

The Klein-Beltrami model of the hyperbolic plane is by no means 
the only one.  It's useful to me because it preserves betweenness, 
which is one of the primitive relations in Tarksi's axioms.  If 
you're using a different set of axioms, another model might be 
more useful.

Tim
<><

Attachment: signature.asc
Description: This is a digitally signed message part.



This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.