Documentation

Foundation.Modal.Kripke.Semantics

Equations
theorem LO.Modal.Formula.Kripke.Satisfies.box_def {α : Type u_1} {M : LO.Kripke.Model α} {x : M.World} {p : LO.Modal.Formula α} :
x p ∀ (y : M.Frame.World), x yy p
theorem LO.Modal.Formula.Kripke.Satisfies.dia_def {α : Type u_1} {M : LO.Kripke.Model α} {x : M.World} {p : LO.Modal.Formula α} :
x p ∃ (y : M.Frame.World), x y y p
theorem LO.Modal.Formula.Kripke.Satisfies.not_def {α : Type u_1} {M : LO.Kripke.Model α} {x : M.World} {p : LO.Modal.Formula α} :
x p ¬x p
Equations
  • LO.Modal.Formula.Kripke.Satisfies.instNotWorld = { realize_not := }
theorem LO.Modal.Formula.Kripke.Satisfies.imp_def {α : Type u_1} {M : LO.Kripke.Model α} {x : M.World} {p : LO.Modal.Formula α} {q : LO.Modal.Formula α} :
x p q x px q
Equations
  • LO.Modal.Formula.Kripke.Satisfies.instImpWorld = { realize_imp := }
theorem LO.Modal.Formula.Kripke.Satisfies.or_def {α : Type u_1} {M : LO.Kripke.Model α} {x : M.World} {p : LO.Modal.Formula α} {q : LO.Modal.Formula α} :
x p q x p x q
Equations
  • LO.Modal.Formula.Kripke.Satisfies.instOrWorld = { realize_or := }
theorem LO.Modal.Formula.Kripke.Satisfies.and_def {α : Type u_1} {M : LO.Kripke.Model α} {x : M.World} {p : LO.Modal.Formula α} {q : LO.Modal.Formula α} :
x p q x p x q
Equations
  • LO.Modal.Formula.Kripke.Satisfies.instAndWorld = { realize_and := }
Equations
  • LO.Modal.Formula.Kripke.Satisfies.instTarskiWorld = LO.Semantics.Tarski.mk
