Documentation

Foundation.IntProp.Kripke.DP

source
@[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.
Instances For
    source
    @[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.
    Instances For
      source
      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)) φ
      source
      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)) φ
      source
      theorem LO.IntProp.Hilbert.Int.disjunctive {φ ψ : Formula ℕ} :
      Hilbert.Int ℕ ⊢! φ ⋎ ψ → Hilbert.Int ℕ ⊢! φ ∨ Hilbert.Int ℕ ⊢! ψ
      source
      instance LO.IntProp.Hilbert.Int.instDisjunctiveFormulaNat :
      System.Disjunctive (Hilbert.Int ℕ)