[CL] Why Don't We Need Free Variables?

[Christopher Welty]

Randy,

These threads tend to get very intense - I wanted to be sure a few things 
were clear:

You wrote on 08/02/2005 11:37:12 AM:
> >   1 Adopt a notation in which variables can be distinguished from
> >   constants orthographically, say, with preposed question marks:
> >
> >       (if (loves John ?x) (species ?x feline))
> 
> For the record, I very much like having a lexical convention that 
> distinguishes variables from other names. This is common practice in 
> technical publications involving mathematical, logical and physical 
> formulas, and to me it's just confusing to obliterate the lexical 
> distinction between variables and other linguistic entities that have 
> names.

Then CL is for you.  Remember that CL is not a language itself.  It is 
easy to define a language using CL that has a special notation for 
variables.

> > What else do you need?  If you want a standard _semantics_ for such
> > formulas, you could adopt the convention that free variables are
> > implicitly universally quantified, but in my experience this
> > convention is often violated.  Anyone can extend CL to include this
> > convention (I assume; who would prevent them?).  But there doesn't
> > seem to be any particular reason for CL to adopt it.  I'd be much
> > more interested in seeing 'lambda' added to the language.
> 
> Is it so outlandish to want to convey FOL-like formulas that have no 
> fixed semantics established by the standard? If CL is so constrained 
> that only facts can be conveyed, it seems to have excluded practical 
> uses.

I suspect there is confusion here that has to do with what a "variable" 
is.  I really think that, according to several common notions of what a 
variable is in logic, CL does have variables, and you are tilting at 
windmills (ie there is nothing here to disagree with).

If your intention is to define a SYNTAX that allows for: visually 
identifiable variables names (eg ?x) and formulae with such names that do 
not appear in a quantifier, then you can do that.  You can define in CL a 
language in which the interpretation of such formulae is defined to have a 
quantifier (ie the convention is formally defined).  You can define 
different languages with different conventions, and through CL they will 
be interchangeable (although what appears in one language to be a sentence 
w/ free variables will not be in the other language, since the meaning of 
free variables is different).

If your intention is to allow such a syntax to have no "convention", so 
that variables in a sentence w/o quantifiers can mean anything, or more 
importantly, that a sentence w/ free variables would look the same in any 
language that allows it, even though they mean something different, then i 
don't think you can do that in CL.  If that is what you wanted, you don't 
need an interchange language at all, you just want a string copy.  I 
strongly suspect you do not, it sounded like you simply wanted a syntax 
that allowed for free variables. 

-ChrisW