Documentation

Foundation.Propositional.Kripke.AxiomWLEM

source
@[reducible, inline]
abbrev LO.Propositional.Kripke.Frame.IsPiecewiseStronglyConvergent (F : Frame) :
Prop
Equations
Instances For
    source
    theorem LO.Propositional.Kripke.Frame.ps_convergent {F : Frame} [F.IsPiecewiseStronglyConvergent] ⦃x y z : F.World⦄ :
    x ≺ y → x ≺ z → ∃ (u : F.World), y ≺ u ∧ z ≺ u
    source
    instance LO.Propositional.Kripke.instIsPiecewiseStronglyConvergentWhitepoint :
    whitepoint.IsPiecewiseStronglyConvergent
    source
    theorem LO.Propositional.Kripke.validate_axiomWLEM_of_isPiecewiseStronglyConvergent {F : Frame} [F.IsPiecewiseStronglyConvergent] :
    F ⊧ Axioms.WLEM #0
    source
    theorem LO.Propositional.Kripke.isPiecewiseStronglyConvergent_of_validate_axiomWLEM {F : Frame} (h : F ⊧ Axioms.WLEM #0) :
    F.IsPiecewiseStronglyConvergent
    source
    instance LO.Propositional.Kripke.instIsPiecewiseStronglyConvergentCanonicalFrameOfHasAxiomWLEMFormulaNat {S : Type u_1} [Entailment S (Formula ℕ)] {𝓢 : S} [Entailment.Consistent 𝓢] [Entailment.Int 𝓢] [Entailment.HasAxiomWLEM 𝓢] :
    (canonicalFrame 𝓢).IsPiecewiseStronglyConvergent