To assert that Pat knows Mike's telephone number we write
with the following conventions:
when we don't intend to iterate knowledge further. know is a predicate in the logic, so we cannot apply any knowledge operators to it. We will have
The reader may be nervous about what is meant by concept. He will have to remain nervous; no final commitment will be made in this paper. The formalism is compatible with many possibilities, and these can be compared using the models of their first order theories. Actually, this paper isn't much motivated by the philosophical question of what concepts really are. The goal is more to make a formal structure that can be used to represent facts about knowledge and belief so that a computer program can reason about who has what knowledge in order to solve problems. From either the philosophical or the AI point of view, however, if (1) is to be reasonable, it must not follow from (1) and the fact that Mary's telephone number is the same as Mike's, that Pat knows Mary's telephone number.
The proposition that Joe knows whether Pat knows Mike's telephone number, is written
and asserting it requires writing
while the proposition that Joe knows that Pat knows Mike's telephone number is written
where K(P,Q) is the proposition that P knows that Q. English does not treat knowing a proposition and knowing an individual concept uniformly; knowing an individual concept means knowing its value while knowing a proposition means knowing that it has a particular value, namely t. There is no reason to impose this infirmity on robots.
We first consider systems in which corresponding to each concept X, there is a thing x of which X is a concept. Then there is a function denot such that
Functions like Telephone are then related to denot by equations like
We call denot X the denotation of the concept X, and (7) asserts that the denotation of the concept of P's telephone number depends only on the denotation of the concept P. The variables in (7) range over concepts of persons, and we regard (7) as asserting that Telephone is extensional with respect to denot. Note that our denot operates on concepts rather than on expressions; a theory of expressions will also need a denotation function. From (7) and suitable logical axioms follows the existence of a function telephone satisfying
Know is extensional with respect to denot in its first argument, and this is expressed by
but it is Not extensional in its second argument. We can therefore define a predicate know(p,X) satisfying
(Note that all these predicates and functions are entirely extensional in the underlying logic, and the notion of extensionality presented here is relative to denot.)
The predicate true and the function denot are related by
provided truth values are in the range of denot, and denot could also be provided with a (partial) possible world argument.
When we don't assume that all concepts have denotations, we use a predicate denotes(X,x) instead of a function. The extensionality of Telephone would then be written
We now introduce the function Exists satisfying
Suppose we want to assert that Pegasus is a horse without asserting that Pegasus exists. We can do this by introducing the predicate Ishorse and writing
which is related to the predicate ishorse by
In this way, we assert extensionality without assuming that all concepts have denotations. Exists is extensional in this sense, but the corresponding predicate exists is identically true and therefore dispensable.
In order to combine concepts propositionally, we need analogs of the propositional operators such as , etc. which we will write And, etc., write as infixes, and axiomatize by
etc. The corresponding formulas for Or, Not, Implies, and Equiv are
The equality symbol ``='' is part of the logic so that X = Y asserts that X and Y are the same concept. To write propositions expressing equality of the denotations of concepts, we introduce Equal(X,Y) which is the proposition that X and Y denote the same thing if anything. We shall want axioms
making an equivalence relation, and
which relates it to equality in the logic.
We can make the concept of equality essentially symmetric by replacing (22) by
i.e. making the two expressions denote the same concept.
The statement that Mary has the same telephone as Mike is asserted by
and it obviously doesn't follow from this and (1) that
To draw this conclusion we need something like
and suitable axioms about knowledge.
If we were to adopt the convention that a proposition appearing at the outer level of a sentence is asserted and were to regard the denotation-valued function as standing for the sense-valued function when it appears as the second argument of Know, we would have a notation that resembles ordinary language in handling obliquity entirely by context. There is no guarantee that general statements could be expressed unambiguously without circumlocution; the fact that the principles of intensional reasoning haven't yet been stated is evidence against the suitability of ordinary language for stating them.