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

[Joe Leslie-Hurd]

With the demise of the theorem metadata proposal there are no open
features for version 6 of the article spec, and so I move to close the
spec and make it official. At this point any future development will
be for version 7 of the article spec.

If I don't hear any objections I'll do this in the next day or so and
release a version of the standard theory library in version 6 format.

Cheers,

Joe

On Wed, Nov 5, 2014 at 11:23 PM, Mario Carneiro <di.gama at gmail.com> wrote:
> 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
>
>
>
> _______________________________________________
> opentheory-users mailing list
> opentheory-users at gilith.com
> http://www.gilith.com/opentheory/mailing-list
>