 In words, K1 says that if \(i\) knows \(A\), then \(A\) must be the case. K2 says that \(i\) knows that some possible world in \(\Omega\) occurs no matter which possible world \(\omega\) occurs.  K3[10]  says that \(i\) knows a conjunction if, and only if, \(i\) knows each conjunct. K4 is a reflection axiom, sometimes also presented as the axiom of transparency (or of positive introspection), which says that if \(i\) knows \(A\), then \(i\) knows that she knows \(A\). Finally, K5 says that if the agent does not know an event, then she knows that she does not know. This axiom is presented as the axiom of negative introspection, or as the axiom of wisdom (since the agents possess Socratic wisdom, knowing that they do not know.) Note that by K3, if \(A \subseteq B\) then \(\mathbf{K}_i (A) \subseteq \mathbf{K}_i (B)\), by K1 and K2, \(\mathbf{K}_i (\Omega) = \Omega\), and by K1 and K4, \(\mathbf{K}_i (A) = \mathbf{K}_i \mathbf{K}_i (A)\). Any system of knowledge satisfying K1–K5 corresponds to the modal system S5, while any system satisfying K1–K4 corresponds to S4 (Kripke 1963). If one drops the K1 axiom and retains the others, the resulting system would give a formal account of what an agent believes, but does not necessarily know.