nLab axiom K (modal logic)

Contents

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

Contents

Idea

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

K:(pq)pq.K \colon \Box(p \to q) \to \Box p \to \Box q.

Developments

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

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

References

Axiom K is discussed in Example 6.1.7 of:

Last revised on December 11, 2023 at 02:31:34. See the history of this page for a list of all contributions to it.