I think I finally understand the relationship between HOL and ZFC/FOL, after
thinking about p 5 of Tom Hales's Notices article
www.ams.org/notices/200811/tx081101370p.pdf, at least in the monomorphic case.
It will take me a while to get the details straight, and I hope folks here
(Michael & Konrad especially) will help me straighten this out. I think to
bring mathematicians into the formal proofs revolution, some documentation like
this is needed. So:
Math folks more or less understand ZFC/FOL: ∀, ∃, ¬, ∧, ∨, ⇒,⇔, axioms, rules
of inference, syntactic proofs we can check on the computer, the f.o. ZFC
axioms. A model of ZFC is a big enough collection of sets, but you don't need
a model to check syntactic ZFC proofs on the computer. HOL must have a similar
description! And it goes like this, I think:
HOL can be understood completely as syntax. All variables have a type, and the
types are generated by the type constants bool, ind and ->, as Tom writes, but
we surely need a compound type for products as well, the prod/# of
HOL4/HOL-Light. We can also define our own type constants (John defined point,
Between and === for me).
HOL involves heavy typed LC (partly explained in Chris Hankin's yellow book
Lambda Calculi), because all variables are typed, and also because we can
define ∀, ∃, ¬, ∧, ∨, ⇒ and ⇔ in LC. We can also define recursive functions in
LC with the Y combinator. The rules of inference are quite simple, and hover
around the LC alpha and beta reduction, and the more complicated inference
rules are then given by LC. That's all very elegant, and I can understand why
CS folks would do it, as LC was the first programming language, but HOL could
easily be explained without this cool typed LC.
The ZFC axioms (or as Rob corrects me, the ZC axioms) are partly encoded in the
type system (e.g. -> looks like the ZC power set axiom) but also in that a
subset of a type is defined by a function/expression (another ZC axiom) written
as a lambda abstraction. We can add in our own axioms with new_axiom.
That's the syntactic description of (monomorphic) HOL, which seems quite
analogous to ZC/FOL. Now we turn to semantics, which the HOL4 manual begins
with: take a huge set of sets U, the types are mapped to sets in U in a simple
way (in the monomorphic case), so type A -> B is mapped to the function space X
-> Y, where the sets X & Y are the elements in U which A & B map to, and an
abstraction is sent to the subset of it's type, the subset guaranteed by the ZC
axioms. So the semantics of HOL look very similar to the ZC semantics. The
main difference I see is that ZC has the bottom (emptyset) but not the top (U),
vice versa for HOL.
Isn't that a simple analogy between HOL and ZC/FOL? My guess is most folks
here understand this quite well. I don't know where this simple analogy is
documented. I'm very happy to finally understand it.
There are a number of holes in my understanding. Here's a very simple matter I
don't understand:
On p 15 of the HOL4 Logic manual, an application is written as
(t_{s1->s2} t'_{s1})_{s2}
That is, in order to form the application t t', there must exist types s1 and
s2 such that t has type s1->s2 and t' has type s1. Then t t' has type s2.
That's of course what we'd want, and something like that must be true
generally, e.g. for products, so (using the HOL Light convention), it must true
that if x has type t#t', then there must exist unique y and z of type t and t'
resp so that x = (y, z). I know this is true because I do it in HOL Light, but
I don't know where it's written down, or the various generalizations. I'm sure
it's well explained in the HOL4 manual, and I'll find it.
--
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
