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

• kreisel_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.kreisel_putnam {F : Frame} [F.SatisfiesKreiselPutnamCondition] (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.instSatisfiesKreiselPutnamConditionWhitepoint : whitepoint.SatisfiesKreiselPutnamCondition

@[simp]

theorem LO.Propositional.Kripke.validate_axiomKreiselPutnam_of_satisfiesKreiselPutnamCondition {F : Frame} {φ ψ χ : Formula ℕ} [F.SatisfiesKreiselPutnamCondition] : F ⊧ Axioms.KreiselPutnam φ ψ χ

instance LO.Propositional.Kripke.Canonical.instSatisfiesKreiselPutnamConditionCanonicalFrameOfHasAxiomKreiselPutnamFormulaNat {S : Type u_1} [Entailment S (Formula ℕ)] {𝓢 : S} [Entailment.Consistent 𝓢] [Entailment.Int 𝓢] [Entailment.HasAxiomKreiselPutnam 𝓢] : (canonicalFrame 𝓢).SatisfiesKreiselPutnamCondition