I'm trying to understand Tom Hales's compact description of HOL Light in his AMS Notices article www.ams.org/notices/200811/tx081101370p.pdf The first things I don't understand are the type bool and the beta-conversion inference rule.
Isn't there an axiom that there are exactly two term type bool, T and F, both constants? I can't see where Tom says that, or where it's explained. Maybe this is the theorem EXCLUDED_MIDDLE from class.ml. I saw in bool.ml something else Tom didn't explain, which Michael N explained to me some time ago, how to define the universal quantifier: let FORALL_DEF = new_basic_definition `(!) = \P:A->bool. P = \x. T`;; That's pretty close to how Church defined the universal quantifier in his 1940 paper A Formulation of the Simple Theory of Types http://www.jstor.org/stable/2266170, with his primitive constant Pi. Church gives beta-conversion as an inference rule, and I think that's what HOL4 does as well. Here's from p 26 of LOGIC; http://sourceforge.net/projects/hol/files/hol/kananaskis-9/kananaskis-9-logic.pdf/download Beta-conversion [BETA CONV] (λx. t1 )t2 = t1 [t2 /x] • Where t1 [t2 /x] is the result of substituting t2 for x in t1 , with suitable renaming of variables to prevent free variables in t2 becoming bound after substitution. Tom (and I think HOL Light) only gives the very simple beta-conversion inference rule (λx. a) x = a Presumably you can deduce this from the Tom's primitive inference rules, or maybe you need the axiom of extensionality as well. I think it's proved in the HOL Light sources in equal.ml: (* ------------------------------------------------------------------------- *) (* General case of beta-conversion. *) (* ------------------------------------------------------------------------- *) let BETA_CONV tm = try BETA tm with Failure _ -> try let f,arg = dest_comb tm in let v = bndvar f in INST [arg,v] (BETA (mk_comb(f,v))) with Failure _ -> failwith "BETA_CONV: Not a beta-redex";; -- 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
