[opentheory-users] type variable names

[Joe Hurd]

Hi Ramana,

Firstly, to conclude the discussion of type variable names (for now),
let's continue with the existing convention of beginning with an upper
case letter in the OpenTheory standard library and let theorem prover
implementations translate to their own conventions.

> (By the way, at risk of hijacking this thread, the
> convention seems to be violated in the theorems generated by
> defineTypeOp, specifically the "r" and "a" variables are free: is
> there a good reason for that?)

Secondly, I'll answer this question. The set of primitive inferences
in OpenTheory comes from HOL Light, and has the clean property that
the only primitive constant that is used is equality. Unfortunately,
binding "r" and "a" would also require a universal quantifier
constant, and so the primitive inference leaves them free.

For the sake of theory aesthetics we insist that all *exported*
theorems have no free variables (and no hypotheses), but theorems
proved in an article strictly for *internal* use are invisible and
thus can have free variables (or hypotheses).

Cheers,

Joe