How to call it?
| Newsgroups | gmane.comp.mathematics.mizar |
|---|---|
| Message-ID | <[email protected]> |
Fixed variables are called sometimes local constants. 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? 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. So I use 'bound variables'. On the other hand fixed variables are also bound, by proof constructors. Regards, Andrzej