**Mail folder:**Interlingua Mail**Next message:**Matthew L. Ginsberg: "Re: FOL vs HOL vs MML"**Previous message:**Robert Neches: "Re: info "**Reply:**Matthew L. Ginsberg: "Re: FOL vs HOL vs MML"**Reply:**Giuseppe Attardi: "Re: FOL vs HOL vs MML"

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