[opentheory-users] definition of "new" constants?

[Joe Leslie-Hurd]

Hi Gunter,

> O.K. (But it appears more like a object-oriented feature to me:
> nothing is equal unless one explicitly defines it to be equal).

I'd highly encourage that view: if you only build objects once and
store them in a dictionary if they are used multiple times, then
equality will be nice and boring.

> Two more questions:
> 1) If I create several constants with name c
> (and the same type bool) by a sequence of const+constTerm commands,
> are they equal (alpha-equivalent) to each other?
> (Like "T" and "T"?)

Yes: these will be equal.

> 2) If I define two constants c with the defineConst command
> with the *same* definition, are they considered equal?

This is implementation-dependent. Some theorem proving systems will
not allow you to define two constants with the same name, some will
allow it if the definitions are equal, and some (like opentheory) will
be fine with it and will give equal constants if the definitions are
equal.

> In any case, I think the documentation needs some clarification,
> in particular here:
>
> const
>     Higher order logic constants, such as T and =.
>     *Constants are identified by name*
>
> It seems rather that the name acts merely as a comment in the above cases.

I agree that this is unclear, in the light of the above examples. For
now I have removed the confusing part you have highlighted.

Cheers,

Joe