Re: [mizar] How to call it?

[Makarius <makarius@sketis.net>]

On Sun, 11 Mar 2012, trybulec@math.uwb.edu.pl wrote:

> Fixed variables are called sometimes local constants. Ground term is 
> defined as 'a term that does not contain any variables at all' 
> (Wikipedia).

Can you quote a source or authority for "fixed variables are called 
sometimes local constants"?

It happens to be my preferred terminology for the locally fixed entities 
(Isar: fix/fixes, Mizar: let), but I've forgotten where I've picked up the 
wording.  "Fixed variable" sounds like an oxymoron at first, but it nicely 
describes what it really is.

BTW, a fixed variable inside an Isar proof body is called "Skolem 
variable" or "Skolem constant", and is printed brown.  Outermost fixes are 
blue, bound variables insided expressions green.  So when I have to 
explain things to new users, I often just use the colors instead of funny 
terminology.


	Makarius