axiom K (modal logic)

*Disambiguation: For axiom K as a principle of type theory, see axiom K (type theory)*

In modal logic, axiom K, named after Saul Kripke, is a basic principle which almost all versions of propositional modal logic satisfy

$K \colon \Box(p \to q) \to \Box p \to \Box q.$

It is possible to consider a variant in dependent type theory (Spitters)

$Dependent\; K \colon \Box \Pi_{y:A} B(y) \to \Pi_{x: \Box A} \Box B [open\; x/y].$

- Bas Spitters et al.,
*Modal Dependent Type Theory and Dependent Right Adjoints*, (slides)