Higher-order logicsowa <firstname.lastname@example.org>
Date: Thu, 11 Nov 93 19:46:17 EST
From: sowa <email@example.com>
To: firstname.lastname@example.org, email@example.com
Subject: Higher-order logic
There are a number of issues that have been getting mixed up in
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
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.