Higher-order logic

• 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