On Tue, 26 Oct 2010 04:55:48 Jasmin Christian Blanchette wrote: > Now it's your turn! I'm working on establishing that "Euclid's Axiom" in Tarski's axiomatization of the plane is independent of the other axioms. I've already provided a (real, Cartesian) model for all of Tarski's axioms, thus establishing that they are consistent (relative to Isabelle/HOL). My independence proof involves building the Beltrami-Klein model of the hyperbolic plane and then establishing that Euclid's Axiom is false in that model, but all the other axioms are true. Timothy <><
Description: This is a digitally signed message part.