Suppose T is a formal AI theory for Knowledge Representation. T contains a distinguished 1-place predicate symbol K (included in the Gödel numbering scheme), where K(┌Ф┐) is intended to formalize the idea that sentence Ф is known. Suppose further that the diagonal function is representable in the system, and that the logic of the knowledge predicate includes the general principles:
(*) ⊢T K(┌Ф┐) → Ф , since knowledge is considered to be factive, and
(**) if ⊢T Ф, then ⊢T K(┌Ф┐) , which is intended to capture the idea that if a statement is proven then it is known.
How do we show that the resulting formal theory of Knowledge Representation is inconsistent.