AxiomGrz

@[reducible, inline]

abbrev LO.Modal.Kripke.ReflexiveTransitiveWeaklyConverseWellFoundedFrameClass : FrameClass

Imported declaration from the Incompleteness formalization.

Equations

• LO.Modal.Kripke.ReflexiveTransitiveWeaklyConverseWellFoundedFrameClass = {F : LO.Modal.Kripke.Frame | Std.Refl F.Rel ∧ IsTrans F.World F.Rel ∧ WeaklyConverseWellFounded F.Rel}

@[reducible, inline]

abbrev LO.Modal.Kripke.ReflexiveTransitiveAntiSymmetricFiniteFrameClass : FiniteFrameClass

Imported declaration from the Incompleteness formalization.

Equations

• LO.Modal.Kripke.ReflexiveTransitiveAntiSymmetricFiniteFrameClass = {F : LO.Modal.Kripke.FiniteFrame | Std.Refl F.Rel ∧ IsTrans F.World F.Rel ∧ Std.Antisymm F.Rel}

theorem LO.Modal.Kripke.validate_Grz_of_refl_trans_wcwf {F : Frame} (hRefl : Std.Refl F.Rel) (hTrans : IsTrans F.World F.Rel) (hWCWF : WeaklyConverseWellFounded F.Rel) : F ⊧ Axioms.Grz (Formula.atom 0)

theorem LO.Modal.Kripke.validate_T_Four_of_validate_Grz {F : Frame} (h : F ⊧ Axioms.Grz (Formula.atom 0)) : F ⊧ □Formula.atom 0 ==> Formula.atom 0 ⋏ □□Formula.atom 0

theorem LO.Modal.Kripke.validate_T_of_validate_Grz {F : Frame} (h : F ⊧ Axioms.Grz (Formula.atom 0)) : F ⊧ Axioms.T (Formula.atom 0)

theorem LO.Modal.Kripke.reflexive_of_validate_Grz {F : Frame} (h : F ⊧ Axioms.Grz (Formula.atom 0)) : Std.Refl F.Rel

theorem LO.Modal.Kripke.validate_Four_of_validate_Grz {F : Frame} (h : F ⊧ Axioms.Grz (Formula.atom 0)) : F ⊧ Axioms.Four (Formula.atom 0)

theorem LO.Modal.Kripke.transitive_of_validate_Grz {F : Frame} (h : F ⊧ Axioms.Grz (Formula.atom 0)) : IsTrans F.World F.Rel

theorem LO.Modal.Kripke.WCWF_of_validate_Grz {F : Frame} (h : F ⊧ Axioms.Grz (Formula.atom 0)) : WCWF F.Rel

instance LO.Modal.Kripke.ReflexiveTransitiveWeaklyConverseWellFoundedFrameClass.definedByAxiomGrz : ReflexiveTransitiveWeaklyConverseWellFoundedFrameClass.DefinedByFormula (Axioms.Grz (Formula.atom 0))

instance LO.Modal.Kripke.ReflexiveTransitiveAntiSymmetricFiniteFrameClass.definedByAxiomGrz : ReflexiveTransitiveAntiSymmetricFiniteFrameClass.DefinedByFormula (Axioms.Grz (Formula.atom 0))