*To*: John Munroe <munddr at gmail.com>*Subject*: Re: [isabelle] A general TP/logic question*From*: Timothy McKenzie <tjm1983 at gmail.com>*Date*: Thu, 24 Mar 2011 15:14:06 +1300*Cc*: Mark.Janney at gdc4s.com, cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <AANLkTi=WQ8vaVOFudvAbcD6LdbKOy33qbUOH7gtnGQ36@mail.gmail.com>*References*: <AANLkTimuEwUCUaJVrxhFpuRo4RP2aqSR2LVk9b+Zn34v@mail.gmail.com> <201103241201.53533.tjm1983@gmail.com> <AANLkTi=WQ8vaVOFudvAbcD6LdbKOy33qbUOH7gtnGQ36@mail.gmail.com>*User-agent*: KMail/1.13.6 (Linux/2.6.34.8-68.fc13.x86_64; KDE/4.5.5; x86_64; ; )

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**

**References**:**[isabelle] A general TP/logic question***From:*John Munroe

**Re: [isabelle] A general TP/logic question***From:*Timothy McKenzie

**Re: [isabelle] A general TP/logic question***From:*John Munroe

- Previous by Date: Re: [isabelle] A general TP/logic question
- Next by Date: [isabelle] Making records instances of classes
- Previous by Thread: Re: [isabelle] A general TP/logic question
- Next by Thread: Re: [isabelle] A general TP/logic question
- Cl-isabelle-users March 2011 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list