<div dir="ltr">I have thought about this some more, and I believe I have answered my own questions.<div><br></div><div>1. The proposed definition mechanism is not more expressive than new_definition, because it can be simulated by first defining c_1 = t_1, ..., c_n = t_n, instantiating the given theorem with the substitution [c_1/v_1, ..., c_n/v_n], and then using the definition theorems of the c_i to prove the hypotheses. So I think the best thing is to keep the OpenTheory defineConst mechanism, and "compile" the proposed definition mechanism using the above scheme.</div>
<div><br></div><div>2. I think my simplification is bogus because defining the c_i in terms of c can fail because of the type variable condition.</div><div><br></div><div>I've created a draft standard article format at</div>
<div><br></div><div><a href="http://www.gilith.com/research/opentheory/article.html">http://www.gilith.com/research/opentheory/article.html</a><br></div><div><br></div><div>with the proposed new commands (native and version) highlighted. Please take a look and let me know what you think.</div>
<div><br></div><div>Cheers,</div><div><br></div><div>Joe</div></div><div class="gmail_extra"><br><br><div class="gmail_quote">On Fri, Mar 14, 2014 at 10:07 AM, Joe Leslie-Hurd <span dir="ltr"><<a href="mailto:joe@gilith.com" target="_blank">joe@gilith.com</a>></span> wrote:<br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div dir="ltr">I like the suggestions for changing the format, I'm making a new draft standard of the article format that I'll ask for feedback on shortly.<div>
<br></div><div>However, for right now I have a question about the new constant definition mechanism. Since OpenTheory has a purely functional logical kernel and there's no mechanism for accessing theorems that are not exported from a theory, I'm not really motivated by arguments arguing against a definition mechanism that permits unintended identities (RJ1). Naturally I require soundness (RJ2), and I would very much like a mechanism based on equality alone (JH1, RA1), but the current constant definition principle gives me that.</div>
<div><br></div><div>So for me the powerful argument for the new definition principle is the ability to define new constants that are currently undefinable due to a stronger than necessary condition on type variables (RA2). However, now I'm carefully reading the proposal, a couple of things occur to me:</div>
<div><br></div><div>1. The exact wording in RA2 is "The condition on type variables imposed by new specification is</div><div>stronger than one would like." But what about new_definition? Does that also have a stronger-than-necessary condition on type variables? Can you define constants using the proposed mechanism that cannot be defined using new_definition?</div>
<div><br></div><div>2. Assuming a positive answer to (1), I wonder whether the proposed mechanism can be simplified to a single variable (i.e., providing the input theorem v = t |- P[v] defines a new constant c and returns the theorem |- P[c]). Given a theory of pairs (which can be built with new_definition), you could then build the general proposed mechanism on top of this by the following three steps:</div>
<div><br></div><div>(i) Define c: v = (t_1,t_2,...,t_n) |- P[FST v, FST (SND v), ... SND (... (SND v))] </div><div><br></div><div>(ii) Define the family of constants c_1, ..., c_n:</div><div><br></div><div>v_1 = FST c |- v_1 = FST c</div>
<div>v_2 = FST (SND c) |- v_2 = FST (SND c)</div><div>...</div><div>v_n = SND (... (SND c)) |- v_n = SND (... (SND c))</div><div><br></div><div>(iii) Derive |- P[c_1, c_2, ..., c_n]</div><div><br></div><div>Because OpenTheory has a purely functional kernel and you can only access theorems that are exported a theory, the client will have no access to the "internal" constant c and the theorems derived in (i) and (ii).</div>
<div><br></div><div>I recognize there are arguments for the general proposed mechanism to be the primitive in the HOL theorem provers, but I'd very much like the simplest possible mechanism to be the primitive in OpenTheory, assuming it has the same expressive power.</div>
<div><br></div><div>Cheers,</div><div><br></div><div>Joe</div><div><br></div></div><div class="HOEnZb"><div class="h5"><div class="gmail_extra"><br><br><div class="gmail_quote">On Tue, Mar 11, 2014 at 1:36 PM, Magnus Myreen <span dir="ltr"><<a href="mailto:magnus.myreen@cl.cam.ac.uk" target="_blank">magnus.myreen@cl.cam.ac.uk</a>></span> wrote:<br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div><div>On 12 March 2014 07:25, Ramana Kumar <<a href="mailto:ramana@member.fsf.org" target="_blank">ramana@member.fsf.org</a>> wrote:<br>
> On Mon, Mar 10, 2014 at 4:09 PM, Rob Arthan <<a href="mailto:rda@lemma-one.com" target="_blank">rda@lemma-one.com</a>> wrote:<br>
>><br>
>> John, Ramana, Scott Owens and I talked about this a few months ago. There<br>
>> was general agreement to adopt the new constant definition mechanism once<br>
>> someone had confirmed my informal proof of correctness with a formal proof.<br>
>> Ramana has done that now. It is certainly only a matter of time before I<br>
>> implement it in ProofPower. It would be nice to be able to extend my<br>
>> OpenTheory reader/writer to handle it at the same time.<br>
>><br>
>> Well, I have proved something about it, but I'm not sure it is as strong<br>
>> as what your informal proof said (which was conservativity) ;) Nevertheless<br>
>> I expect to prove that soon.<br>
>><br>
>><br>
>> Great! Thanks for all your efforts on this.<br>
><br>
><br>
> Further to this, I have just finished proving a semantic version of<br>
> conservativity for the revised new_specification rule. That is: if you start<br>
> in a context that has a model then update the context by making a<br>
> new_specification, the resulting context still has a model. That's probably<br>
> all I'll do. For the curious, the theorem can be found here:<br>
> <a href="https://github.com/xrchz/vml/blob/master/hol-light/stateful/holSoundnessScript.sml#L391" target="_blank">https://github.com/xrchz/vml/blob/master/hol-light/stateful/holSoundnessScript.sml#L391</a><br>
> (although that link might not stay valid very long).<br>
<br>
</div></div>This link might stay valid for longer:<br>
<br>
<a href="https://github.com/xrchz/vml/blob/d3f84400361838ad28423168c0ecb3f0569aa244/hol-light/stateful/holSoundnessScript.sml#L391" target="_blank">https://github.com/xrchz/vml/blob/d3f84400361838ad28423168c0ecb3f0569aa244/hol-light/stateful/holSoundnessScript.sml#L391</a><br>
<div><div><br>
> _______________________________________________<br>
> opentheory-users mailing list<br>
> <a href="mailto:opentheory-users@gilith.com" target="_blank">opentheory-users@gilith.com</a><br>
> <a href="http://www.gilith.com/opentheory/mailing-list" target="_blank">http://www.gilith.com/opentheory/mailing-list</a><br>
><br>
<br>
_______________________________________________<br>
opentheory-users mailing list<br>
<a href="mailto:opentheory-users@gilith.com" target="_blank">opentheory-users@gilith.com</a><br>
<a href="http://www.gilith.com/opentheory/mailing-list" target="_blank">http://www.gilith.com/opentheory/mailing-list</a><br>
</div></div></blockquote></div><br></div>
</div></div></blockquote></div><br></div>