Hi Bill, on 21/3/14 6:19 AM, Bill Richter <rich...@math.northwestern.edu> wrote:
> ... > > 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 =? No, not at all. The above is defining the constant 'T'. The constant '=' does not have a definition in HOL Light, or in any of the HOL axiomatisations. We have to start somewhere with entities that don't have definitions but are just declared. In HOL Light's axiomatisation, the only such entities are the 'bool' and 'fun' type constants and the '=' constant (the other axiomatisations also have the '==>' and '?' constants). In the logic, the meaning of such entities is not captured in definitions, but instead "drops out" from the aggregation of the axioms and primitive inference rules. Best, Mark. ------------------------------------------------------------------------------ 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
