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

Mario Carneiro di.gama at gmail.com
Thu Nov 6 06:45:58 UTC 2014

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).


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
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.gilith.com/opentheory/mailing-list/attachments/20141106/94277d9a/attachment-0001.html>

More information about the opentheory-users mailing list