 Proof. Assume the existence of a consistent formal theory \(S\) extending first-order arithmetic and containing axiom schemas A1–A4. We need to show that this assumption leads to a contradiction. The proof mimics the paradox of the knower. Apply the diagonal lemma to obtain a sentence \(\lambda\) satisfying \(\lambda \leftrightarrow \neg K \langle \lambda \rangle\) in \(S\). The sentence \(\lambda\) expresses of itself that it is not knowable, so \(\lambda\) roughly corresponds to the knower sentence, \(KS\). The first piece of argumentation used in the paradox of the knower led to the conclusion that \(KS\) is indeed true. This piece of argumentation is mimicked by the following piece of formal reasoning within \(S\):