[opentheory-users] Troubleshooting an article reader

[Joe Leslie-Hurd]

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.

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

Cheers,

Joe

On Mon, Oct 13, 2014 at 12:50 PM, Rob Arthan <rda at lemma-one.com> wrote:
> 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.
>
>
>
> _______________________________________________
> opentheory-users mailing list
> opentheory-users at gilith.com
> http://www.gilith.com/opentheory/mailing-list
>