[opentheory-users] new_specification

[Magnus Myreen]

On 12 March 2014 07:25, Ramana Kumar <ramana at member.fsf.org> wrote:
> 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).

This link might stay valid for longer:

https://github.com/xrchz/vml/blob/d3f84400361838ad28423168c0ecb3f0569aa244/hol-light/stateful/holSoundnessScript.sml#L391

> _______________________________________________
> opentheory-users mailing list
> opentheory-users at gilith.com
> http://www.gilith.com/opentheory/mailing-list
>