On Thu, Aug 2, 2012 at 8:03 AM, Bill Richter
<rich...@math.northwestern.edu>wrote:
> Thanks, Ramana and Rob! As Rob says, I don't use new_axiom to define by
> type "point", but I do use new_axiom to define Hilbert's geometry axioms,
> so I took no offense. I would definitely prefer to use neither new_type
> nor new_axiom. I'm using what John set me up with, but I think he thought
> of it as more of a way to get started, rather than the best way to
> formalize Euclid's book 1. BTW I don't think either of you answered my
> question
>
> > the variable l refers to a subset of H, the variables A, B & C
> > refer to elements of H, and that the subset l is actually a line,
> > meaning that Line(l) =True. Am I getting this right?
>
> I would prefer to say that a Hilbert plane is a set H with two relations,
> Between and ===, with a predicate Line defined on subsets of H, so that H
> satisfies the axioms I1--3, B1--4 and C1--6.
Yes, you can certainly say that all with definitions.
Define a four-argument predicate
Hilbert_plane H (Between) (===) Line = axiom_1_holds /\ axiom_2_holds /\
...
and use that as a hypothesis on all your theorems.
H, Between, ===, and Line, will all be variables that you universally
quantify over, but restrict with the hypothesis Hilbert_plane.
Apart from avoiding new_axiom, this has the additional benefit of making
your results reusable: anyone can provide whatever H, Between, ===, and
Line they want by specialising one of your theorems and their obligation is
to show that their combination satisfies all the axioms then they get your
result as a conclusion.
That's how I wrote my Tarski geometry Mizar code. I wasn't quite happy
> with that, and folks certainly believe that Hilbert's axioms are
> consistent. But I would like to know how to avoid new_type nor new_axiom.
I described how above. And we have discussed this before. See for example
http://sourceforge.net/mailarchive/message.php?msg_id=29172311
> It's possible that miz3 could not handle the extra set theory load, as
> John suggested, and he said he'd improve the miz3 set theory capacity when
> he returned. Neither of you addressed
>
> > John Harrison's documentation barely explains HOL, and he does
> > not (I think) refer to your manuals.
>
> Do you agree with me? What is to be made of this?
Read the history of HOL Light.
Here are some suggestions:
http://www.cl.cam.ac.uk/~jrh13/papers/holright.html
http://www.cl.cam.ac.uk/~mjcg/papers/HolHistory.html
http://www.nicta.com.au/__data/assets/pdf_file/0010/17695/tphols-2008.pdf
> I mean, if one uses new_type in HOL Light, what theorems is HOL Light
> supposed to be formalizing? I don't know where John writes anything
> stronger about types than on p 13 of his tutorial:
>
> A key feature of HOL is that every term has a well-defined
> type. Roughly speaking, the type indicates what kind of
> mathematical object the term represents (a number, a set, a
> function, etc.)
>
> --
> 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
>
------------------------------------------------------------------------------
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
