[opentheory-users] article format wording about constants

[Joe Hurd]

Hi Ramana,

> What does the phrase "with definition ..." mean in the article format spec?
> In my opinion it doesn't add anything except potential confusion.

I agree that the "with definition ..." language is more confusing than
helpful, and I've removed it from the article format spec.

> However, notice the asymmetry: const takes 1 argument, constTerm takes
> 2, but var takes 2 arguments and varTerm takes 1. Surely constants
> should act more like variables?

This asymmetry is deliberate, and reflects a fundamental difference of
constants and variables. Constants are determined just by their name,
but variables are determined by their name and type. This is
illustrated by the theorems

|- !(v : 'a list) (v : bool list). P (v : 'a list) (v : bool list)

|- P (c : 'a list) (c : bool list)

Applying the type instantiation ('a |-> bool) to both results in

|- !(v : bool list) (v' : bool list). P (v : bool list) (v' : bool list)

|- P (c : bool list) (c : bool list)

where the two constants have been identified, but the two variables
have been kept separate.

> Also, it's not clear whether a "new constant" with the same name as a
> previously defined constant is allowed. I presume so.

This is left to the system, which must be careful to disallow

define `c = T`
define `c = F`
prove `T = F`

I believe all of the HOL theorem provers maintain a symbol table of
constants, and will not allow redefinitions with the same name. The
logical kernel of the opentheory tool stores the definition with the
constant, so will happily allow redefinitions with the same name
(because the two "c" constants above will be treated as different
constants).

Cheers,

Joe