[mizar] Re: How to call it?

[Jesse Alama <jesse.alama@gmail.com>]

Josef Urban <josef.urban@gmail.com> writes:

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

"Eigenvariable" is used to describe a variable in an application of a
rule of inference for existential or universal quantifiers.  Since
fixed variables have a meaning beyond the single "rule application" by
which they are introduced, I would advise against "eigenvariable".

"Henkin constant", in the sense of Henkin's proof of the completeness
theorem for first-order logic, is not related to fixed variables.
Such constants are introduced to ensure that valid existential
formulas have witnesses in the term model.

I don't know "Skolem constant" as a synonym for "Henkin constant", so
I can't comment on that.  The sense I can give to "Skolem constant"
has to do with rewriting FOL formulas in 'equivalent' forms that lack
existential quantifiers.  Or maybe you're referring to the
"skolemization" trick used in the model theory of FOL by which any
complex formula can be considered atomic, but that's not related to
fixed variables, either, so far as I can see.

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

In addition to Josef's suggestions, I'll add "fixed term" and "local
term".

This issue comes up in the MML, I believe, in the Braselmann-Koepke
formalization of a proof of the completeness theorem for FOL.  They
use the name

  still_not-bound_in p ,

where p has the type QC_formula of A (and A has type QC-alphabet), to
refer to the set of bound variables of p that somehow avoid being
bound by any quantifier appearing in p.  They also define a notion of
fixed variable, but don't seem to use it.

Braselmann and Koepke were mizaring the proof found in Ebbinghaus,
Flum, and Thomas's _Mathematical Logic_, so perhaps you may find some
inspiration there in their setup of the language of FOL.  You might
also look into Hilbert and Bernays; like E, F, and T, they also have
separate syntactic categories "free variable" and "bound variable" and
may well have needed to define the fixed variable concept that you are
after.

> 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 :-).

I can ask some experts: I'm currently in Cambridge and some of the
Bonn naproche guys are around.  One can also consult the entry on DRT
in the Stanford Encyclopedia of Philosophy:

  http://plato.stanford.edu/entries/discourse-representation-theory/

Jesse

-- 
Jesse Alama
http://centria.di.fct.unl.pt/~alama/