[opentheory-users] Finalizing version 6 of the article file format standard
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:
> 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?
> opentheory-users mailing list
> opentheory-users at gilith.com
-------------- next part --------------
An HTML attachment was scrubbed...
More information about the opentheory-users