Re: [isabelle] A general TP/logic question

On Wed, Mar 23, 2011 at 11:01 PM, Timothy McKenzie <tjm1983 at> wrote:
> On Thu, 24 Mar 2011 05:11:15 Mark.Janney at 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.

I see. Do you know where I can find the proof that shows that it's unprovable?


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