Hi Bill,
It's important to understand that the HOL4 Logic Manual gives a
(more-or-less) formal semantics of a formal logic. That's two levels of
formal! None of the set theory given in this document is actually part of
the HOL logic itself. Rather the set theory is a formal way of portraying
to the reader what the HOL logic is. This is a valuable document, making
crystal clear in minute detail exactly what the HOL logic is meant to be.
But it is not necessarily the best document to be reading for newcomers
wanting to get a good solid intuitive grasp.
By the way, I have a glossary of HOL terminology on my website which I think
will be of use to you, both in reading other documents about HOL, and as a
self-contained description of HOL (which can be read like an encyclopedia,
skipping between definitions). It tries to explain clearly, concisely and
consistently all the concepts that you need to know. Even though it is
written for HOL Zero, it applies to all HOL systems, and clearly states
where it is talking specifically about HOL Zero. Unfortunately it is only a
text document at the moment, but one day I will make it HTML if anyone shows
any interest in it. Get it here:
http://www.proof-technologies.com/misc/Glossary.txt
Mark.
on 13/8/12 5:18 AM, Bill Richter <rich...@math.northwestern.edu> wrote:
> Thanks, Michael! I will treat the Logic Manual as a true description of
the
> HOL in HOL Light, and I will try harder to read it. I have a lot of
trouble
> with your 3 sentences:
>
> Sets in HOL Light and HOL4 are predicates over their respective
> types. Types correspond to non-empty sets (as already discussed).
> So, because any predicate bounded above corresponds to a ZFC set,
> the sets in HOL do also correspond to ZFC sets.
>
> One question would be: how does HOL Light turn my code into ZFC FOL? That
> sounds like a tough question which I'm interested in, but it's not my real
> question. I need to talk about sets to my audience of mathematicians in
my
> paper I'll submit soon to the Amer Math Monthly. I have 3900 lines of
code
>
>
http://www.math.northwestern.edu/~richter/RichterHOL-LightMiz3HilbertAxiomGe
> ometry.tar.gz
> and I want to tell them something about which sets I'm using. My first 4
> lines of code are
>
> new_type("point",0);;
> new_type_abbrev("point_set",`:point->bool`);;
> new_constant("Between",`:point->point->point->bool`);;
> new_constant("Line",`:point_set->bool`);;
>
> I think that says I told HOL Light to define a set called point and two
> functions
> Between: point x point x point ---> {True, False}
> Line: P(point) ---> {True, False}
> These sets & functions will be specified more closely by my axioms. We
then
> (in our heads) define a "point" to be an element of point, and a "line" to
> be a subset of point (i.e. element of P(point)) which Line sends to True.
> I think my first axiom
> let I1 = new_axiom
> `! A B. ~(A = B) ==> ?! l. Line l /\ A IN l /\ B IN l`;;
> says that given two elements of the set point, there is a unique line
> containing them. I often write
> let A B C be point;
> I think that means that A, B and C are variables referring to "points",
and
> so (in our heads) we say that if
> Between A B C = True
> then the middle "point" is "between" the two outer "points".
> I have a definition
>
> let Interval_DEF = new_definition
> `! A B. open (A,B) = {X | Between A X B}`;;
>
> I think that says if A, B refer to two elements of a & a of the set point,
> then open (A,B) refers to the subset of point consisting of all "points"
> between a and a.
>
> Now is my interpretation of my own code correct? I'm happy to cite the
> Logic Manual in my paper, but need to give audience more to go on. Are
> there any examples in the Logic Manual that are as "concrete" as my
> description above? I'm not too worried right now about how HOL Light is
> able to prove my statements about such sets are actually true.
>
> I have technical questions about sets defined by {...}, whether they're
> abstractions or enumerations (thanks for the new terminology, Mark). My
> first theorem is
>
> let IN_Interval = prove
> (`! A B X. X IN open (A,B) <=> Between A X B`,
> REWRITE_TAC[IN_ELIM_THM; Interval_DEF]);;
>
> Here's the code in sets.ml for IN_ELIM_THM:
>
> let IN_ELIM_THM = prove
> (`(!P x. x IN GSPEC (\v. P (SETSPEC v)) <=> P (\p t. p /\ (x = t))) /\
> (!p x. x IN GSPEC (\v. ?y. SETSPEC v (p y) y) <=> p x) /\
> (!P x. GSPEC (\v. P (SETSPEC v)) x <=> P (\p t. p /\ (x = t))) /\
> (!p x. GSPEC (\v. ?y. SETSPEC v (p y) y) x <=> p x) /\
> (!p x. x IN (\y. p y) <=> p x)`,
> REPEAT STRIP_TAC THEN REWRITE_TAC[IN; GSPEC] THEN
> TRY(AP_TERM_TAC THEN REWRITE_TAC[FUN_EQ_THM]) THEN
> REWRITE_TAC[SETSPEC] THEN MESON_TAC[]);;
>
> Why do we have to work so hard to prove IN_Interval? I would have thought
> that the {...} definition in Interval_DEF just amounted to a lambda, so
> open (A,B) = {X | Between A X B}
> means that
> open (A,B) = \X. Between A X B
> With that lambda definition of open (A,B), my theorem IN_Interval looks
> really obvious, it just needs the first definition of sets.ml
>
> let IN = new_definition
> `!P:A->bool. !x. x IN P <=> P x`;;
>
> Are you & Mark saying that HOL Light has a more complicated definition of
{X
> | Between A X B}, one that requires the serious technicality of
IN_ELIM_THM?
> Can I just rewrite sets.ml myself with ordinary lambdas so that I don't
> need IN_ELIM_THM? I think my audience of mathematicians needs some
> explanation, and hoping you'll give me one.
>
> --
> 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
