On 11/08/2012, at 17:05, Bill Richter wrote:
> My main problem is that I don't understand HOL, so I don't know what theorems
> HOL Light is proving for me. The HOL4 Logic manual looks like a very
> respectable CS document, but I haven't been able to read it yet, and it's not
> a HOL Light do
Hi Bill,
There are a few points which you may or may not already realise. Sorry if
these are obvious, but I haven't been following the (very lengthy!) thread
in detail.
1. Just checking you understand this: In HOL Light and HOL4 (but not
ProofPower HOL), sets are represented as functions to boo
Hi Bill,
> ... My main problem is that I don't understand HOL, so I don't know what
> theorems HOL Light is proving for me. The HOL4 Logic manual looks like
> a very respectable CS document, but I haven't been able to read it yet,
and
> it's not a HOL Light document.
And it's not a particularly
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 a
Thanks, Mark! I looked at Tom Hales's Notices article, as you suggested
www.ams.org/notices/200811/tx081101370p.pdf
Now Tom is a great mathematician (he's the main reason I'm here), but Tom is
now an HOL Light expert, and I think mathematicians can't be expected to
understand him. He starts ou
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.
On 13/08/12 14:53, Bill Richter wrote:
> That sounds great, but here I want more details:
>
> The types are presented in the HOL Light System box.
>
> Terms are the basic mathematical objects of the HOL Light system. The
> syntax is based on Church’s lambda-calculus [to define functions
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
Hi Bill,
> Isn't this supposed to be about sets?
No, HOL is about types. Tom is informally explaining what the HOL logic is,
rather than explaining it in terms of some other formal notation (e.g. ZFC
set theory).
> Can you explain how the set abstraction/enumerations of sets.ml are
lambdas?
It
