[opentheory-users] Troubleshooting an article reader

[Rob Arthan]

Mario, Joe,

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

> Hi Mario,
> 
>> The only
>> conclusion I can draw is that dummy variables should never be generated in a
>> formula where they would appear free, since there are no means to eliminate
>> them. I'm surprised, then, that a and r aren't quantified in the outputs to
>> defineTypeOp, because if they were you could use dummy variables rather than
>> hardcoding the strings "a" and "r" into the implementation.
> 
@Mario:

The reason they aren’t quantified is because OpenTheory follows HOL Light
in not wiring any dependency on the definitions of the logical connectives and
quantifiers into the logical kernel. This means that they both have to represent
the logical content of a the defining property of a new type without using
universal quantification and implication, which they do using a theorem with
assumptions and free variables. It would be really nice if there was a simple
closed formula you could use instead, but no-one has come up with one.

> I agree with your assessment that dummy free variables are a scourge,
> and therefore in version 6 of the article standard I propose changing
> the behaviour of defineTypeOp to take the names of the "a" and "r"
> variables as additional arguments:

@Joe:

I have no strong objection to your proposal, but I don’t understand the reasons
for it. My understanding of defineTypeOp in version 5 of the article standard
was that the names of the variables in the theorem it produced were
“r” and “a” (not dummies). So the onus is on an OpenTheory reader to make it so
(by applying derived rules to the output of their “native” type definition principle
to give what the OpenTheory article spec requires).

What you are now proposing makes it clearer that an OpenTheory reader
has to have the capability to produce a defining property with any chosen
variable names, but I don’t see what value it adds. It just gives a tiny extra
burden to the implementor of an OpenTheory reader.

> 
> http://www.gilith.com/research/opentheory/article.html#defineTypeOpCommand
> 
> The nice thing is that literally any variable name will work, because
> the two resulting theorems of defineTypeOp each have precisely one
> free variable, so there's nothing to clash with. It's easy to recover
> the legacy version 5 behaviour by simply passing in the names "a" and
> "r".
> 
> Does that satisfy your concerns? I believe that's the only instance in
> the spec of dummy free variables, but please let me know if that's not
> the case.

@Joe:

To reiterate, I don’t see why you think the spec required or suggested
the introduction of dummy free variables. And I don’t see how it will
help Mario - if his implementation of defineTypeOp produces a theorem
with dummy variable names, then he will have to implement a derived rule to
adjust those names to the ones specified in the article (as opposed to “a” and
“r”, which is what you have to do with version 5 of the article standard).

By the way, is the version 5 of the article standard available on-line.
I have a paper copy somewhere, but it would be nice to have it available
on-line for comparison with version 6.

Regards,

Rob.


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