Unary Modal Logic

@[match_pattern]

def Cslib.Logic.Modal.Proposition.Context.dynDiamond {τ : PFunctor.{u_1, u_2}} [τ.Unary] {Atom : Type u_3} (c : Context τ Atom) (a : τ.A) : Context τ Atom

Context constructor for the dynamic diamond modality.

Equations

• c.dynDiamond a = Cslib.Logic.Modal.Proposition.Context.triangle a default c fun (x : { j : τ.B a // j ≠ default }) => match x with | ⟨i, hi⟩ => ⋯.elim

theorem Cslib.Logic.Modal.Proposition.unary_triangle_eq_dynDiamond {τ : PFunctor.{u_2, u_3}} [τ.Unary] {Atom : Type u_1} {a : τ.A} (φs : PropositionMap τ a Atom) : HasTriangle.triangle a φs = HasDynamicDiamond.dynDiamond a (φs default)

theorem Cslib.Logic.Modal.Satisfies.dynDiamond_iff_exists {τ : PFunctor.{u_3, u_4}} [τ.Unary] {World : Type u_1} {Atom : Type u_2} {w : World} {a : τ.A} {m : Model World τ Atom} {φ : Proposition τ Atom} : ⇓{ m := m, w := w, φ := HasDynamicDiamond.dynDiamond a φ } ↔ ∃ (w' : World), m.diagonal a w w' ∧ ⇓{ m := m, w := w', φ := φ }

theorem Cslib.Logic.Modal.Satisfies.dynBox_iff_forall {τ : PFunctor.{u_3, u_4}} [τ.Unary] {World : Type u_1} {Atom : Type u_2} {w : World} {a : τ.A} {m : Model World τ Atom} {φ : Proposition τ Atom} : ⇓{ m := m, w := w, φ := HasDynamicBox.dynBox a φ } ↔ ∀ (w' : World), m.diagonal a w w' → ⇓{ m := m, w := w', φ := φ }

theorem Cslib.Logic.Modal.Satisfies.dynBox_dynDiamond_diagonalInverse₁ {τ : PFunctor.{u_3, u_4}} [τ.Unary] {World : Type u_1} {Atom : Type u_2} {w : World} {m : Model World τ Atom} {op₁ op₂ : τ.A} [m.DiagonalInverse op₁ op₂] {φ : Proposition τ Atom} : ⇓{ m := m, w := w, φ := HasImp.imp φ (HasDynamicBox.dynBox op₁ (HasDynamicDiamond.dynDiamond op₂ φ)) }

If two operators op₁ and op₂ have inverse diagonal relations, then φ → d[op₁](d⟨op₂⟩φ).

theorem Cslib.Logic.Modal.Satisfies.dynBox_dynDiamond_diagonalInverse₂ {τ : PFunctor.{u_3, u_4}} [τ.Unary] {World : Type u_1} {Atom : Type u_2} {w : World} {m : Model World τ Atom} {op₁ op₂ : τ.A} [m.DiagonalInverse op₁ op₂] {φ : Proposition τ Atom} : ⇓{ m := m, w := w, φ := HasImp.imp φ (HasDynamicBox.dynBox op₂ (HasDynamicDiamond.dynDiamond op₁ φ)) }

If two operators op₁ and op₂ have inverse diagonal relations, then φ → d[op₂](d⟨op₁⟩φ).

theorem Cslib.Logic.Modal.Satisfies.unary_dual {τ : PFunctor.{u_3, u_4}} {World : Type u_1} {Atom : Type u_2} (f : Frame World τ) {a : τ.A} {φ : Proposition τ Atom} : InferenceSystem.derivation (Axiom f) (HasIff.iff (HasDynamicDiamond.dynDiamond a φ) (HasNot.not (HasDynamicBox.dynBox a (HasNot.not φ))))

The dual axiom (reformulated for unary modal logic).