Hi Bill, Have you tried looking at the HOL Zero source code? I think you will find it illustrative for your purposes. It has a simple core like HOL Light, but the source code explains more of what is going on. In file 'corethy.ml' I try to motivate the axioms and constant definitions used in the axiomatisation. I try to use terminology as carefully as possible, and to define everything precisely in the bundled HOL glossary, although I'm always looking for suggestions for improvements (it's changed a lot over the years, thanks to the suggestions of Rob, John and others). And all derived theorems and inference rules (e.g. in bool.ml') have annotations in comments that explain what is going on in the derivation (although I've just spotted a couple of theorems that don't).
HOL Zero has a different axiomatisation of the HOL logic than the one used in HOL Light and the one used in HOL4 and ProofPower. In a nutshell, it is the same as HOL4 with the same primitive constants, except that it has 3 basic primitive inference rules (EQ_MP, INST and MK_COMB) in place of the rather complicated SUBST (making it close to HOL Light's set of primitive inference rules), and that it derives BOOL_CASES_AX (using the Beeson-like proof) instead of IMP_ANTISYM_AX (whereas HOL Light derives both). So it's axiomatisation is between that of HOL4 and HOL Light, but somewhat closer to HOL4's "classic" axiomatisation that HOL Light's. Best, Mark. The source code comments explain a of what is going on. on 21/3/14 6:19 AM, Bill Richter <rich...@math.northwestern.edu> wrote: > 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 > > > ------------------------------------------------------------------------------ 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
