AxiomL

@[reducible, inline]

abbrev LO.Modal.Kripke.TransitiveConverseWellFoundedFrameClass : FrameClass

Imported declaration from the Incompleteness formalization.

Equations

• LO.Modal.Kripke.TransitiveConverseWellFoundedFrameClass = {F : LO.Modal.Kripke.Frame | IsTrans F.World F.Rel ∧ ConverseWellFounded F.Rel}

@[reducible, inline]

abbrev LO.Modal.Kripke.TransitiveIrreflexiveFiniteFrameClass : FiniteFrameClass

Imported declaration from the Incompleteness formalization.

Equations

• LO.Modal.Kripke.TransitiveIrreflexiveFiniteFrameClass = {F : LO.Modal.Kripke.FiniteFrame | IsTrans F.World F.Rel ∧ Std.Irrefl F.Rel}

theorem LO.Modal.Kripke.validate_L_of_trans_and_cwf {F : Frame} (hTrans : IsTrans F.World F.Rel) (hCWF : ConverseWellFounded F.Rel) : F ⊧ Axioms.L (Formula.atom 0)

theorem LO.Modal.Kripke.trans_of_validate_L {F : Frame} : F ⊧ Axioms.L (Formula.atom 0) → IsTrans F.World F.Rel

theorem LO.Modal.Kripke.cwf_of_validate_L {F : Frame} : F ⊧ Axioms.L (Formula.atom 0) → ConverseWellFounded F.Rel

instance LO.Modal.Kripke.TransitiveConverseWellFoundedFrameClass.DefinedByL : TransitiveConverseWellFoundedFrameClass.DefinedByFormula (Axioms.L (Formula.atom 0))

instance LO.Modal.Kripke.TransitiveIrreflexiveFiniteFrameClass.DefinedByL : TransitiveIrreflexiveFiniteFrameClass.DefinedByFormula (Axioms.L (Formula.atom 0))