Documentation

Foundation.IntProp.Kripke.Semantics

@[simp]
theorem LO.IntProp.Formula.Kripke.Satisfies.atom_def {α : Type u} {M : LO.Kripke.Model α} {w : M.World} {a : α} :
w LO.IntProp.Formula.atom a M.Valuation w a
@[simp]
@[simp]
@[simp]
theorem LO.IntProp.Formula.Kripke.Satisfies.and_def {α : Type u} {M : LO.Kripke.Model α} {w : M.World} {p : LO.IntProp.Formula α} {q : LO.IntProp.Formula α} :
w p q w p w q
@[simp]
theorem LO.IntProp.Formula.Kripke.Satisfies.or_def {α : Type u} {M : LO.Kripke.Model α} {w : M.World} {p : LO.IntProp.Formula α} {q : LO.IntProp.Formula α} :
w p q w p w q
@[simp]
theorem LO.IntProp.Formula.Kripke.Satisfies.imp_def {α : Type u} {M : LO.Kripke.Model α} {w : M.World} {p : LO.IntProp.Formula α} {q : LO.IntProp.Formula α} :
w p q ∀ {w' : M.World}, w w'w' pw' q
@[simp]
theorem LO.IntProp.Formula.Kripke.Satisfies.neg_def {α : Type u} {M : LO.Kripke.Model α} {w : M.World} {p : LO.IntProp.Formula α} :
w p ∀ {w' : M.World}, w w'¬w' p
Equations
  • LO.IntProp.Formula.Kripke.Satisfies.instTopWorld = { realize_top := }
Equations
  • LO.IntProp.Formula.Kripke.Satisfies.instBotWorld = { realize_bot := }
Equations
  • LO.IntProp.Formula.Kripke.Satisfies.instAndWorld = { realize_and := }
Equations
  • LO.IntProp.Formula.Kripke.Satisfies.instOrWorld = { realize_or := }
theorem LO.IntProp.Formula.Kripke.Satisfies.formula_hereditary {α : Type u} {M : LO.Kripke.Model α} {w : M.World} {p : LO.IntProp.Formula α} {w' : M.Frame.World} (herditary : M.Valuation.atomic_hereditary) (F_trans : Transitive M.Frame.Rel) (hw : w w') :
w pw' p
Equations
Instances For
    Equations
    theorem LO.IntProp.Formula.Kripke.ValidOnModel.and₃ {α : Type u} {M : LO.Kripke.Model α} {p : LO.IntProp.Formula α} {q : LO.IntProp.Formula α} (atom_hereditary : ∀ {w₁ w₂ : M.World}, w₁ w₂∀ {a : α}, M.Valuation w₁ aM.Valuation w₂ a) (F_trans : autoParam (Transitive M.Frame.Rel) _auto✝) :
    M p q p q
    theorem LO.IntProp.Formula.Kripke.ValidOnModel.or₃ {α : Type u} {M : LO.Kripke.Model α} {p : LO.IntProp.Formula α} {q : LO.IntProp.Formula α} {r : LO.IntProp.Formula α} (F_trans : autoParam (Transitive M.Frame.Rel) _auto✝) :
    M (p r) (q r) p q r
    theorem LO.IntProp.Formula.Kripke.ValidOnModel.imply₁ {α : Type u} {M : LO.Kripke.Model α} {p : LO.IntProp.Formula α} {q : LO.IntProp.Formula α} (atom_hereditary : ∀ {w₁ w₂ : M.World}, w₁ w₂∀ {a : α}, M.Valuation w₁ aM.Valuation w₂ a) (F_trans : autoParam (Transitive M.Frame.Rel) _auto✝) :
    M p q p
    theorem LO.IntProp.Formula.Kripke.ValidOnModel.imply₂ {α : Type u} {M : LO.Kripke.Model α} {p : LO.IntProp.Formula α} {q : LO.IntProp.Formula α} {r : LO.IntProp.Formula α} (F_trans : autoParam (Transitive M.Frame.Rel) _auto✝) (F_refl : autoParam (Reflexive M.Frame.Rel) _auto✝) :
    M (p q r) (p q) p r
    theorem LO.IntProp.Formula.Kripke.ValidOnModel.mdp {α : Type u} {M : LO.Kripke.Model α} {p : LO.IntProp.Formula α} {q : LO.IntProp.Formula α} (F_refl : autoParam (Reflexive M.Frame.Rel) _auto✝) (hpq : M p q) (hp : M p) :
    M q
    theorem LO.IntProp.Formula.Kripke.ValidOnModel.lem {α : Type u} {M : LO.Kripke.Model α} {p : LO.IntProp.Formula α} (atom_hereditary : ∀ {w₁ w₂ : M.World}, w₁ w₂∀ {a : α}, M.Valuation w₁ aM.Valuation w₂ a) (F_trans : autoParam (Transitive M.Frame.Rel) _auto✝) :
    Symmetric M.Frame.RelM LO.Axioms.LEM p
    theorem LO.IntProp.Formula.Kripke.ValidOnModel.dum {α : Type u} {M : LO.Kripke.Model α} {p : LO.IntProp.Formula α} {q : LO.IntProp.Formula α} (atom_hereditary : ∀ {w₁ w₂ : M.World}, w₁ w₂∀ {a : α}, M.Valuation w₁ aM.Valuation w₂ a) (F_trans : autoParam (Transitive M.Frame.Rel) _auto✝) :
    Connected M.Frame.RelM LO.Axioms.GD p q
    theorem LO.IntProp.Formula.Kripke.ValidOnModel.wlem {α : Type u} {M : LO.Kripke.Model α} {p : LO.IntProp.Formula α} (atom_hereditary : ∀ {w₁ w₂ : M.World}, w₁ w₂∀ {a : α}, M.Valuation w₁ aM.Valuation w₂ a) (F_trans : autoParam (Transitive M.Frame.Rel) _auto✝) :
    Confluent M.Frame.RelM LO.Axioms.WeakLEM p
    Equations
    Instances For
      Equations
      theorem LO.IntProp.Formula.Kripke.ValidOnFrame.imply₂ {α : Type u} {F : LO.Kripke.Frame.Dep α} {p : LO.IntProp.Formula α} {q : LO.IntProp.Formula α} {r : LO.IntProp.Formula α} (F_trans : Transitive F.Rel) (F_refl : Reflexive F.Rel) :
      F (p q r) (p q) p r
      theorem LO.IntProp.Formula.Kripke.ValidOnFrame.mdp {α : Type u} {F : LO.Kripke.Frame.Dep α} {p : LO.IntProp.Formula α} {q : LO.IntProp.Formula α} (F_refl : Reflexive F.Rel) (hpq : F p q) (hp : F p) :
      F q
      theorem LO.IntProp.Formula.Kripke.ValidOnFrame.dum {α : Type u} {F : LO.Kripke.Frame.Dep α} {p : LO.IntProp.Formula α} {q : LO.IntProp.Formula α} (F_trans : Transitive F.Rel) (F_conn : Connected F.Rel) :
      Equations
      • LO.IntProp.Formula.Kripke.ValidOnFrame.instBotDep = { realize_bot := }
      Equations
      @[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
              theorem LO.IntProp.Kripke.sound {α : Type u} {Λ : LO.IntProp.Hilbert α} {p : LO.IntProp.Formula α} :
              Λ ⊢! p𝔽(Λ) p
              theorem LO.IntProp.Kripke.sound_of_characterizability {α : Type u} {Λ : LO.IntProp.Hilbert α} {p : LO.IntProp.Formula α} {𝔽₂ : LO.Kripke.FrameClass} [characterizability : LO.Kripke.FrameClass.Characteraizable 𝔽(Λ) 𝔽₂] :
              Λ ⊢! p𝔽₂#α p
              Equations
              • LO.IntProp.Kripke.Cl_Characteraizable = { characterize := , nonempty := }
              Equations
              • LO.IntProp.Formula.Kripke.instSemanticsClassicalValuation = { Realize := LO.IntProp.Formula.Kripke.ClassicalSatisfies }
              Equations
              • LO.IntProp.Formula.Kripke.ClassicalSatisfies.instTarskiClassicalValuation = LO.Semantics.Tarski.mk