<div dir="ltr"><div class="gmail_extra"><div class="gmail_quote">On Mon, Mar 10, 2014 at 4:09 PM, Rob Arthan <span dir="ltr"><<a href="mailto:rda@lemma-one.com" target="_blank">rda@lemma-one.com</a>></span> wrote:<br>

<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div style="word-wrap:break-word">John, Ramana, Scott Owens and I talked about this a few months ago. There was general agreement to adopt the new constant definition mechanism once someone had confirmed my informal proof of correctness with a formal proof. Ramana has done that now. It is certainly only a matter of time before I implement it in ProofPower. It would be nice to be able to extend my OpenTheory reader/writer to handle it at the same time. <div>

<div><div class=""><blockquote type="cite"><div dir="ltr"><div class="gmail_extra"><div class="gmail_quote"><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left-width:1px;border-left-color:rgb(204,204,204);border-left-style:solid;padding-left:1ex">

<div style="word-wrap:break-word"><div>

</div></div></blockquote><div></div><div>Well, I have proved something about it, but I'm not sure it is as strong as what your informal proof said (which was conservativity) ;) Nevertheless I expect to prove that soon.<br>

</div></div></div></div></blockquote><div><br></div></div>Great! Thanks for all your efforts on this.</div></div></div></blockquote><div><br></div><div>Further to this, I have just finished proving a semantic version of conservativity for the revised new_specification rule. That is: if you start in a context that has a model then update the context by making a new_specification, the resulting context still has a model. That's probably all I'll do. For the curious, the theorem can be found here: <a href="https://github.com/xrchz/vml/blob/master/hol-light/stateful/holSoundnessScript.sml#L391">https://github.com/xrchz/vml/blob/master/hol-light/stateful/holSoundnessScript.sml#L391</a> (although that link might not stay valid very long).<br>

</div></div></div></div>