[opentheory-users] new_specification

[Ramana Kumar]

On Mon, Mar 10, 2014 at 4:09 PM, Rob Arthan <rda at lemma-one.com> wrote:

> 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.
>
>  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.
>
>
> Great! Thanks for all your efforts on this.
>

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:
https://github.com/xrchz/vml/blob/master/hol-light/stateful/holSoundnessScript.sml#L391(although
that link might not stay valid very long).
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.gilith.com/opentheory/mailing-list/attachments/20140311/55f30b45/attachment.html>