Re: Types vs. monadic relations
YOUR NAME HERE <hayes@sumex-aim.stanford.edu>
Reply-To: cg@cs.umn.edu
Date: Mon, 3 Feb 1992 22:58:24 PST
From: YOUR NAME HERE <hayes@sumex-aim.stanford.edu>
Subject: Re: Types vs. monadic relations
To: sowa@watson.ibm.com
Cc: macgregor@ISI.EDU, interlingua@ISI.EDU, srkb@ISI.EDU, cg@cs.umn.edu,
hayes@cs.stanford.edu
In-reply-to: Your message of Mon, 3 Feb 92 18:43:28 EST
Message-id: <MacMS.31120.17515.hayes@sumex-aim.stanford.edu>
John, greetings.
The difference between a sorted logic and an unsorted one is essentially a
computational difference, not an assertional one. While I agree that sorted
langauges are an excellent idea, essentially for computational reasons, I
think we need to not get too involved with philosophical intuitions that have
no semantic basis. And not all the reasons you give are very convincing.
>1. ... In a sorted logic, there are four ways to
express that information, ...:
But this is hardly an advantage. The language is highly redundant, it seems:
one can say the same thing in four different ways. Why do you consider this a
good thing? It is a problem both computationally and for human use. If these
differences have consequence, then four users can say what they thought was
the same thing but the system understands them differently, and presumably
will fail to make some inferences that it should make. If the differences
have no consequence, this is just like offering the user a variety of fonts.
> Therefore, they are truth-functionally
equivalent. But ontologically, they make different assumptions
about the nature of reality.
But then it must be that the way in which they differ in meaning is not
accessible to the inference system. So it is merely philosphical decoration.
Actually, I disagree, in any case: I think they say exactly the same thing
about reality, but the ontological difference is something you have
hallucinated onto this functionally irrelevant syntactic distinction.
>I would say that formula (b) comes
closest to the implicit ontology in ordinary language, since most
languages express balls as nouns and colors as words that modify
nouns.
I think this illustrates your error here: a representation language is not a
natural language. But we should argue about this offline...
> But I would also
argue that the system should accommodate any ontology that anyone
might find useful for any purpose.
I agree, and that is why I suggested allowing people to assert arbitrary
properties of predicates. Why do you suppose that being a type is going to be
the only property that someone might wish to assert of a predicate? At the
very least one should allow the user to assert the kind of types they require:
as I am sure you know, languages can be typed in all sorts of ways.
>2. A second reason for a sorted or typed logic is that it makes the
formulas much shorter, more readable, and less error-prone for
humans.
>...note that both the English sentences and the sorted logic formulas
have the same syntactic form for the...
I think this is largely irrelevant. As I understand it, the point of the
representatinal standard is not to be especially perspicuous to human readers;
but in any case a tiny bit of syntactic icing will make an untyped language
with type information in it look just like a typed language ( in fact, BE such
a language). Again, I think you are confusing the language of human interface
with the language of representation.
>As someone who has taught many iterations of logic courses...
Yes, I have taught logic to undergraduates too. In my experience the best way
to get their minds clear is to teach them simple model theory and have them
learn to interpret what the axioms mean, rather than try to intuitively map
>From English sentences as most of the textbooks do. But in any case, the
kinds of errors that philosophy undergraduates make is hardly relevant to the
use of a system by educated professionals.
>3....Philosophically, when you use an unrestricted
quantifier...you allow that quantifier to range over
everything in the universe...but when you restrict it... you have reduced
its range of applicability by many orders of magnitude...
This seems confused. Typically the domains might well be infinite anyway, so
talk of 'orders of magnitude' seems wrong: but in any case, surely you arent
proposing that we handle quantifiers by somehow running through their domains?
If so, how would you suggest handling an assertion like 'The native tribes of
Africa have always respected their elders" ?
>4. Finally, there are very strong computational reasons for using
sorted logic in theorem proving....
Right, I agree.
> Pat Hayes's suggestion of using a second-order
assertion such as relation(red) or type(ball) is not sufficient. It
might allow you to preserve the distinction in mapping CGs to and
>From KIF, but it would do nothing to make KIF more efficient in
theorem proving or less error-prone for humans.
But thats not what the KIF is supposed to be. The KIF is for communication
between systems, a reference language for knowledge. Human perspicuity has
different requirements, and theorem-proving efficiency is very much a local
matter in each system. While it makes sense that one system might be able to
tell another that it treats some predicates in a certain way - so this
information should be expressible - there is no reason why the KIF reference
languauge itself must be optimised for either of these properties.
Pat Hayes
-------