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

[Joe Leslie-Hurd]

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