<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="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 class="HOEnZb"><div class="h5">On 12 March 2014 07:25, Ramana Kumar <<a href="mailto:ramana@member.fsf.org">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">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 class="HOEnZb"><div class="h5"><br>
> _______________________________________________<br>
> opentheory-users mailing list<br>
> <a href="mailto:opentheory-users@gilith.com">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">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>