[opentheory-users] Troubleshooting an article reader

[Rob Arthan]

Mario,

On 13 Oct 2014, at 22:13, Mario Carneiro <di.gama at gmail.com> wrote:

> Hi Rob,
> 
> On Mon, Oct 13, 2014 at 3:50 PM, Rob Arthan <rda at lemma-one.com> wrote:
> 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.
> 
> Well, there's no need to use the definition of ! : you could just write
> 
> (\a. (abs (rep a)) = a) = (\a. a = a)
> (\r. (P r) = ((rep (abs r)) = r)) = (\r. r = r)
> 
> and since now the variables are bound, you are free to use whatever dummies you like.

But that’s just expanding the definition of the connectives and it’s not very pretty.
(Strictly speaking, I don’t know whether it is expanding the definition of the
connectives or not, since you haven’t told me what the type of the second
variable called r is, and for technical reasons it is boolean in the definition
of T.)

>   
> 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).
> 
> I have no strong feelings or difficulty implementing either standard; rather, as Joe suggested, I find it inelegant to hard-code anything into the spec that isn't necessary. The problem isn't that I am forced to invent a dummy variable, and have to convert it - it's that I have to name it *something*, and since there had been no previous examples of hard-coded names, it was my mistake to interpret the "a" and "r" as dummy names (which is another way to avoid hard-coded names, although as it turns out it's not a viable solution in this case). What I'm trying to do is offload as much responsibility for variable naming into the proof as possible, so that the spec doesn't have to pull names like "a" out of a hat (which may or may not conflict with another variable, or may just not be good variable names for the proof if one has a particular naming convention in mind).
> 
> 
> 
> On Mon, Oct 13, 2014 at 4:52 PM, Rob Arthan <rda at lemma-one.com> wrote:
> 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?
> 

I misunderstood what was going on. I thought you were introducing dummy names
you had an existing implementation of something like defineConst that was forcing
you to use invented variable names. I didn’t realise you had a choice.


> For comparison purposes (and for a glimpse of where I'm coming from), Metamath does this for *every* axiom and theorem. For example, there is a theorem http://us.metamath.org/mpegif/rabid2.html, written in Metamath as:
> 
>     |- ( A = { x e. A | ph } <-> A. x e. A ph )
> 
> and which could be translated into HOL as
> 
>     |- ((a = (\x. (a x) /\ (P x))) = (!x. (a x) ==> (P x)))
> 
> When applied as a step in another theorem, the stack machine accepts the label "rabid2" as the command, and treats it as if it were a primitive inference rule which pops "var v", "class B", "wff ps" off the stack (equivalents to "var" and "term" stack entries - here v is an arbitrary variable and B stands for any valid class expression, and ps is any valid wff), and pushes the theorem
> 
>   |- ( B = { y e. B | ps } <-> A. y e. B ps )
> 
> onto the stack. The original (non-substituted) formula, which had previously been exported, never appears on the stack at any point. Thus Metamath is essentially "subst"-ing every single formula that appears on the stack, which on the one hand makes it very powerful, but it does not actually contain a "subst" command, so a formula already on the stack cannot be further substituted unless you get a fresh copy from whatever formulas you derived it from or break off a new lemma.
> 
> Metamath has nothing hardcoded at all, not even "primitive rules of inference", just this "subst"-like behavior, and axioms which are specified during execution. That's part of the reason why I internally reject having to make arbitrary decisions regarding variable naming which should rightly be done by the proof writer and their own naming sense.

Unfortunately that is just not how it is in HOL Light.
The way the equivalent of defineTypeOp is implemented in HOL4
and ProofPower gives a defining property with no free variables.
But the HOL4 and ProofPower kernels require that the logical
connectives and one or two other constants are pre-defined.
The HOL Light and OpenTheory kernels don’t make this
requirement, but this causes them to produce defining properties
for type with free variables. I am rather inclined to agree with
you that the names of those free variables should be the user’s
choice. But that is not how HOL Light is at the moment.

Regards,

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