Re: [isabelle] A general TP/logic question



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
Description: This is a digitally signed message part.



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