Professor John McCarthy
Father of AI

Articles

Formalization of Two Puzzles Involving Knowledge

Formalization of two Puzzles Involving Knowledge involves formalization of facts about knowledge including both knowing what and knowing that, how to assume and prove non-knowledge, joint knowledge and the effect of learning a fact on the set of facts then known. It uses the Kripke possible worlds formalism directly.

Formalization of two Puzzles Involving Knowledge was written between 1971 and 1987. It involves formalization of facts about knowledge including both knowing what and knowing that, how to assume and prove non-knowledge, joint knowledge and the effect of learning a fact on the set of facts then known.

A major proof was done by Xiwen Ma, then visiting Stanford from Peking 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.

Download the article in PDF.