On 13/08/12 14:17, Bill Richter 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.
The easy answer is that HOL Light does not turn your code into ZFC FOL at all.
Not even a little bit. When you carry out a HOL proof, you use the proof
system
that is described in the Logic manual. That proof system doesn't even have to
treat implication and universal quantification as primitive. In particular, in
HOL Light, implication, and existential and universal quantification are
derived
notions. That means you can be sure that at the very bottom level, the proof
system is not doing the traditional FOL thing (involving modus ponens,
generalisation etc). Those proof principles are present in HOL, but as derived
notions.
As for my quoted paragraph, I hope it is just the 3rd sentence that is causing
you trouble. If you write a predicate on a HOL type (say (λn:num. n > 6)),
then
this is equal to the HOL "set" { n | n > 6 }. Now, in contrast, when you get
really fussy with FOL set theory, you're not allowed to write { n | n > 6 };
you
have to use the axiom of separation, and impose an upper bound. For my
example,
I might take the reals, or the integers or the natural numbers as my "bound".
I
don't need to do that in HOL because the type over which the predicate is
expressed is itself the bound.
> 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 ...
> 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?
Your interpretation of what you've written seems fine to me.
> I have technical questions about sets defined by {...}, whether they're
> abstractions or enumerations (thanks for the new terminology, Mark).
They can be either. The test is whether or not there's a set comprehension |
(bar) in there or not. If you write { x | P x }, you're defining an
abstraction. If you write { x; y; z }, that's an enumeration.
> 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.
I'm not sure quite how HOL Light's GSPEC and SETSPEC constants work (they're
different from HOL4's treatment of this syntax), but I imagine the
complications
are there only to allow for notations like
{ n + 1 | n > 6 }
where what appears to the left of the bar may be an arbitrary term. (This
notation is really just a nice way of writing an image construction of course.)
If you never use that notation, then it's certainly fine to just view
{ x | P x }
as a fancy way of writing (λx. P x). If you want to investigate, try the
following:
let t = `{ x | x > 4 }`;;
let (f,ab) = dest_comb t;; (* f will be the GSPEC constant *)
let (bv,bod) = dest_abs ab;;
(* etc; use dest_comb, dest_abs as necessary *)
Also try the same with more complicated comprehensions.
In this way, you can see past the pretty-printing and get at what is really
going on with that notation.
Michael
------------------------------------------------------------------------------
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
