Not to be confused with the Axiom K of Martin-Löf type theory.
The K axiom of modal logic (named after Saul Kripke) is
□(ϕ→ψ)→□ϕ→□ψ \Box (\phi \to \psi) \to \Box \phi \to \Box \psi □(ϕ→ψ)→□ϕ→□ψ
It is equivalent to any of the following statements.