Thanks, Konrad! You seem to agree with me here, that the typed-LC-implies-FOL isn't actually important:
My personal feelings on this foundational aspect are that the actual set of axioms isn't that important provided the usual introduction and elimination rules of predicate calculus can be derived from them. Now you're encouraging me to go read Church's typed LC paper more carefully, and see if I can work out the apparent difference between Church and what I quoted Andrews as saying about Church: My recollection (don't have citations to hand) is that Church originally wanted the untyped lambda calculus to serve as a foundation for logic, but that was discovered to be inconsistent. Something like Russell's paradox would be easy to code up in it. However, the simply typed lambda calculus worked better, i.e., it supports the derivation of the expected FOL-like rules, as we see in HOL theorem provers, and it is sound. Here's a some dumb questions about HOL4 and HOL Light. On p 29 of LOGIC, you write that there are constants Tbool, ∀(α→bool)→bool etc. Why aren't there colons? I would have written that as T:bool and ∀:(α→bool)→bool Are the apparent subscripts supposed to indicate colons, or does HOL4 not use colons for type annotations? I'm having trouble seeing your derivation of the expected FOL-like rules in HOL Light. Is there a paper where somebody explained these HOL derivations, or is it perhaps easier to understand in HOL4? Tom Hales writes on p 6 of http://www.ams.org/notices/200811/tx081101370p.pdf The system [HOL Light] has only two primitive constants. One of them is the equality symbol (=) of type :A->A->bool. So = is primitive, and p 5 lists the HOL Light axioms about the properties of =. Let's try to find this in the HOL Light sources. In hol_light/bool.ml it seems to me that first the type bool is defined, then = and <=> are defined to have type bool->bool->bool and to be the same as each other, then T is defined as let T_DEF = new_basic_definition `T = ((\p:bool. p) = (\p:bool. p))`;; That's your first HOL axiom on p 29 (again without colons): T = ((λxbool . x) = (λxbool . x)) So it looks to me that HOL Light is defining Tom's primitive = in terms of the Ocaml =. Is that correct? And maybe that just means that the HOL Light primitive = is "represented" in Ocaml as the ordinary =? -- 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
