class LO.Propositional.Kripke.Frame.SatisfiesKriselPutnamCondition (F : Frame) : Prop

• kriesel_putnam (x y z : F.World) : x ≺ y ∧ x ≺ z ∧ ¬y ≺ z ∧ ¬z ≺ y → ∃ (u : F.World), x ≺ u ∧ u ≺ y ∧ u ≺ z ∧ ∀ (v : F.World), u ≺ v → ∃ (w : F.World), v ≺ w ∧ (y ≺ w ∨ z ≺ w)

theorem LO.Propositional.Kripke.Frame.kriesel_putnam {F : Frame} [F.SatisfiesKriselPutnamCondition] (x y z : F.World) : x ≺ y ∧ x ≺ z ∧ ¬y ≺ z ∧ ¬z ≺ y → ∃ (u : F.World), x ≺ u ∧ u ≺ y ∧ u ≺ z ∧ ∀ (v : F.World), u ≺ v → ∃ (w : F.World), v ≺ w ∧ (y ≺ w ∨ z ≺ w)

instance LO.Propositional.Kripke.instSatisfiesKriselPutnamConditionWhitepoint : whitepoint.SatisfiesKriselPutnamCondition

theorem LO.Propositional.Kripke.validate_axiomKrieselPutnam_of_satisfiesKrieselPutnamCondition {F : Frame} [F.SatisfiesKriselPutnamCondition] : F ⊧ Axioms.KrieselPutnam (Formula.atom 0) (Formula.atom 1) (Formula.atom 2)

instance LO.Propositional.Kripke.Canonical.instSatisfiesKriselPutnamConditionCanonicalFrameOfHasAxiomKrieselPutnamFormulaNat {S : Type u_1} [Entailment (Formula ℕ) S] {𝓢 : S} [Entailment.Consistent 𝓢] [Entailment.Int 𝓢] [Entailment.HasAxiomKrieselPutnam 𝓢] : (canonicalFrame 𝓢).SatisfiesKriselPutnamCondition