<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;"><div>Mario, Joe,</div><div><br></div><div><div><div>On 13 Oct 2014, at 16:54, Joe Leslie-Hurd <<a href="mailto:joe@gilith.com">joe@gilith.com</a>> wrote:</div><br class="Apple-interchange-newline"><blockquote type="cite">Hi Mario,<br><br><blockquote type="cite">The only<br>conclusion I can draw is that dummy variables should never be generated in a<br>formula where they would appear free, since there are no means to eliminate<br>them. I'm surprised, then, that a and r aren't quantified in the outputs to<br>defineTypeOp, because if they were you could use dummy variables rather than<br>hardcoding the strings "a" and "r" into the implementation.<br></blockquote><br></blockquote>@Mario:</div><div><br></div><div>The reason they aren’t quantified is because OpenTheory follows HOL Light</div><div>in not wiring any dependency on the definitions of the logical connectives and</div><div>quantifiers into the logical kernel. This means that they both have to represent</div><div>the logical content of a the defining property of a new type without using</div><div>universal quantification and implication, which they do using a theorem with</div><div>assumptions and free variables. It would be really nice if there was a simple</div><div>closed formula you could use instead, but no-one has come up with one.</div><div><br></div><div><blockquote type="cite">I agree with your assessment that dummy free variables are a scourge,<br>and therefore in version 6 of the article standard I propose changing<br>the behaviour of defineTypeOp to take the names of the "a" and "r"<br>variables as additional arguments:<br></blockquote><div><br></div>@Joe:</div><div><br></div><div>I have no strong objection to your proposal, but I don’t understand the reasons</div><div>for it. My understanding of defineTypeOp in version 5 of the article standard</div><div>was that the names of the variables in the theorem it produced were</div><div>“r” and “a” (not dummies). So the onus is on an OpenTheory reader to make it so</div><div>(by applying derived rules to the output of their “native” type definition principle</div><div>to give what the OpenTheory article spec requires).</div><div><br></div><div>What you are now proposing makes it clearer that an OpenTheory reader</div><div>has to have the capability to produce a defining property with any chosen</div><div>variable names, but I don’t see what value it adds. It just gives a tiny extra</div><div>burden to the implementor of an OpenTheory reader.</div><div><div><br></div></div><div><blockquote type="cite"><br><a href="http://www.gilith.com/research/opentheory/article.html#defineTypeOpCommand">http://www.gilith.com/research/opentheory/article.html#defineTypeOpCommand</a><br><br>The nice thing is that literally any variable name will work, because<br>the two resulting theorems of defineTypeOp each have precisely one<br>free variable, so there's nothing to clash with. It's easy to recover<br>the legacy version 5 behaviour by simply passing in the names "a" and<br>"r".<br><br>Does that satisfy your concerns? I believe that's the only instance in<br>the spec of dummy free variables, but please let me know if that's not<br>the case.<br></blockquote><div><br></div>@Joe:</div><div><br></div><div>To reiterate, I don’t see why you think the spec required or suggested</div><div>the introduction of dummy free variables. And I don’t see how it will</div><div>help Mario - if his implementation of defineTypeOp produces a theorem</div><div>with dummy variable names, then he will have to implement a derived rule to</div><div>adjust those names to the ones specified in the article (as opposed to “a” and</div><div>“r”, which is what you have to do with version 5 of the article standard).</div><div><br></div><div>By the way, is the version 5 of the article standard available on-line.</div><div>I have a paper copy somewhere, but it would be nice to have it available</div><div>on-line for comparison with version 6.</div><div><br></div><div>Regards,</div><div><br></div><div>Rob.</div><div><br></div><div><br></div></div></body></html>