@[reducible, inline]

abbrev LO.IntProp.Kripke.IntDPCounterexampleFrame (F₁ : LO.Kripke.Frame) (F₂ : LO.Kripke.Frame) (w₁ : F₁.World) (w₂ : F₂.World) : LO.Kripke.Frame

Equations

• One or more equations did not get rendered due to their size.

theorem LO.IntProp.Kripke.IntDPCounterexampleFrame.reflexive {F₁ : LO.Kripke.Frame} {F₂ : LO.Kripke.Frame} {w₁ : F₁.World} {w₂ : F₂.World} (F₁_refl : Reflexive F₁.Rel) (F₂_refl : Reflexive F₂.Rel) : Reflexive (LO.IntProp.Kripke.IntDPCounterexampleFrame F₁ F₂ w₁ w₂).Rel

theorem LO.IntProp.Kripke.IntDPCounterexampleFrame.transitive {F₁ : LO.Kripke.Frame} {F₂ : LO.Kripke.Frame} {w₁ : F₁.World} {w₂ : F₂.World} (F₁_trans : Transitive F₁.Rel) (F₂_trans : Transitive F₂.Rel) : Transitive (LO.IntProp.Kripke.IntDPCounterexampleFrame F₁ F₂ w₁ w₂).Rel

theorem LO.IntProp.Kripke.IntDPCounterexampleFrame.antisymmetric {F₁ : LO.Kripke.Frame} {F₂ : LO.Kripke.Frame} {w₁ : F₁.World} {w₂ : F₂.World} (F₁_antisymm : Antisymmetric F₁.Rel) (F₂_antisymm : Antisymmetric F₂.Rel) : Antisymmetric (LO.IntProp.Kripke.IntDPCounterexampleFrame F₁ F₂ w₁ w₂).Rel

@[reducible, inline]

abbrev LO.IntProp.Kripke.IntDPCounterexampleModel {α : Type u_1} (M₁ : LO.Kripke.Model α) (M₂ : LO.Kripke.Model α) (w₁ : M₁.World) (w₂ : M₂.World) : LO.Kripke.Model α

Equations

• One or more equations did not get rendered due to their size.

theorem LO.IntProp.Kripke.IntDPCounterexampleModel.atomic_hereditary {α : Type u_1} {M₁ : LO.Kripke.Model α} {M₂ : LO.Kripke.Model α} {w₁ : M₁.World} {w₂ : M₂.World} (M₁_hered : M₁.Valuation.atomic_hereditary) (M₂_hered : M₂.Valuation.atomic_hereditary) : (LO.IntProp.Kripke.IntDPCounterexampleModel M₁ M₂ w₁ w₂).Valuation.atomic_hereditary

theorem LO.IntProp.Kripke.satisfies_left_on_IntDPCounterexampleModel {α : Type u_1} {p : LO.IntProp.Formula α} {M₁ : LO.Kripke.Model α} {M₂ : LO.Kripke.Model α} {w : M₁.World} {w₁ : M₁.World} {w₂ : M₂.World} : LO.IntProp.Formula.Kripke.Satisfies M₁ w p ↔ LO.IntProp.Formula.Kripke.Satisfies (LO.IntProp.Kripke.IntDPCounterexampleModel M₁ M₂ w₁ w₂) (Sum.inr (Sum.inl w)) p

theorem LO.IntProp.Kripke.satisfies_right_on_IntDPCounterexampleModel {α : Type u_1} {p : LO.IntProp.Formula α} {M₁ : LO.Kripke.Model α} {M₂ : LO.Kripke.Model α} {w : M₂.World} {w₁ : M₁.World} {w₂ : M₂.World} : LO.IntProp.Formula.Kripke.Satisfies M₂ w p ↔ LO.IntProp.Formula.Kripke.Satisfies (LO.IntProp.Kripke.IntDPCounterexampleModel M₁ M₂ w₁ w₂) (Sum.inr (Sum.inr w)) p

theorem LO.IntProp.Kripke.disjunctive_int {α : Type u_1} [DecidableEq α] [Encodable α] {p : LO.IntProp.Formula α} {q : LO.IntProp.Formula α} : 𝐈𝐧𝐭 ⊢! p ⋎ q → 𝐈𝐧𝐭 ⊢! p ∨ 𝐈𝐧𝐭 ⊢! q

instance LO.IntProp.Kripke.instDisjunctiveFormulaHilbertIntuitionistic {α : Type u_1} [DecidableEq α] [Encodable α] : LO.System.Disjunctive 𝐈𝐧𝐭

Equations

• ⋯ = ⋯