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