Documentation

Foundation.Modal.Kripke.Logic.K4n

source
@[reducible, inline]
abbrev LO.Modal.Kripke.Frame.IsK4n (F : Frame) (n : ℕ) :
Prop
Equations
Instances For
    source
    @[reducible, inline]
    abbrev LO.Modal.Kripke.FrameClass.K4n (n : ℕ) :
    FrameClass
    Equations
    Instances For
      source
      instance LO.Modal.K4n.instSoundLogicNatFormulaFrameClassK4n {n : ℕ} :
      Sound (Modal.K4n n) (Kripke.FrameClass.K4n n)
      source
      instance LO.Modal.K4n.instConsistentFormulaNatLogic {n : ℕ} :
      Entailment.Consistent (Modal.K4n n)
      source
      instance LO.Modal.K4n.instCanonicalLogicNatK4n {n : ℕ} :
      Kripke.Canonical (Modal.K4n n) (Kripke.FrameClass.K4n n)
      source
      instance LO.Modal.K4n.instCompleteLogicNatFormulaFrameClassK4n {n : ℕ} :
      Complete (Modal.K4n n) (Kripke.FrameClass.K4n n)
      source
      @[reducible, inline]
      abbrev LO.Modal.K4n.counterframe (n : ℕ) :
      Kripke.Frame
      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        @[reducible, inline]
        abbrev LO.Modal.K4n.counterframe.last {n : ℕ} :
        (counterframe n).World
        Equations
        Instances For
          source
          theorem LO.Modal.K4n.counterframe.iff_rel_from_zero {n m : ℕ} {x : (counterframe n).World} :
          0 ≺^[m] x ↔ ↑x = min m (n + 1)
          source
          theorem LO.Modal.K4n.counterframe.iff_rel_from {n : ℕ} {i j : (counterframe n).World} {m : ℕ} :
          i ≺^[m] j ↔ ↑j = min (↑i + m) (n + 1)
          source
          instance LO.Modal.K4n.instIsWeakTransitiveCounterframeHAddNatOfNat {n : ℕ} :
          (counterframe n).IsWeakTransitive (n + 1)
          source
          instance LO.Modal.K4n.instStrictlyWeakerThanFormulaNatLogicK {n : ℕ} :
          Modal.K ⪱ Modal.K4n n
          source
          theorem LO.Modal.K4n.succ_strictlyWeakerThan {n : ℕ} :
          Modal.K4n (n + 1) ⪱ Modal.K4n n
          source
          theorem LO.Modal.K4n.add_strictlyWeakerThan {n : ℕ} {m : ℕ+} :
          Modal.K4n (n + ↑m) ⪱ Modal.K4n n
          source
          theorem LO.Modal.K4n.strictlyWeakerThan_of_lt {n m : ℕ} (hnm : n < m) :
          Modal.K4n m ⪱ Modal.K4n n
          source
          theorem LO.Modal.K4n.not_equiv_of_ne {n m : ℕ} (hnm : n ≠ m) :
          ¬Modal.K4n n ≊ Modal.K4n m
          source
          instance LO.Modal.K4n.instInfiniteSubtypeLogicNatAndNonemptyIsNormalConsistentFormula :
          Infinite { L : Logic ℕ // Nonempty L.IsNormal ∧ Entailment.Consistent L }
          source
          instance LO.Modal.K4n.instEquivFormulaNatLogicOfNatKTc :
          Modal.K4n 0 ≊ Modal.KTc
          source
          instance LO.Modal.K4n.instEquivFormulaNatLogicOfNatK4 :
          Modal.K4n 1 ≊ Modal.K4
          source
          instance LO.Modal.K4n.instStrictlyWeakerThanFormulaNatLogicOfNat :
          Modal.K4n 1 ⪱ Modal.K4n 0
          source
          instance LO.Modal.K4n.instStrictlyWeakerThanFormulaNatLogicOfNat_1 :
          Modal.K4n 2 ⪱ Modal.K4n 1