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

[John F. Sowa]

Randy,

What you seem to be saying is that there are different
interpretations of formulas with free variables.

RS> Because a formula with a free variable is never
 > interchangeable with one with that variable bound.

I agree.  But that is because the formula with variables
bound has a specific interpretation, and the one with
free variables is ambiguous.  When and why could that
be desirable?

RS> Many systems supply some sort of default quantification
 > in the presence of free variables, and sometimes that's
 > a suitable convention. For example, in Cyc asserting a formula
 > as a rule or fact that bears free variables is not deemed an
 > error and a universal quantifier is supplied gratis. Some might
 > call it gratuitous... In systems that implement deductive
 > question-answering, a complementary operation supplies existential
 > quantifiers are often supplied for free variables in submitted
 > queries. In the latter case, it is also typical only to display
 > bindings for those free variables when printing the query's results.

Each of these examples is a case where one default convention or
another determines which quantifier is implied.  You could add
KIF, for which the manual explicitly states that any variable not
bound by a quantifier has a universal quantifier by default.
That is also the Prolog convention.

RS> None of this has anything to do with any particular inference
 > rules or proof procedures. It's just a kind of logical content
 > that may have utility in certain contexts.

What utility?  In each of the above examples, there was a default
convention that determined what implicit quantifier was intended,
but different conventions lead to different choices.  None of them
expressed anything different from what could have been stated
explicitly by specifying the quantifier.

As I said, there are intermediate steps in some proof procedures
where the quantifiers are temporarily removed.  But what advantage
could there be in transmitting an ambiguous statement in a message
between two different systems?  What's the point?

John