Yes, for now you can replace the "new_axiom" stuff with the
explicit model construction I sent out earlier. I will experiment a
bit to find the nicest way of doing things with the axioms as
hypotheses. I like Freek's idea of having the hypothesis in the
assumption list of the theorem rather than as the antecedent of an
implication, but I need to dig into miz3 a bit more deeply or get
help from Freek to make it work.
Great, John, and thanks for helping me! I have two thoughts:
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!
2) I've often posted here that my Mizar code was silly, but I think I
finally understand it. I'm taking advantage of a Mizar feature: a
more aggressive automation would defeat my 2-column proofs, but Mizar
is aggressive enough that it works. It goes like this:
I have a big definition of all the axioms, and I give them names like
CongruenceSymmetry. Then I define a a set S to be a Tarski-model if
it satisfies all the axioms, so e.g. S CongruenceSymmetry is true.
Then I prove theorems that the axioms hold for a Tarski model! All 7
proofs are ridiculously short. Then I invoke the axioms like this.
In theorem EquivReflexive, the 2-line proof is
b,a equiv a,b by A1, TarskiModel;
hence a,b equiv a,b by A2, TarskiModel;
I thought today, why didn't I just write the proof simpler, like
b,a equiv a,b by TarskiModel;
hence a,b equiv a,b by TarskiModel;
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. So I now think my original Mizar code
isn't so bad, and it looks even better with the extra HOL-powered sets
needed for Hilbert's axioms.
--
Best,
Bill
------------------------------------------------------------------------------
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
