[opentheory-users] Finalizing version 6 of the article file format standard

[Mario Carneiro]

Oh wow, that's a pretty direct derivation of extensionality from my version
of defineTypeOp. I stand corrected; certainly it's not desirable to have a
"conservative extension" allow the derivation of an axiom before its
introduction. And I guess that the next best thing if you want to maintain
conservativity is exactly your version of the axiom.

Mario

On Thu, Nov 6, 2014 at 2:16 AM, Joe Leslie-Hurd <joe at gilith.com> wrote:

> Hi Mario,
>
> As you say, extensionality is an axiom of the system, but the use of
> it is explicitly tracked. For example, you can see which theorems in
> bool theory depend on it using the following command:
>
> opentheory info --theory --show-assumptions --show-derivations bool
>
> If defineTypeOp produced this:
>
> ⊦ p = (\r. rep (abs r) = r)  (1)
>
> then you could apply appThm, betaConv and absThm to get:
>
> ⊦ (\r. p r) = (\r. rep (abs r) = r)  (2)
>
> and then sym and trans using (1) and (2) to get
>
> ⊦ (\r. p r) = p  (3)
>
> which is an untracked application of extensionality for any non-empty
> predicate p. It seemed more elegant to reformulate the theorem to
> avoid this possibility.
>
> Cheers,
>
> Joe
>
> On Wed, Nov 5, 2014 at 10:45 PM, Mario Carneiro <di.gama at gmail.com> wrote:
> > I was aware that equation (1) is stronger than (2) without
> extensionality,
> > but I'm curious why this is a problem, since it is an axiom of the system
> > and doesn't require proof. Any v5 proof that starts with (2) can easily
> be
> > rebuilt to use (1), while conversely for a v6 proof there are very few
> > theorems that follow from (1) but not (2) in the absence of
> extensionality
> > (mostly trivial restatements of (1) itself), and I expect that any proof
> > that starts from (1) will immediately wrap it with appThm, upon which
> point
> > it will again be equivalent to (2).
> >
> > Mario
> >
> > On Thu, Nov 6, 2014 at 1:31 AM, Joe Leslie-Hurd <joe at gilith.com> wrote:
> >>
> >> Now that there is a release of the opentheory tool for processing
> >> version 6 articles, and I am sitting on a release of the standard
> >> theory library that uses version 6 articles, I'd like to finalize
> >> version 6 of the article file format standard, which is currently in
> >> draft mode:
> >>
> >> http://www.gilith.com/research/opentheory/article.html
> >>
> >> The commands that are new in version 6 are highlighted in yellow and
> >> the command with changed semantics (defineTypeOp) is highlighted in
> >> red. We have discussed the changes on this list, so there shouldn't be
> >> any surprises in store.
> >>
> >> Actually, there is one minor change that hasn't been discussed before.
> >> During implementation work on defineTypeOp I discovered that one of
> >> Mario's proposed theorems
> >>
> >> ⊦ p = (\r. rep (abs r) = r)  (1)
> >>
> >> required the axiom of extensionality to be logically equivalent to the
> >> same theorem produced by version 5 of defineTypeOp:
> >>
> >> ⊦ p r = (rep (abs r) = r)  (2)
> >>
> >> Although it would be theoretically possible to invoke the axiom of
> >> extensionality to convert between the two versions of defineTypeOp, I
> >> thought it was more elegant to reformulate theorem (1)
> >> by eta-expanding p:
> >>
> >> ⊦ (\r. rep (abs r) = r) = \r. p r  (3)
> >>
> >> [I also flipped the LHS and RHS so that theorem (3) has a pleasing
> >> similarity to the other theorem produced by defineTypeOp.] Now theorem
> >> (3) is logically equivalent to theorem (2) without requiring the axiom
> >> of extensionality, and retains the desirable property of having no
> >> free term variables.
> >>
> >> Anyway, there are no other "brown bag updates" to the standard, and
> >> I'd like to finalize it so we can start using it for real work.
> >>
> >> Does anybody have any objections or last-minute additions?
> >>
> >> Cheers,
> >>
> >> Joe
> >>
> >> _______________________________________________
> >> 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
> >
>
> _______________________________________________
> 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/20141106/b4351c58/attachment.html>