**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