Thanks for correcting me, Mark! I'll look at your HOL Zero source code,
especially corethy.ml. I see my error now. From bool.ml:
let T_DEF = new_basic_definition
`T = ((\p:bool. p) = (\p:bool. p))`;;
The first = is an Ocaml =, but the 2nd =, the one we care about, is the
primitive HOL Light constant =.
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.
Thanks, that's a good explaination. BTW where is the constant = defined in HOL
Light? I see now that the line in bool.ml
override_interface ("<=>",`(=):bool->bool->bool`);;
just means that <=> is being defined as a synonym for = in this special case.
In general = has type A->A-bool.
--
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
