[opentheory-users] New principle of constant definition

[Joe Leslie-Hurd]

Hi Rob,

> It would be sound to permit that, but I have a prejudice against
> free variables in defining properties, so I was deliberately requiring
> the user to take the universal closure w.r.t. the variable n in an
> example like the above, so that the resulting defining property
> would be a closed formula.

The aesthetic argument convinces me: I just wanted to check the
condition wasn't also necessary for soundness in some subtle way.

>> Also, why "contained in" and not "exactly"? If there are extra
>> variables v_i that are not free in p, then it is a simple matter to
>> remove them from the hypotheses before calling gen_new_specification.
>
> Yes, but then the rule won't introduce the corresponding constants.
> I don't think this is very important, but I didn't want to require
> the user to impose a constraint on all the new constants.

>From the perspective of a purely functional logical kernel introducing
a new constant with no defining property is a no-op, but in a
traditional logical kernel with a symbol table I can see there might
be a reason to introduce a new constant with a null definition.

>> Finally, a practical point that I ran into during implementation: in
>> the case where the set v_i is empty (i.e., there is nothing to
>> define), should the input theorem simply be returned or do you
>> consider that an error condition?
>
> The current ProofPower implementation allows the set to be empty
> and just stores the input theorem as a definition (of nothing) in that
> case. I think that is it how it is specified in the CakeML work too.
> Maybe Ramana could confirm that.

OK, I'll mirror this behavior in the opentheory tool. In this trivial
case the rule should succeed iff the input theorem has no free
variables.

Cheers,

Joe