[mizar] Re: still_not-bound_in p

[Andrzej Trybulec <trybulec@math.uwb.edu.pl>]

Hi Jesse:

Definitely the second. It is the set of "bound" variables that are 
syntactically free, as a rule in
a subformula. In a well formed sentence all "bound" variables must be 
bound. We have introduced
2 kinds of variables because in the Jaskowski system (and the ultimate 
goal was to describe this system,
as it is used in Mizar) there are two kinda of variables: regular 
variables and local constants (local in
a proof). We call them "fixed variables". It seems that formalizing the 
system in this way (using two kinds
of variables) is more clear.

The third kind of variables was introduced "just in the case". We 
thought about at least two application:
- formalizing systems of natural deduction in Gentzen style
- full formalization of (a part) of the Mizar language, in which 
syntactically free variables occur.

The "free" variables in Mizar are not "real" variables (in the Hilbert 
terminology). They are bound by default
on the beginning of the sentence (or maybe by the Fraenkel operator if 
they occur in a Fraenkel term).
If they are reserved for a type, if not an error is reported.

Czeslaw Bylinski used them as meta-variables. A predicate form is 
defined as a formula with free variables
and to get a formula one substitutes them by bound or fixed variables. 
In which way Patrick and Peter
are using these concepts, I do not know. I still hope to find time to 
read their articles.

All the best,
Andrzej


Jesse Alama wrote:

> Hi Piotr, Andrzej,
>
> I'm investigating the new proof of Gödel's completeness theorem that 
> was carried out in the Mizar system.  In particular, I'm investigating 
> the definition of the functor `still_not-bound_in p', where the 
> variable `p' has type `QC-formula'.  This definition is in QC_LANG1.  
> I'm puzzled by that definition, so I thought I'd ask about it.  Is 
> `still_not-bound_in p' supposed to represent the set of free variables 
> in the first-order formula p?  Or: is it supposed to represent the set 
> of bound variables that occur freely in p?
>
> Warm regards,
>
> Jesse