theorem LO.Modal.Formula.Kripke.Satisfies.multibox_def {α : Type u_1} {M : LO.Kripke.Model α} {x : M.World} {p : LO.Modal.Formula α} {n : } :
x □^[n]p ∀ {y : M.Frame.World}, x ≺^[n] yy p
theorem LO.Modal.Formula.Kripke.Satisfies.multidia_def {α : Type u_1} {M : LO.Kripke.Model α} {x : M.World} {p : LO.Modal.Formula α} {n : } :
x ◇^[n]p ∃ (y : M.Frame.World), x ≺^[n] y y p
theorem LO.Modal.Formula.Kripke.Satisfies.trans {α : Type u_1} {M : LO.Kripke.Model α} {x : M.World} {p : LO.Modal.Formula α} {q : LO.Modal.Formula α} {r : LO.Modal.Formula α} (hpq : x p q) (hqr : x q r) :
x p r
theorem LO.Modal.Formula.Kripke.Satisfies.mdp {α : Type u_1} {M : LO.Kripke.Model α} {x : M.World} {p : LO.Modal.Formula α} {q : LO.Modal.Formula α} (hpq : x p q) (hp : x p) :
x q
theorem LO.Modal.Formula.Kripke.Satisfies.not_imp {α : Type u_1} {M : LO.Kripke.Model α} {x : M.World} {p : LO.Modal.Formula α} {q : LO.Modal.Formula α} :
¬x p q x p q
Equations
Instances For
    Equations
    Equations
    • LO.Modal.Formula.Kripke.ValidOnModel.instBotModel = { realize_bot := }
    theorem LO.Modal.Formula.Kripke.ValidOnModel.mdp {α : Type u_1} {M : LO.Kripke.Model α} {p : LO.Modal.Formula α} {q : LO.Modal.Formula α} (hpq : M p q) (hp : M p) :
    M q
    Equations
    Instances For
      Equations
      Equations
      • LO.Modal.Formula.Kripke.ValidOnFrame.instBotDep = { realize_bot := }
      theorem LO.Modal.Formula.Kripke.ValidOnFrame.mdp {α : Type u_1} {F : LO.Kripke.Frame.Dep α} {p : LO.Modal.Formula α} {q : LO.Modal.Formula α} (hpq : F p q) (hp : F p) :
      F q
      Equations
      theorem LO.Modal.Formula.Kripke.ValidOnFrameClass.mdp {α : Type u_1} {𝔽 : LO.Kripke.FrameClass.Dep α} {p : LO.Modal.Formula α} {q : LO.Modal.Formula α} (hpq : 𝔽 p q) (hp : 𝔽 p) :
      𝔽 q
      @[reducible, inline]
      Equations
      Instances For
        Equations
        theorem LO.Modal.Kripke.nec {α : Type u_1} {𝔽 : LO.Kripke.FrameClass} {p : LO.Modal.Formula α} (h : 𝔽#α p) :
        𝔽#α p
        theorem LO.Modal.Kripke.mdp {α : Type u_1} {𝔽 : LO.Kripke.FrameClass} {p : LO.Modal.Formula α} {q : LO.Modal.Formula α} (hpq : 𝔽#α p q) (hp : 𝔽#α p) :
        𝔽#α q
        theorem LO.Modal.Kripke.iff_not_validOnFrameClass {α : Type u_1} {𝔽 : LO.Kripke.FrameClass} {p : LO.Modal.Formula α} :
        ¬𝔽#α p F𝔽, ∃ (V : LO.Kripke.Valuation F α) (x : { Frame := F, Valuation := V }.World), ¬LO.Modal.Formula.Kripke.Satisfies { Frame := F, Valuation := V } x p
        theorem LO.Modal.Kripke.iff_not_set_validOnFrameClass {α : Type u_1} {𝔽 : LO.Kripke.FrameClass} {T : Set (LO.Modal.Formula α)} :
        ¬𝔽#α ⊧* T pT, F𝔽, ∃ (V : LO.Kripke.Valuation F α) (x : { Frame := F, Valuation := V }.World), ¬LO.Modal.Formula.Kripke.Satisfies { Frame := F, Valuation := V } x p
        theorem LO.Modal.Kripke.iff_not_validOnFrame {α : Type u_1} {F : LO.Kripke.Frame} {T : Set (LO.Modal.Formula α)} :
        ¬F#α ⊧* T pT, ∃ (V : LO.Kripke.Valuation F α) (x : { Frame := F, Valuation := V }.World), ¬LO.Modal.Formula.Kripke.Satisfies { Frame := F, Valuation := V } x p
        @[reducible, inline]
        Equations
        Instances For
          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            @[reducible, inline]
            Equations
            Instances For
              Equations
              • One or more equations did not get rendered due to their size.
              Instances For
                def LO.Modal.Kripke.definability_union_frameclass_of_theory {α : Type u_1} {𝔽₁ : LO.Kripke.FrameClass} {𝔽₂ : LO.Kripke.FrameClass} {T₁ : LO.Modal.Theory α} {T₂ : LO.Modal.Theory α} (defi₁ : 𝔽(T₁).DefinedBy 𝔽₁) (defi₂ : 𝔽(T₂).DefinedBy 𝔽₂) (nonempty : Set.Nonempty (𝔽₁ 𝔽₂)) :
                𝔽(T₁ T₂).DefinedBy (𝔽₁ 𝔽₂)
                Equations
                Instances For
                  def LO.Modal.Kripke.characterizability_union_frameclass_of_theory {α : Type u_1} {𝔽₁ : LO.Kripke.FrameClass} {𝔽₂ : LO.Kripke.FrameClass} {T₁ : LO.Modal.Theory α} {T₂ : LO.Modal.Theory α} (char₁ : 𝔽(T₁).Characteraizable 𝔽₁) (char₂ : 𝔽(T₂).Characteraizable 𝔽₂) (nonempty : Set.Nonempty (𝔽₁ 𝔽₂)) :
                  𝔽(T₁ T₂).Characteraizable (𝔽₁ 𝔽₂)
                  Equations
                  Instances For
                    @[reducible, inline]
                    Equations
                    Instances For
                      Equations
                      • One or more equations did not get rendered due to their size.
                      Instances For
                        Equations
                        • LO.Modal.Kripke.instDefinedByFrameClassOfHilbertExtKOfFrameClassOfTheory = { define := , nonempty := }
                        Equations
                        • LO.Modal.Kripke.instCharacteraizableFrameClassOfHilbertExtKOfFrameClassOfTheory = { characterize := , nonempty := }
                        @[reducible, inline]
                        Equations
                        Instances For
                          Equations
                          • One or more equations did not get rendered due to their size.
                          Instances For
                            Equations
                            • LO.Modal.Kripke.instDefinedByFiniteFrameClassOfHilbertExtKOfFiniteFrameClassOfTheory = { define := , nonempty := }
                            Equations
                            • LO.Modal.Kripke.instCharacteraizableFiniteFrameClassOfHilbertExtKOfFiniteFrameClassOfTheory = { characterize := , nonempty := }
                            theorem LO.Modal.Kripke.sound {α : Type u} {Λ : LO.Modal.Hilbert α} {p : LO.Modal.Formula α} :
                            Λ ⊢! p𝔽(Λ) p
                            Equations
                            Equations
                            • LO.Modal.Kripke.K_definability = .mpr LO.Modal.Kripke.K_definability'
                            theorem LO.Modal.Kripke.restrict_finite {α : Type u_1} {𝔽 : LO.Kripke.FrameClass} {p : LO.Modal.Formula α} :
                            𝔽#α p𝔽#α p
                            theorem LO.Modal.Kripke.exists_finite_frame {α : Type u_1} {𝔽 : LO.Kripke.FrameClass} {p : LO.Modal.Formula α} :
                            ¬𝔽#α p F𝔽, ¬F.toFrame#α p
                            Instances
                              theorem LO.Modal.weakerThan_of_subset_FrameClass {α : Type u_2} {Ax₁ : LO.Modal.Theory α} {Ax₂ : LO.Modal.Theory α} (𝔽₁ : LO.Kripke.FrameClass) (𝔽₂ : LO.Kripke.FrameClass) [sound₁ : LO.Sound (𝜿Ax₁) 𝔽₁#α] [complete₂ : LO.Complete (𝜿Ax₂) 𝔽₂#α] (h𝔽 : 𝔽₂ 𝔽₁) :
                              𝜿Ax₁ ≤ₛ 𝜿Ax₂
                              theorem LO.Modal.equiv_of_eq_FrameClass {α : Type u_2} {Ax₁ : LO.Modal.Theory α} {Ax₂ : LO.Modal.Theory α} (𝔽₁ : LO.Kripke.FrameClass) (𝔽₂ : LO.Kripke.FrameClass) [sound₁ : LO.Sound (𝜿Ax₁) 𝔽₁#α] [sound₂ : LO.Sound (𝜿Ax₂) 𝔽₂#α] [complete₁ : LO.Complete (𝜿Ax₁) 𝔽₁#α] [complete₂ : LO.Complete (𝜿Ax₂) 𝔽₂#α] (h𝔽 : 𝔽₁ = 𝔽₂) :
                              𝜿Ax₁ =ₛ 𝜿Ax₂