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 out great:
Much day-to-day mathematics is written at a level of abstraction
that is indifferent to its exact representation as sets.
This layer of abstraction is good news, because it allows us to
shift from Zermelo-Fraenkel- Choice (ZFC) set theory to a different
foundational system with equanimity and ease.
HOL Light is a new axiomatic foundation with types, different from
the usual ZFC.
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]
What is a type? Compared to a set, I think. What is a term?
1. Types: The collection of types is freely generated from type
variables :A,:B,... and type constants :bool (boolean), :ind
(infinite type), joined by arrows
Isn't this supposed to be about sets? My code (largely written by John)
doesn't obviously obey Tom's rule:
new_type("point",0);;
new_type_abbrev("point_set",`:point->bool`);;
new_constant("Between",`:point->point->point->bool`);;
new_constant("Line",`:point_set->bool`);;
Maybe I need to read something by Church.
2. `{A,B}` is a set enumeration, not a set abstraction, so I'm not
sure why you are pointing to the definition of "INSERT" (which is
used in the representation of set enumerations) and then talking
about set abstractions.
Because it was about all that was explained about sets in the tutorial, and
because I was intrigued that INSERT was explicitly defined as a lambda in
sets.ml.
But anyway, any set enumeration or set abstraction is of course a
set, and, in HOL Light, any set is a function (as explained by 1.),
which is what a lambda is, so there should be no surprise that a
set abstraction/enumeration can be expressed as a lambda in HOL
Light.
Can you explain how the set abstraction/enumerations of sets.ml are lambdas?
Does HOL4 have anything comparable to sets.ml?
Sorry, I had two typos in my last post. I meant to say
let I1 = new_axiom
`! A B. ~(A = B) ==> ?! l. Line l /\ A IN l /\ B IN l`;;
says there is a unique "line" containing any two DISTINCT "points".
if A, B refer to "points" a & b, then open (A,B) refers to the
subset of point consisting of all "points" between a and b.
--
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
