Bill,
On Sun, Aug 12, 2012 at 9:53 PM, Bill Richter <[email protected]
> wrote:
> 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
>
Oooh. This item is talking about the syntax of the language. The concept of
"term" is also syntactic, the same thing as an expression in the
language. (These questions about types versus sets are wonderfully basic,
and it makes me happy to happy to see them asked by people other than me!)
Boolean-valued functions are sets. So \x. x < 3 is the set of integers less
than 3. As discussed, this is the same as {x | x < 3}. There are also sets
of sets. For example the set of all sets of integers containing exactly one
element is {S | size s = 1}.
In type theory, every value has a specific type as well as the ability to
be a member of various sets. And every expression in the language has a
(syntactic!) type, and the type of every expression is fully determined by
the types of the variables in constants in it. For example if the constant
T has type bool and the constant "==>" has type "function from bool and
bool to bool", then the expression "T ==> T" has type bool. For this
expression it is only necessary to see that it is an application of "==>"
to two arguments, but for lambdas there is slightly more syntactic
bookkeeping to be done. The language also has syntactic type checking, so
in this same example "T ==> T", the two input terms must have type bool or
the whole term is syntactically illegal.
It is customary to allow types of variables and constants to be omitted
when writing formulas in type theory where the types can be inferred by the
system. This is an important syntactic convenience.
Every syntactically correct expression in type theory can only produce
values that are of the type implied by the syntactic type of the
expression! And about the difference between types and sets, I prefer not
to say that a type is a set, because the set of all things having a type is
expressible as \x. T (or {x | T}. When explicit type annotation looks like
x:real or x:bool, then the set of all values of type bool is written as
{x:bool | T}.
It's helpful to look at Russell's paradox. It involves a set being or not
being a member of itself. In type theory syntax we would try to write "(X
X)". Fortunately in type theory this expression is syntactically illegal,
so Russell's paradox cannot be written.
Where in set theory the existence of a set must be proved, in type theory
many of these cases are no more than the syntactic type checking of the
expressions of your formulas. In type theory one could say that every value
expressible in a legal
Note also that in type theory there are things that are not sets! There are
integers, real numbers, booleans, functions from real numbers to real
numbers, sets of integers, and so on. This approach certainly fits basic
intuition.
Rob Arthan references Peter Andrews' textbook, which has been my entree
into type theory. That reminds me that online there are a couple of entries
in the Stanford Encyclopedia of Philosophy on type theory:
http://plato.stanford.edu/entries/type-theory/ by Thierry Coquand
(associated with Coq), and
http://plato.stanford.edu/entries/type-theory-church/ by Peter Andrews
Best regards,
Cris
>
> 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
>
------------------------------------------------------------------------------
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
