On Mon, Sep 3, 2012 at 6:36 AM, Bill Richter
<[email protected]>wrote:
>
> 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.
There is a syntactic side of the story and a semantic side, just as with
FOL.
> All variables have a type, and the types are generated by the type
> constants bool, ind and ->,
New types can be defined, as you say below: not all of them are generated
by bool, ind, and -> (depending on what you mean by "generated").
> 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.
Not sure what you mean by "heavy typed". HOL is "simply typed lambda
calculus", and that is a standard term.
> We can also define recursive functions in LC with the Y combinator.
The Y combinator doesn't work in simply typed calculus (it is untypeable).
Support for recursive functions is developed differently (using recursive
types).
> The rules of inference are quite simple, and hover around the LC alpha and
> beta reduction,
alpha reduction is usually built into the syntax (it is invisible to the
inference rules). beta reduction is an inference rule, though.
> 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.
I'm not sure that it could. Certainly you don't have to mention "lambda
calculus", but you're going to have to describe something isomorphic to it
in explaining what the terms of your proof system are.
>
> 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.
Here is my attempt at an analogy. Does it match up with yours? I'm not sure.
FOL | HOL
(syntax) | (syntax)
variables | (typed) variables
terms | (simply typed) terms
function symbol | constant with function type
predicate symbol | constant with type whose range is bool
formulas | terms of type bool
(semantics) | (semantics)
domain | type
interpretation | definition of constants
Hmm this is turning more into an embedding of FOL into HOL... I'm not sure
how strong the analogy really is...
An important things I think missing from your analogy (or comparison),
though, is the definition of types and constants. In FOL do you just use
abbreviations, or is there a notion of definition that is logically visible?
>
> 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.
>
The property of product types you wrote above is guaranteed by the
definition of product types. It is not part of the logical foundation, but
rather is carefully ensured by JRH or whoever wrote the theory of pairs as
definitions of new types and constants above the basic logical foundation.
One is free to define another type of "pairs" that doesn't have that
property, but it wouldn't be useful as a product type.
>
> --
> 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
