Hi Bill, | 1) One advantage of Tarski's axioms over Hilbert's is that they're | ``more'' FOL. In my Hilbert paper, I'm constantly using set theory, | and we use sets to define notions like rays, angles and triangles, and | the congruence axioms are based on these set-definitions. So what a | great place to try out HOL set theory ideas!
Indeed so, though as Phil pointed out earlier, you may need to be careful not to assume the axiom of infinity without justification. That shouldn't be a danger since you will be using the special geometric type of points without relying on any infinite types like :num that are already there. In fact, Phil and Jacques have an interesting paper where they systematically derive the natural numbers from some of Hilbert's axioms. | That would really make a joke out of my scheme. An aggressive | automation would be able to handle this simpler proof, because | TarskiModel is a label saying that S satisfies Tarski's axioms, | including A1 and A2. Well, much to my relief, this simpler proof | didn't work. Which means that the Mizar automation is so | non-aggressive that we can do 2-column proofs this way. I assume | miz3 is similarly non-aggressive. In general, the default miz3 prover may be more powerful than Mizar's because it first tries "HOL_BY" (which is close to Mizar's basic prover) and then MESON (which is a more general first-order prover. However, since "TarskiModel(....)" refers to something merely defined to be equal to the conjunction of the axioms, rather than actually *being* the conjunction of those axioms, neither prover will automatically take that definition into account. So indeed I don't think this will by default work in miz3 either. This situation does seem right from a pedagogical point of view if you want to identify clearly where each axiom and earlier theorem gets used in a proof. John. ------------------------------------------------------------------------------ Live Security Virtual Conference Exclusive live event will cover all the ways today's security and threat landscape has changed and how IT managers can respond. Discussions will include endpoint security, mobile security and the latest in malware threats. http://www.accelacomm.com/jaw/sfrnl04242012/114/50122263/ _______________________________________________ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
