Michael, thanks again, and it works: set theoretic segment ordering!
http://www.math.northwestern.edu/~richter/RichterHOL-LightMiz3HilbertAxiomGeometry.tar.gz
Formalization really clarified my mathematics here. Here's my
definition, following your suggestion (and my original try).
let SegmentOrdering_DEF = new_definition
`s seg_less t <=>
? A B C D X. s = Segment A B /\ t = Segment C D /\
~(A = B) /\ ~(C = D) /\
X IN open (C,D) /\ Segment A B === Segment C X`;;
Here's the miz3 theorem I proved.
SegmentOrderingTransitive_THM : thm =
|- ! s t u. s seg_less t ==> t seg_less u ==> s seg_less u
The problem was not with HOL Light, but my own murky understanding of
segment ordering. I don't think Greenberg and Hartshorne explained it
well, although quite possibly they understood the following point.
Greenberg and Hartshorne both write AB < CD, which means of course
that < is a predicate defined on two segments. The segment AB is the
set of points between A and B together with A and B:
Segment_DEF : thm = |- ! A B. Segment A B = {A, B} UNION open (A,B)
But I'd fallen into the mental mistake of thinking of < as a predicate
defined on four points, not two sets of points, as in
seg<(A, B, C, D).
Not a whole lot is riding on it, but something is:
It's obviously true that AB = BA, and Hartshorne stresses this, and
therefore we don't need Tarski's axiom which amounts to
seg<(A, B, B, A).
One can prove that if AB = XY, then either A = X and B = Y or A = Y
and B = X. I figure this is bound to come up somewhere, but to my
surprise it was not needed in my proof of my transitivity result
above. A more interesting version of this will come up with angle
ordering, or even angle congruence. One typically writes
angle AOB
meaning the subset of the plane which is the union of the two rays
ray OA and ray OB. So
angle AOB = angle BOA and
angle AOB = angle A'OB for any point A' IN ray OA - {O}.
If one wants to think of angle congruence as a relation on 6 points,
then we need two more axioms. Since nobody wants those axioms
angle AOB cong angle BOA
angle AOB cong angle A'OB for any point A' IN ray OA - {O}.
it's important to really thing of the angle as a subset of the plane.
I don't believe I've been really thinking this way. Formalization
will force to me straighten some things out, I believe.
Thanks, Freek, this looks great:
# EXISTS_UNIQUE;;
val it : thm = |- !P. (?!x. P x) <=> (?x. P x /\ (!y. P y ==> y = x))
I see it's from theorems.ml. I'll try it out.
--
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
[email protected]
https://lists.sourceforge.net/lists/listinfo/hol-info
