 This proof shows that \(\lambda\), our formal version of \(KS\), is provable in \(S\). The proof corresponds to the informal argument that \(KS\) is true. As argued in the paradox of the knower, any agent with sufficient reasoning capabilities will be able to prove the truth of \(KS\), and thus come to know that \(KS\) holds. Thus \(KS\) must be knowable. What this means in the present formal framework is that we can also prove the knowability of \(\lambda\) in \(S\):