On Wed, Aug 1, 2012 at 6:00 AM, Bill Richter
<[email protected]>wrote:
> new_type("point",0);;
> new_type_abbrev("point_set",`:point->bool`);;
> new_constant("Between",`:point->point->point->bool`);;
> new_constant("Line",`:point_set->bool`);;
> new_constant("≡",`:(point->bool)->(point->bool)->bool`);;
> I haven't read the manual carefully, but I see that you're working in
> something like a model of ZFC (except there's no empty set), and that
> `new_type' does not occur in the manual. I see it occurs in the
> Description manual
> http://sourceforge.net/projects/hol/files/hol/kananaskis-7/kananaskis-7-description.pdf/download
> I hope you can appreciate my confusion, as I'm working in HOL Light, and
> John Harrison's documentation barely explains HOL, and he does not (I
> think) refer to your manuals. A few dumb questions first:
>
> Can we call your manual a HOL4 manual?
Yes.
> Do all version of HOL (e.g. HOL Light, Proof Power & Isabelle) abide by
> your Logic manual?
Roughly yes, with minor variations, except for Isabelle. Isabelle is a
logical framework. Isabelle/HOL very roughly abides by the HOL4 Logic
manual but the logic inherits some completely new features from the
underlying framework.
> What does Kananaskis mean?
>
It's the name of some lakes and a river in Alberta. (I think that's the
intended reference.) It was adopted (as was "Athabasca"), as the name of a
"generation" of HOL4 releases. We're up to Kananaskis release 7 (soon to be
8).
>
> My guess is that my new_type declaration of "point" says that there exists
> an un-named set of point, and that any variable of type point will refer to
> an element of this set. Is that right? Let's call this set H, for Hilbert
> plane. The new_constant declaration of "Line" then says there's a
> predicate Line defined on the power set P(H). So later on when I write
>
> let l be point_set;
> let A B C be point;
> assume Line l
>
> I mean that 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? Can you explain an easy way
> I can cite this in my forthcoming geometry paper?
>
new_type and new_constant add new types and new constants to HOL by fiat. I
suppose you must characterise them with new_axiom.
The HOL Logic Manual does not mention new_type because one of its aims is
to build a model of HOL in set theory to give confidence that HOL is sound.
Once you use new_type or new_constant or new_axiom, the model described in
the manual is no longer guaranteed to exist.
It's up to you to show that another model exists if you want people to
believe your work isn't inconsistent.
(And it's hard to imagine doing so without first understanding the manual
or something equivalent.)
But if you know roughly what your model would look like, and it fits within
the existing HOL model (very likely), then there's no reason to declare new
types and new constants by fiat and then prove that the resulting system is
sound (outside of the proof assistant).
You can use HOL4's (and HOL Light's) mechanisms for definition! (You end up
doing roughly the same proof, and you get the advantage of having it
formalised and checked by the system.)
The manual does account for definitions of new types and constants by
conservative extension and explicitly proves that such definitions are
covered by the model in set theory that it develops.
>
> BTW I recently adopted a better spin of my paper. Before I was saying
> that I was improving Hartshorne's book Geometry: Euclid and Beyond, as a
> number of his proofs have gaps too wide for a high school student to leap.
> Sounds kinda negativistic, right? Now I say that I'm continuing
> Hartshorne's great work by actually formalizing Hartshorne's Theorem 10.4,
> that all of Euclid's propositions in book I up to Prop (I.28) are true in
> any Hilbert plane, except for Props (I.1) and (I.22), which require extra
> 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
> [email protected]
> 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
[email protected]
https://lists.sourceforge.net/lists/listinfo/hol-info
