Thanks, John and Rob! The main problem I'm having is actually embarrassingly simple: I don't understand the typed Lambda Calculus angle in Church's work or HOL. Now I definitely see the point of having functions as well as sets, and that means that the HOL type theory (sets are either types or terms of type alpha->bool) is superior to ZFC (which only has sets, so functions are really the graphs of what we think the functions are---massive inconvenience). And once you have functions, the Lambda Calculus is right there, and we'll definitely need both alpha- and beta-reduction, and we ought to prove that e.g. beta reduction is well-defined on alpha-equivalence classes.
But somehow I think that there's a much more interesting Lambda Calculus angle which I'm guessing Church understood himself. I'm guessing that all the PL (Propositional Logic, part of the edifice of FOL that's assumed by ZFC) we need is easily handled by Church's typed Lambda Calculus! Presumably that's how we prove things like BOOL_CASES_AX, because the HOL4 dox are quite clear that the only PL "axioms" they take are really definitions of ∀, ∃, T, F etc. I'm embarrassed to not know any of this LC-implies-PL work myself. I'm not sure how important I think this LC-implies-PL work is. If I understood it, I'm sure I'd say it was elegant mathematics, and that it's good we're assuming the weakest possible set of axioms. But then I think I'd also say that what really matters is the type theory that allows us both sets and functions, and not the elegant LC formulation that means we don't have to assume any PL axioms. RDA> Concerning beta-conversion ... You don’t need anything other than RDA> Tom’s 10 rules. Thanks, Rob. I'll study your proof of BOOL_CASES_AX. RDA> Note that he doesn’t give a schematic presentation of the last RDA> two rules that let you substitute for type and term variables, so RDA> they are easy to miss. Ah, and I had missed it, until I saw it in the HOL4 dox. It strikes me that I've often been befuddled writing code in that I don't quite understand what the type and term substitution rules actually are. Do you feel you do a good job in your dox explaining these matters? ProofPower can't really be that different theoretically from HOL4 and HOL Light, right? -- Best, Bill ------------------------------------------------------------------------------ Learn Graph Databases - Download FREE O'Reilly Book "Graph Databases" is the definitive new guide to graph databases and their applications. Written by three acclaimed leaders in the field, this first edition is now available. Download your free book today! http://p.sf.net/sfu/13534_NeoTech _______________________________________________ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
