Ramana, > new_type and new_constant add new types and new constants to HOL > by fiat.
What these functions do is introduce new names into the available vocabulary (or signatures and type signatures to use the terminologies of the LOGIC manual). This is a conservative extension mechanism. For new_constant, it is equivalent to a constant_specification with defining property T. new_type has no equivalent in terms of type_specification, because when it imposes no restriction on the cardinality of the new type, so it really ought to be in the LOGIC manual. > I > suppose you must characterise them with new_axiom. This is not true. IF all you need to know of a types is that it is non-empty or of a constant that it has a given type, then you have no need to use new_axiom in conjunction with new_type and new_constant. This is precisely what Bill is doing, I believe. It is not very common to work like this, because the theory you get is not very suitable for reuse. It is more common to use type variables for unknown types and variable parameters for unknown objects, so that they can be instantiated to particular models. However, working with the unspecified types and constants you get from new_type and new_constant is a perfectly good approach and can be clearer if the theory you want is just intended as a thing to be read and appreciated in its own right. > The HOL Logic Manual does not mention new_type because one of its aims is > to build a model of HOL in set theory to give confidence that HOL is > sound. > Once you use new_type or new_constant or new_axiom, the model described in > the manual is no longer guaranteed to exist. What you say about new_axiom is true. Once you use new_axiom, it is down to you do produce some argument of your own as to the consistency of the resulting system. What you say about new_type or new_constant is wrong, see above. Regards, Rob. ------------------------------------------------------------------------------ Live Security Virtual Conference Exclusive live event will cover all the ways today's security and threat landscape has changed and how IT managers can respond. Discussions will include endpoint security, mobile security and the latest in malware threats. http://www.accelacomm.com/jaw/sfrnl04242012/114/50122263/ _______________________________________________ hol-info mailing list [email protected] https://lists.sourceforge.net/lists/listinfo/hol-info
