@[reducible, inline]

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

Equations

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

@[reducible, inline]

abbrev LO.IntProp.Kripke.counterexampleDPModel (M₁ M₂ : Model) (w₁ : M₁.World) (w₂ : M₂.World) : Model

Equations

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

theorem LO.IntProp.Kripke.satisfies_left_on_counterexampleDPModel {φ : Formula ℕ} {M₁ M₂ : Model} {w w₁ : M₁.World} {w₂ : M₂.World} : w ⊧ φ ↔ Formula.Kripke.Satisfies (counterexampleDPModel M₁ M₂ w₁ w₂) (Sum.inr (Sum.inl w)) φ

theorem LO.IntProp.Kripke.satisfies_right_on_counterexampleDPModel {φ : Formula ℕ} {M₁ M₂ : Model} {w : M₂.World} {w₁ : M₁.World} {w₂ : M₂.World} : w ⊧ φ ↔ Formula.Kripke.Satisfies (counterexampleDPModel M₁ M₂ w₁ w₂) (Sum.inr (Sum.inr w)) φ

theorem LO.IntProp.Hilbert.Int.disjunctive {φ ψ : Formula ℕ} : Hilbert.Int ℕ ⊢! φ ⋎ ψ → Hilbert.Int ℕ ⊢! φ ∨ Hilbert.Int ℕ ⊢! ψ

instance LO.IntProp.Hilbert.Int.instDisjunctiveFormulaNat : System.Disjunctive (Hilbert.Int ℕ)