*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] A general TP/logic question*From*: Timothy McKenzie <tjm1983 at gmail.com>*Date*: Thu, 24 Mar 2011 12:01:40 +1300*Cc*: Mark.Janney at gdc4s.com, munddr at gmail.com*In-reply-to*: <9D31108D62FAE54AA21AEF899D69931E07E75749@AZ25EXM04.gddsi.com>*References*: <AANLkTimuEwUCUaJVrxhFpuRo4RP2aqSR2LVk9b+Zn34v@mail.gmail.com> <9D31108D62FAE54AA21AEF899D69931E07E75749@AZ25EXM04.gddsi.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 05:11:15 Mark.Janney at gdc4s.com wrote: > You could try to exhibit a model of T in which 'f = g' holds > and then exhibit another model of T in which 'f = g' does not > hold. That's how the 'parallel postulate' of Euclidian > geometry was shown to be unprovable from the other axioms. I'm currently doing this in Isabelle. The way I've chosen to do it is using locales. I have a locale for (Tarski's axioms of) the absolute plane. I've proven that the real Cartesian plane is an instance of this locale and that it also satisfies Tarski's version of "Euclid's axiom". I've now defined a model of the hyperbolic plane, and I'm in the process of proving that it's also an instance of my absolute plane locale. Then I'll need to prove that it doesn't satisfy Euclid's axiom. 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. In all of this, I have to rely on the assumption that Isabelle/HOL is consistent, but I guess all work in Isabelle/HOL makes that assumption. Tim <><

**Attachment:
signature.asc**

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

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

**Re: [isabelle] A general TP/logic question***From:*Mark.Janney

- Previous by Date: Re: [isabelle] A general TP/logic question
- Next by Date: Re: [isabelle] A general TP/logic question
- 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