Re: [mizar] How to call it?

[Josef Urban <josef.urban@gmail.com>]

2012/3/11  <trybulec@math.uwb.edu.pl>:
> Fixed variables are called sometimes local constants.

I have also seen eigenvariables and henkin/skolem constants. But I
doubt Jaskowski uses these names, perhaps "eigenvariable" could come
from Gentzen?

> Ground term is defined
> as
> 'a term that does not contain any variables at all' (Wikipedia).
>
> How to call a term that does not contain bound variables, but local
> constants
> are allowed?

locally ground/closed?

>
> The same goes for closed terms and so on.
>
> BTW How to call variables that are not fixed. I tried to use 'quantified
> variables'. It is O.K. in the case of variables bound by quatifiers, not so
> is they are bound by operators.

I would consult Jeff Pelletier and his ND overview:
www.sfu.ca/~jeffpell/papers/pelletierNDtexts.pdf .

That reminds me that we still have not found out if Discourse
Representation Theory (which was recently proposed by some for math
formalization) took inspiration (via the Montague/Tarski connection)
by Jaskowski's ND. That would be a funny circle :-).

Josef


>
> So I use 'bound variables'. On the other hand fixed variables are also
> bound, by proof constructors.
>
> Regards,
> Andrzej