[opentheory-users] Troubleshooting an article reader

[Rob Arthan]

Joe,

On 13 Oct 2014, at 21:19, Joe Leslie-Hurd <joe at gilith.com> wrote:

> Hi Rob,
> 
> You're right, "a" and "r" are not dummy free variables, but rather
> hard-coded free variables in the rule. At present the only hard-coded
> names in the OpenTheory spec are the names of the primitive symbols,
> so this seemed a little inelegant to me.
> 
> However, I accept your point that it complicates the spec (because
> readers have to implement the behaviour for both versions) and doesn't
> solve a real problem, so the proposed change may not be worth it.
> 

For now, the only system we have to cope with that produces defining
properties with free variables is HOL Light and it does this for type
definitions only and it uses the fixed names “a” and “r” for the free variables. 
I appreciate, on reflection, that if it did generate fresh variable names, it
would be a (not insuperable) challenge to implement an OpenTheory writer for it.
On the other hand, why would anyone want a definitional principle that
gave defining properties containing unpredictable free variable names?

> The easiest way of accessing version 5 of the article spec is to
> follow the link at the bottom of version 6, but here's the direct link
> for posterity:
> 
> http://www.gilith.com/research/opentheory/article-5.html

Thanks. I did look at the end of version 6 and don’t know how I
managed not to spot the link there.

Regards,

Rob.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.gilith.com/opentheory/mailing-list/attachments/20141013/42b9d6ef/attachment.html>