**Mail folder:**Interlingua Mail**Next message:**Fritz Lehmann: "Higher-Order KIF and Conceptual Graphs"**Previous message:**Dan Schwartz: "Examples- Higher-Order KIF and Conceptual graphs"**In-reply-to:**sowa: "Higher-Order Logic"

Reply-To: cg@cs.umn.edu Date: Thu, 11 Nov 93 19:46:17 EST From: sowa <sowa@turing.pacss.binghamton.edu> Message-id: <9311120046.AA00805@turing.pacss.binghamton.edu> To: cg@cs.umn.edu, interlingua@cs.umn.edu Subject: Higher-order logic Cc: sowa@turing.pacss.binghamton.edu

There are a number of issues that have been getting mixed up in these discussions: 1. The ability to have unrestricted quantification over functions, predicates, propositions, and other "higher-order" objects. 2. The use of metalanguage capabilities for quantifying over the expressions that define various functions, predicates, and propositions. This capability seems to be sufficient to handle all of Fritz's examples. I translated one of Fritz's expressions into my version of CGs using metalanguage, and a similar mechanism could be used to represent the others. 3. Since the number of possible functions and predicates may be uncountable, but the number of possible expressions is at most countable, option 2 doesn't let the quantifiers range over as many "things" as option 1. But since all of Fritz's examples were stated in informal English, it is very far from clear whether option 1 or option 2 comes closer to capturing the intutive "meaning" that Leibniz et al. were trying to grope towards. 4. Another way of quantifying over higher-order objects is by means of a typed or sorted version of logic. Since this approach restricts the quantifiers to range only over a predefined sort, it may give you a logic which seems to express "the same thing", but which really has a much more restricted domain of discourse. However, if you stuff the whole uncountable mess of possible functions into your function sort, then you get the same collection of models. 5. The mechanisms currently defined for CGs allow you to take the metalanguage option of quantifying over expressions. They also allow you to take the typed-logic option of stuffing whatever you want into a type. You can, if you like, stuff an uncountable set of functions into a type. That is not something that I would do, but I am not going to stop anyone else from playing such games. 6. The question of which kind of syntactic sugar you spray over any of these constructions depends on your taste, and you can make any of these options look as pretty or as ugly as you like by defining appropriate symbols, macros, abbreviations, etc. Since Fritz mentioned Peirce, I'd like to quote a discussion by Peirce in a letter to Victoria, Lady Welby: When we have analyzed a proposition so as to throw into the subject everything that can be removed from the predicate, all that it remains for the predicate to represent is the form of connection between the different subjects as expressed in the propositional form. What I mean by "everything that can be removed from the predicate" is best explained by giving an example of something not so removable. But first take something removable. "Cain kills Abel." Here the predicate appears as "--kills--." But we can remove killing from the predicate and make the latter "--stands in the relation--to--." This quote is from p. 396 of _Charles S. Peirce: Selected Writings_, edited by P. P. Wiener, Dover Publications, NY, 1958. I would interpret that passage as implying that Peirce would sanction the option of reifying relations by "taking them out of the predicate" and making them objects subject to quantification in a first-order language. Therefore, that would put Fritz's examples taken from Peirce into the category of things that can be expressed adequately with a typed first-order logic, as we have in CGs. John Sowa