[opentheory-users] new_specification

[Joe Leslie-Hurd]

I have thought about this some more, and I believe I have answered my own
questions.

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.

2. I think my simplification is bogus because defining the c_i in terms of
c can fail because of the type variable condition.

I've created a draft standard article format at

http://www.gilith.com/research/opentheory/article.html

with the proposed new commands (native and version) highlighted. Please
take a look and let me know what you think.

Cheers,

Joe


On Fri, Mar 14, 2014 at 10:07 AM, Joe Leslie-Hurd <joe at gilith.com> wrote:

> 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.
>
> 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.
>
> 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:
>
> 1. The exact wording in RA2 is "The condition on type variables imposed by
> new specification is
> 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?
>
> 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:
>
> (i) Define c: v = (t_1,t_2,...,t_n) |- P[FST v, FST (SND v), ... SND (...
> (SND v))]
>
> (ii) Define the family of constants c_1, ..., c_n:
>
> v_1 = FST c |- v_1 = FST c
> v_2 = FST (SND c) |- v_2 = FST (SND c)
> ...
> v_n = SND (... (SND c)) |- v_n = SND (... (SND c))
>
> (iii) Derive |- P[c_1, c_2, ..., c_n]
>
> 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).
>
> 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.
>
> Cheers,
>
> Joe
>
>
>
> On Tue, Mar 11, 2014 at 1:36 PM, Magnus Myreen <magnus.myreen at cl.cam.ac.uk
> > wrote:
>
>> 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
>> >
>>
>> _______________________________________________
>> opentheory-users mailing list
>> opentheory-users at gilith.com
>> http://www.gilith.com/opentheory/mailing-list
>>
>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.gilith.com/opentheory/mailing-list/attachments/20140314/dc685baa/attachment-0001.html>