Metalanguage and Higher-order language

• Mail folder: Interlingua Mail
• Next message: Tom Gruber: "what is the "all" in KIF's forall ?"
• Previous message: phayes@cs.uiuc.edu: "Re: A proposal of "sorts""

Date: Mon, 6 Dec 93 19:11:13 EST
From: sowa <sowa@turing.pacss.binghamton.edu>
Message-id: <9312070011.AA07636@turing.pacss.binghamton.edu>
To: cg@cs.umn.edu, interlingua@ISI.EDU
Subject: Metalanguage and Higher-order language
Cc: sowa@turing.pacss.binghamton.edu

Fritz,
When Tom Gruber, Mike Genesereth, and I have been advocating a first-order
approach, we have always insisted on FOL plus arbitrarily many metalevels.
That point is that the metalanguage gives you the ability to define
axiom schemata, lambda conversion, and all such things within a logic
that still has first-order style models.
 
That logic also gives you the ability to define all of Peano's axioms,
including the axiom of induction, which is the only one that goes beyond
a purely first-order framework.
 
In a higher-order logic, you can state the axiom of induction in
the following way:
 
    For all predicates P, if P(0) is true and if P(n) implies P(n+1),
    then for all n, P(n) is true.
 
This is a second-order statement because the first quantifier in it
ranges over all predicates P.
 
But we can state the axiom of induction in a metalanguage in the
following way:
 
    For all predicate definitions D, let P be the predicate defined by P;
    Then if P(0) is true and if P(n) implies P(n+1), then for all n, P(n).
 
Notice that the only difference between these two statements of the
axiom of induction is the domain of quantification.  The first one
ranges over all predicates, and the second ranges only over all definitions
of predicates.  Since the number of possible statements is countable,
the number of possible definitions is at most countable.  Therefore,
the metalevel statement ranges only over a countable number of
definable predicates whereas the higher-order statement allows the
variable P to range over undefinable predicates.
 
That same restriction applies to all of your examples about
virtues of philosophers, etc.  A higher-order language could range
over undefinable virtues, but a first-order language with metalevels
would only range over definable virtues.
 
As far as I can see from that HOL book that I suggested, they are not
using "true" higher-order logic, but rather a first-order logic plus
metalevels -- very much the same kind of thing that we are recommending
for KIF and CGs.  So their HOL is the same as what we were calling
FOL.
 
As far as I know, I can't think of any possible application of
KIF or CGs to computer science or linguistics that would require anything
beyond FOL plus metalevels.  We might not be able to quantify over
undefinable predicates, but I can't see why one would need to.
Perhaps someday someone might find some need for such quantifiers.
But then, nothing we are doing now will prevent future ANSI and ISO
committees from extending KIF and/or CGs to allow such quantification.
But until then, I don't see why we should put it in.
 
I also object to a statement you made that I have "now departed from FOL
by including numbers as primitives along with a cardinality function
>From a set to a number."  That example I gave was purely first order.
I can have a pure first-order statement in which one of my sorts or
types happens to be the integers.
 
The definition of infinity (which was first suggested by C. S. Peirce
by the way) uses higher order logic INSTEAD of assuming the integers.
It says that a set S is infinite if there exists a one-to-one
mapping from S to one of its proper subsets.  This statement is higher
order because it quantifies over mappings (i.e. functions), but it
does not require any reference to numbers or counting.
 
If you allow numbers and counting, then the definition of finiteness
is trivial:  A set S is finite if there exists a number n where
count(S)=n.  And the count function is a very simple function that
can be defined in the metalanguage:  
 
    if S is the empty set, then count(S)=0;
    else delete one element from S to form S' and define
    count(S) to be count(S')+1.
 
The point about this is that when you have metalanguage, you have
the ability to define functions, state the rules of lambda conversion
for evaluating functions, define axiom schemata as a replacement for
quantifying over predicates -- all within a framework of first-order
logic plus metalanguage.
 
And I also claim that the HOL system I suggested that you look at
is not doing any kind of quantification over undefinable predicates.
I believe (although I must say that I have not studied HOL in full
detail) that HOL is doing just the same kind of thing that we have
been advocating for KIF and CGs.  
 
That is a clear-cut claim that could be verified or falsified by
someone who truly knows HOL.  I would be happy to have someone
do that -- tell me that I'm right or wrong and cite the passage
in the HOL book that supports or refutes my claim. 
 
John