 The epistemic paradoxes constitute a threat to the construction of formal theories of knowledge, as the paradoxes become formalisable in many such theories. Suppose we wish to construct a formal theory of knowability within an extension of first-order arithmetic. The reason for choosing to formalise knowability rather than knowledge is that knowledge is always relative to a certain agent at a certain point in time, whereas knowability is a universal concept like truth. We could have chosen to work directly with knowledge instead, but it would require more work and make the presentation unnecessarily complicated. To formalise knowability we introduce a special predicate \(K\), and use sentences of the form \(K\langle \phi \rangle\) to express that \(\phi\) is knowable. Analogous to the cases of truth and set membership, there must be certain logical principles that \(K\) needs to satisfy in order for our formal theory to qualify as an adequate theory of knowability. First of all, all knowable sentences must be true. This property can be formalised by the following logical principle: