Axioms

As an example, describe about axiom . Other axioms such as and follow the same manner.

-- Axiom schema
abbrev System.Axioms.K (p q : F) := □(p ⟶ q) ⟶ □p ⟶ □q

abbrev Modal.Standard.AxiomSet (α : Type*) := Set (Modal.Standard.Formula α)

abbrev Modal.Standard.AxiomSet.K : AxiomSet α := { System.Axioms.K p q | (p) (q) }

notation "𝗞" => Modal.Standard.AxiomSet.K

Well-Known Axioms

NotationNameSchemaGeach
𝗞K□(p ⟶ q) ⟶ □p ⟶ □q
𝗧T□p ⟶ p✅
𝗕Bp ⟶ □◇p✅
𝗗D□p ⟶ ◇p✅
𝟰Four□p ⟶ □□p✅
𝟱Five◇p ⟶ □◇p✅
.𝟮Dot2◇□p ⟶ □◇p✅
.𝟯Dot3□(□p ⟶ □q) ⋎ □(□q ⟶ □p)
𝗟L□(□p ⟶ p) ⟶ □p
𝗚𝗿𝘇Grz□(□(p ⟶ □p) ⟶ p) ⟶ p
𝗧𝗰Tcp ⟶ □p✅
𝗩𝗲𝗿Ver□p
𝗖𝟰C4□□p ⟶ □p✅
𝗖𝗗CD◇p ⟶ □p✅
𝗠M□◇p ⟶ ◇□p

Geach Axioms

Geach Axiom is defined as .

structure Geach.Taple where
  i : ℕ
  j : ℕ
  m : ℕ
  n : ℕ

abbrev Geach (l : Geach.Taple) (p : F) := ◇^[l.i](□^[l.m]p) ⟶ □^[l.j](◇^[l.n]p)
notation "𝗴𝗲(" t ")" => AxiomSet.Geach t

Some axioms is generalized as Geach axioms (Above table, Geach: ✅). For example and .