Re: [mizar] How to call it?

[trybulec@math.uwb.edu.pl]

Cytowanie 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"?

I believe it is the Mizar jargon, maybe the old Mizar MSE jargon. It is 
used in

'Mizar-MSE introduction to logic' by Marcin Mostowski
www.calculemus.org/MathUniversalis/3/most-tex.txt

but also in some new documents e.g.

The Mizar Mathematical Library in OMDoc: Translation and Applications
by Mihnea Iancu, Michael Kohlhase, Florian Rabe and Josef Urban
https://svn.omdoc.org/repos/latin/public/MizarOMDocAppl.pdf

It is rather surprising that it is still used in a comment to a Mizar error

# 138
Cannot identify a local constant, free in the default type

what means "there is no fixed variable with the same identifier as 
variable free in the reserved type"

We use still 'local constants' but with a different meaning, a constant
introduced by 'set' construction, like

     set c = the carrier of G;

> 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 inside expressions green.  So when I
> have to explain things to new users, I often just use the colors
> instead of funny terminology.

I believe that 'Skolem constant' should be used only for a variable introduced
by the Choice Statement like

        consider x such that x > y;

(and related constructions like 'reconsider', 'given').

Katuzi Ono in 'ON A PRACTICAL WAY OF DESCRIBING FORMAL DEDUCTIONS' 
constructions
that introduce fixed variables calls 'nominating quantifiers'. I do not 
remember if he coined a special name for variables introduced by them.

Regards,
Andrzej