@[reducible, inline]

abbrev LO.Propositional.Kripke.Frame.IsPiecewiseStronglyConvergent (F : Frame) : Prop

Equations

• F.IsPiecewiseStronglyConvergent = IsPiecewiseStronglyConvergent F.Rel

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

instance LO.Propositional.Kripke.instIsPiecewiseStronglyConvergentWhitepoint : whitepoint.IsPiecewiseStronglyConvergent

@[simp]

theorem LO.Propositional.Kripke.validate_axiomWLEM_of_isPiecewiseStronglyConvergent {F : Frame} {φ : Formula ℕ} [F.IsPiecewiseStronglyConvergent] : F ⊧ Axioms.WLEM φ

theorem LO.Propositional.Kripke.isPiecewiseStronglyConvergent_of_validate_axiomWLEM {F : Frame} (h : F ⊧ Axioms.WLEM #0) : F.IsPiecewiseStronglyConvergent

instance LO.Propositional.Kripke.instIsPiecewiseStronglyConvergentCanonicalFrameOfHasAxiomWLEMFormulaNat {S : Type u_1} [Entailment S (Formula ℕ)] {𝓢 : S} [Entailment.Consistent 𝓢] [Entailment.Int 𝓢] [Entailment.HasAxiomWLEM 𝓢] : (canonicalFrame 𝓢).IsPiecewiseStronglyConvergent