The assumption seems to do the job provided that it has no free variables.
Then once proven it can be removed by modus ponens or other cut-like rule.
I'm not seeing a problem with type variables, though it's true they must
match in both parts of tm |- tm or |- tm --> tm.
-Cris
On Thu, Jul 19, 2012 at 9:20 AM, Konrad Slind <[email protected]>wrote:
> I wrote:
> >> It also suffers from the problem that a polymorphic formula
> >> assumed in this way can't be instantiated. Asserting an axiom
> >> is more powerful. In HOL4 axiom usage can be tracked in a similar
> >> way to how assumptions are propagated, so you can get the same
> >> effect as using an assumption.
>
> Cris then asked:
>
> > Could you explain for us relative beginners a bit more what you mean
> here? I
> > looked at the HOL Light code for PROVE_HYP, but the meaning and use are
> not
> > clear to me.
> >
> > And anyway I am wondering if you mean that asserting an axiom is more
> > powerful than _any_ ASSUME-like mechanism, or is somehow specific to
> > PROVE_HYP.
> >
> > Additional enlightenment will be much appreciated.
> >
> > -Cris
>
> One aspect of HOL that occasionally bites is that one needs to remember
> that type variables are subject to similar constraints as term variables.
> Suppose I want to ASSUME a formula containing a type variable, getting
> a theorem
>
> th = tm |- tm
>
> I won't be able to instantiate said type variable in the conclusion of th
> without also instantiating it in the hypotheses. On the other hand
>
> new_axiom("foo",tm)
>
> returns
>
> |- tm
>
> and you don't have that limitation to deal with. Of course, you've
> then got a new
> axiom roaming around and potentially obliterating the usefulness of your
> formalization.
>
> Konrad.
>
------------------------------------------------------------------------------
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
