[opentheory-users] Troubleshooting an article reader

[Mario Carneiro]

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.


> 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?
>

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.

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