Documentation

Foundation.Modal.Kripke.AxiomL

source
@[reducible, inline]
abbrev LO.Modal.Kripke.Frame.IsConverseWellFounded (F : Frame) :
Prop
Equations
Instances For
    source
    theorem LO.Modal.Kripke.Frame.cwf {F : Frame} [F.IsConverseWellFounded] :
    ConverseWellFounded F.Rel
    source
    instance LO.Modal.Kripke.instIsConverseWellFoundedOfIsFiniteOfIsTransitiveOfIsIrreflexive {F : Frame} [F.IsFinite] [F.IsTransitive] [F.IsIrreflexive] :
    F.IsConverseWellFounded
    source
    instance LO.Modal.Kripke.instIsIrreflexiveOfIsConverseWellFounded {F : Frame} [F.IsConverseWellFounded] :
    F.IsIrreflexive
    source
    theorem LO.Modal.Kripke.validate_AxiomL_of_trans_cwf {F : Frame} {φ : Formula ℕ} [F.IsTransitive] [F.IsConverseWellFounded] :
    F ⊧ Axioms.L φ
    source
    theorem LO.Modal.Kripke.validate_AxiomL_of_finite_trans_irrefl {F : Frame} {φ : Formula ℕ} [F.IsFinite] [F.IsTransitive] [F.IsIrreflexive] :
    F ⊧ Axioms.L φ
    source
    theorem LO.Modal.Kripke.isTransitive_of_validate_axiomL {F : Frame} (h : F ⊧ Axioms.L (Formula.atom 0)) :
    F.IsTransitive
    source
    theorem LO.Modal.Kripke.isConverseWellFounded_of_validate_axiomL {F : Frame} (h : F ⊧ Axioms.L (Formula.atom 0)) :
    F.IsConverseWellFounded