Documentation

Foundation.IntProp.Kripke.DP

source
@[reducible, inline]
abbrev LO.IntProp.Kripke.counterexampleDPFrame (F₁ F₂ : LO.IntProp.Kripke.Frame) (w₁ : F₁.World) (w₂ : F₂.World) :
LO.IntProp.Kripke.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₂ : LO.IntProp.Kripke.Model) (w₁ : M₁.World) (w₂ : M₂.World) :
    LO.IntProp.Kripke.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 {φ : LO.IntProp.Formula ℕ} {M₁ M₂ : LO.IntProp.Kripke.Model} {w w₁ : M₁.World} {w₂ : M₂.World} :
      w ⊧ φ ↔ LO.IntProp.Formula.Kripke.Satisfies (LO.IntProp.Kripke.counterexampleDPModel M₁ M₂ w₁ w₂) (Sum.inr (Sum.inl w)) φ
      source
      theorem LO.IntProp.Kripke.satisfies_right_on_counterexampleDPModel {φ : LO.IntProp.Formula ℕ} {M₁ M₂ : LO.IntProp.Kripke.Model} {w : M₂.World} {w₁ : M₁.World} {w₂ : M₂.World} :
      w ⊧ φ ↔ LO.IntProp.Formula.Kripke.Satisfies (LO.IntProp.Kripke.counterexampleDPModel M₁ M₂ w₁ w₂) (Sum.inr (Sum.inr w)) φ
      source
      theorem LO.IntProp.Hilbert.Int.disjunctive {φ ψ : LO.IntProp.Formula ℕ} :
      LO.IntProp.Hilbert.Int ℕ ⊢! φ ⋎ ψ → LO.IntProp.Hilbert.Int ℕ ⊢! φ ∨ LO.IntProp.Hilbert.Int ℕ ⊢! ψ
      source
      instance LO.IntProp.Hilbert.Int.instDisjunctiveFormulaNat :
      LO.System.Disjunctive (LO.IntProp.Hilbert.Int ℕ)
      Equations