Thank you Rob! I was hoping for someone to clear up my mistakes and teach
me something more about conservative extension :)
(I may come off sounding confident but usually I am not.)
Also, Bill if you're not using new_axiom, then sorry for any offence caused
by the tone of my previous email.
On Wed, Aug 1, 2012 at 8:29 AM, <[email protected]> wrote:
> 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
