next up previous
Next: Functions from Things to Up: FIRST ORDER THEORIES OF Previous: Introduction

Knowing What and Knowing That

To assert that Pat knows Mike's telephone number we write

  equation39

with the following conventions:

  1. Parentheses are often omitted for one argument functions and predicates. This purely syntactic convention is not important. Another convention is to capitalize the first letter of a constant, variable or function name when its value is a concept. (We considered also capitalizing the last letter when the arguments are concepts, but it made the formulas ugly).
  2. Mike is the concept of Mike; i.e. it is the sense of the expression ``Mike''. mike is Mike himself.
  3. Telephone is a function that takes a concept of a person into a concept of his telephone number. We will also use telephone which takes the person himself into the telephone number itself. We do not propose to identify the function Telephone with the general concept of a person's telephone number.
  4. If P is a person concept and X is another concept, then Know(P,X) is an assertion concept or proposition meaning that P knows the value of X. Thus in (1) Know(Pat,Telephone Mike) is a proposition and not a truth value. Note that we are formalizing knowing what rather than knowing that or knowing how. For AI and for other practical purposes, knowing what seems to be the most useful notion of the three. In English, knowing what is written knowing whether when the ``knowand'' is a proposition.
  5. It is often convenient to write tex2html_wrap_inline1023 instead of

    displaymath1025

    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

      equation53

  6. We expect that the proposition tex2html_wrap_inline1029 will be useful accompanied by axioms that allow inferring that Pat will use this knowledge under appropriate circumstances, i.e. he will dial it or retell it when appropriate. There will also be axioms asserting that he will know it after being told it or looking it up in the telephone book.
  7. While the sentence ``Pat knows Mike'' is in common use, it is harder to see how Know(Pat, Mike) is to be used and axiomatized. I suspect that new methods will be required to treat knowing a person.
  8. true Q is the truth value, t or f, of the proposition Q, and we must write tex2html_wrap_inline1039 in order to assert Q. Later we will consider formalisms in which true has a another argument--a situation, a story, a possible world, or even a partial possible world (a notion we suspect will eventually be found necessary).
  9. The formulas are in a sorted first order logic with functions and equality. Knowledge, necessity, etc. will be discussed without extending the logic in any way--solely by the introduction of predicate and function symbols subject to suitable axioms. In the present informal treatment, we will not be explicit about sorts, but we will use different letters for variables of different sorts.

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

  equation64

and asserting it requires writing

  equation67

while the proposition that Joe knows that Pat knows Mike's telephone number is written

  equation71

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

  equation74

Functions like Telephone are then related to denot by equations like

  equation77

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

  equation85

Know is extensional with respect to denot in its first argument, and this is expressed by

  equation88

but it is Not extensional in its second argument. We can therefore define a predicate know(p,X) satisfying

  equation91

(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

  equation94

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

  eqnarray98

We now introduce the function Exists satisfying

  equation101

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

  equation104

which is related to the predicate ishorse by

  equation107

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 tex2html_wrap_inline1123 , etc. which we will write And, etc., write as infixes, and axiomatize by

  equation110

etc. The corresponding formulas for Or, Not, Implies, and Equiv are

  equation113

  equation116

  equation119

and

  equation122

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 gif

  equation126

  equation129

and

  equation132

making tex2html_wrap_inline1151 an equivalence relation, and

  equation135

which relates it to equality in the logic.

We can make the concept of equality essentially symmetric by replacing (22) by

  equation139

i.e. making the two expressions denote the same concept.

The statement that Mary has the same telephone as Mike is asserted by

  equation143

and it obviously doesn't follow from this and (1) that

  equation147

To draw this conclusion we need something like

  equation150

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.


next up previous
Next: Functions from Things to Up: FIRST ORDER THEORIES OF Previous: Introduction

John McCarthy
Tue May 14 16:07:43 PDT 1996