Documentation

Foundation.Propositional.Kripke2.AxiomSym

source
@[reducible, inline]
abbrev LO.Propositional.Kripke2.Frame.IsSymmetric (F : Frame) :
Prop
Equations
Instances For
    source
    @[simp]
    theorem LO.Propositional.Kripke2.Frame.symm {F : Frame} [F.IsSymmetric] {x y : F.World} :
    x ≺ y → y ≺ x
    source
    instance LO.Propositional.Kripke2.Frame.instIsSerialOfIsSymmetric {F : Frame} [F.IsSymmetric] :
    F.IsSerial
    source
    @[simp]
    theorem LO.Propositional.Kripke2.valid_axiomSym_of_isSymmetric {F : Frame} {φ ψ : Formula ℕ} [F.IsSymmetric] :
    F ⊧ Axioms.Sym φ ψ
    source
    theorem LO.Propositional.Kripke2.isSymmetric_of_valid_axiomSym {F : Frame} (h : F ⊧ Axioms.Sym #0 #1) :
    F.IsSymmetric