Abstract

This paper provides a consistent first-order theory solving the knower paradoxes of Kaplan and Montague, with the following main features: 1. It solves the knower paradoxes by providing a faithful formalization of the principle of veracity (that knowledge requires truth), using both a knowledge and a truth predicate. 2. It is genuinely untyped i.e., it is untyped not only in the sense that it uses a single knowledge predicate applying to all sentences in the language (including sentences in which this predicate occurs), but in the sense that its axioms quantify over all sentences in the language, thus supporting comprehensive reasoning with untyped knowledge ascriptions. 3. Common knowledge predicates can be defined in the system using self-reference. These facts, together with a technique based on Löb’s theorem, enables it to support comprehensive reasoning with untyped common knowledge ascriptions (without having any axiom directly addressing common knowledge).