John McCarthy
Computer Science Department
1978-1981
Stanford University
This paper describes a formal system and uses it to express the puzzle of the three wise men and the puzzle of Mr. S and Mr. P. Four innovations in the axiomatization of knowledge were required: the ability to express joint knowledge of several people, the ability to express the initial non-knowledge, the ability to describe knowing what rather than merely knowing that, and the ability to express the change which occurs when someone learns something. Our axioms are written in first order logic and use Kripke-style possible worlds directly rather than modal operators or imitations thereof. We intend to use functions imitating modal operators and taking ``propositions'' and ``individual concepts'' as operands, but we haven't yet solved the problem of how to treat learning in such a formalism.1