<html><head><meta http-equiv="Content-Type" content="text/html charset=windows-1252"></head><body style="word-wrap: break-word; -webkit-nbsp-mode: space; -webkit-line-break: after-white-space;">Joe,<div><br></div><div><div><div>On 13 Oct 2014, at 21:19, Joe Leslie-Hurd <<a href="mailto:joe@gilith.com">joe@gilith.com</a>> wrote:</div><br class="Apple-interchange-newline"><blockquote type="cite">Hi Rob,<br><br>You're right, "a" and "r" are not dummy free variables, but rather<br>hard-coded free variables in the rule. At present the only hard-coded<br>names in the OpenTheory spec are the names of the primitive symbols,<br>so this seemed a little inelegant to me.<br><br>However, I accept your point that it complicates the spec (because<br>readers have to implement the behaviour for both versions) and doesn't<br>solve a real problem, so the proposed change may not be worth it.<br><br></blockquote><div><br></div>For now, the only system we have to cope with that produces defining</div><div>properties with free variables is HOL Light and it does this for type</div><div>definitions only and it uses the fixed names “a” and “r” for the free variables. </div><div>I appreciate, on reflection, that if it did generate fresh variable names, it</div><div>would be a (not insuperable) challenge to implement an OpenTheory writer for it.</div><div>On the other hand, why would anyone want a definitional principle that</div><div>gave defining properties containing unpredictable free variable names?</div><div><br></div><div><blockquote type="cite">The easiest way of accessing version 5 of the article spec is to<br>follow the link at the bottom of version 6, but here's the direct link<br>for posterity:<br><br><a href="http://www.gilith.com/research/opentheory/article-5.html">http://www.gilith.com/research/opentheory/article-5.html</a><br></blockquote></div><br></div><div>Thanks. I did look at the end of version 6 and don’t know how I</div><div>managed not to spot the link there.</div><div><br></div><div>Regards,</div><div><br></div><div>Rob.</div></body></html>