FOL vs HOL vs MML

sowa <sowa@turing.pacss.binghamton.edu>
Date: Sat, 11 Dec 93 14:05:39 EST
From: sowa <sowa@turing.pacss.binghamton.edu>
Message-id: <9312111905.AA13466@turing.pacss.binghamton.edu>
To: cg@cs.umn.edu, interlingua@ISI.EDU
Subject: FOL vs HOL vs MML

Fritz and Norman,
 
Re MML:  I believe that the misunderstanding concerning the KIF/CG
semantics has resulted from calling it a version of first-order logic.
Perhaps a better term is Multi-Metalevel Logic or MML.  This gives us
all the "virtues" of HOL, but without some of the vices.  I believe
that the HOL system I cited before is also using what I am calling
MML rather than the unrestricted quantification over predicates that
characterizes HOL. 

Although I gave a rather complete description of MML in earlier notes,
I'll summarize it here:

 1. As a base language L0, assume a conventional FOL with a domain of
    discourse D0 and a conventional FOL-style of model theory.

 2. The let the first metalanguage L1 have the same syntax as L0
    (eg, KIF, CG, conventional predicate calculus, or whatever)
    but with a domain of discourse D1 which is the union of D0
    plus all syntactically correct expressions of L0.  L1 is also
    first-order, but it can be used to talk about L0, define new
    predicates and axioms for L0, define rules of lambda conversion
    for L0, and even define a model theory for L0.

 3. Then let L2 have the same syntax as L0 and L1, but with a domain
    D2, which is the union of D0, D1, and all the syntactically correct
    expressions of L1.  This gives us a metalanguage for L1 and a
    metametalanguage for L0.
 
 4. Continue in this way to define L3, L4, ....  Then take the union
    of all these languages and their domains of discourse and call the
    resulting language L* with domain D*.

The language L* and its semantics is what we have been assuming for
KIF and CGs.  It gives you an immense amount of power, but with a
model theory at each level that is purely first-order in style.
Furthermore, if the original domain D0 is countable, all the otehr
domains up to D* are also countable.  But if you wish, you can start
with uncountable sets in D0 and do all the kinds of things you might
want to do with uncountable infinities, still within a first-order
framework.

If you don't want to take my word for it, I suggest that you read
Quine's stuff.  Q. also advocates a first-order style of reasoning,
but instead of a metalevel, he uses "axiom schemata".  As a reference,
see Quine's _Set Theory and its Logic_, Harvard University Press, 1963.
Quine develops natural numbers, transfinite ordinals and cardinals,
and five different axiomatizations for set theory -- all within a
first-order style with axiom schemata.

Following is Quine's explanation for how he gets away without using
HOL:
   
   The schematic predicate letters 'F', 'G', ... attach to variables
to make dummy clauses 'Fxy','Gx', etc., as expository aids when we
want to talk about the outward form of a complex sentence without
specifying the component clauses....  So the letters 'F', 'G', ... are
never to be thought of as variables....  But the letters 'F', 'G',...
are withheld from quantifiers, indeed withheld from sentences
altogether and used only as dummies depicting the form of unspecified
sentences.

Some brief responses to the points raised by Fritz and Norman:

Re ontology revision:  Yes, this is a very important topic to pursue,
but it doesn't require quantification over unrestricted predicates.
It can be done at the metalevel in MML.

Re semantics for natural numbers:  Yes, I am assuming Peano's axioms.
As I said before, all of them are purely first-order, except for the
axiom of induction.  There are three ways of stating induction:

 1. In HOL, you quantify over predicates:

    For all predicates P, if P(0) and for all n, if P(n) implies P(n+1),
    then for all n, P(n).

 2. Using axiom schemata, as in Quine's approach, you do not quantify
    over P.  Instead, you treat P as a "dummy", which is to be replaced
    by an actual name for whatever predicate you want to talk about:

    If P(0) and for all n, if P(n) implies P(n+1), then for all n, P(n).

    With this approach, if you have 50 predicate names in your language,
    then this single axiom schema corresponds to 50 different axioms
    each one with a different substitution for the dummy P.

 3. In the metalanguage approach, you quantify over P at the metalevel
    and create a new axiom whenever you need one.  It is identical in
    practice to using axiom schemata, since the quantification is done
    only at the metalevel, not at the object level.

Re defining finite:  Defining "finite" is very simple if you assume
the ability to count:  A set S is finite iff when you count the elements
in S you eventually stop at some number N.  You can say this in FOL
very nicely:

    S is finite iff (En)(integer(n) & n>0 & count(S)=n).

Defining finite only becomes a problem if you want to avoid assuming
the integers as given.  Frege and Russell believed that set theory was
a part of logic and that it was somehow more primitive than the integers.
Other people, me included, believe that set theory is NOT a part of
logic, but a separate subject that is at least as much in need of
a foundation as the integers.  In fact, I have more faith in the
integers than I do in set theory.
 
Re opaqueness:  The metalevel treatment we have been assuming for MML
gives you all the transparency that you might want.  At each level,
the language Ln can talk about Ln-1, Ln-2, Ln-3,... plus all their
domains of discourse Dn-1, Dn-2,....  So you can use it both to define
new kinds of expressions in any of the lower levels and to define how
those expressions are related to one another.

Re mermaid:  Yes, if you restrict the domains over which you quantify,
you restrict expressive power.  But if you really want that power, you
can assume domains that are uncountable -- that gives you exactly the
same expressive power and equivalent denotations in your semantics.

Bottom line:  MML gives you a way of doing higher-order things, but in
a form that allows you to retain a first-order style of model theory
with the nice properties, such as compactness.  If you really believe
that you must quantify over all those uncountable infinities of possible
functions and predicates, you can do so by putting them into your
ground domain D0.  That is essentially what Quine does with his
approach of using axiom schemata, and we can do exactly the same thing
with MML.

John