[opentheory-users] new_specification

[Joe Leslie-Hurd]

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/95948841/attachment.html>