[opentheory-users] New principle of constant definition

Joe Leslie-Hurd joe at gilith.com
Thu Nov 6 06:51:37 UTC 2014

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



More information about the opentheory-users mailing list