def LO.IntProp.Hilbert.Kripke.canonicalFrameOf (H : Hilbert ℕ) [H.Consistent] [H.IncludeEFQ] : Kripke.Frame

Equations

• LO.IntProp.Hilbert.Kripke.canonicalFrameOf H = LO.IntProp.Kripke.Frame.mk (LO.IntProp.SCT H) fun (t₁ t₂ : LO.IntProp.SCT H) => t₁.tableau.1 ⊆ t₂.tableau.1

theorem LO.IntProp.Hilbert.Kripke.canonicalFrame.is_confluent {H : Hilbert ℕ} [H.IncludeEFQ] [H.Consistent] [System.HasAxiomWeakLEM H] : Confluent (canonicalFrameOf H).Rel

theorem LO.IntProp.Hilbert.Kripke.canonicalFrame.is_connected {H : Hilbert ℕ} [H.IncludeEFQ] [H.Consistent] [System.HasAxiomDummett H] : Connected (canonicalFrameOf H).Rel

def LO.IntProp.Hilbert.Kripke.canonicalModelOf (H : Hilbert ℕ) [H.Consistent] [H.IncludeEFQ] : Kripke.Model

Equations

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

theorem LO.IntProp.Hilbert.Kripke.truthlemma {H : Hilbert ℕ} {φ : Formula ℕ} [H.IncludeEFQ] [H.Consistent] {t : (canonicalModelOf H).World} : t ⊧ φ ↔ φ ∈ t.tableau.1

theorem LO.IntProp.Hilbert.Kripke.deducible_of_validOnCanonicelModel {H : Hilbert ℕ} {φ : Formula ℕ} [H.IncludeEFQ] [H.Consistent] : canonicalModelOf H ⊧ φ ↔ H ⊢! φ

theorem LO.IntProp.Hilbert.Kripke.complete_of_canonical {H : Hilbert ℕ} {φ : Formula ℕ} [H.IncludeEFQ] [H.Consistent] {C : Kripke.FrameClass} (hC : canonicalFrameOf H ∈ C) : C ⊧ φ → H ⊢! φ

instance LO.IntProp.Hilbert.Kripke.instCompleteOfCanonical {H : Hilbert ℕ} [H.IncludeEFQ] [H.Consistent] {C : Kripke.FrameClass} (hC : canonicalFrameOf H ∈ C) : Complete H C

instance LO.IntProp.Hilbert.Int.Kripke.complete : Complete (Hilbert.Int ℕ) Kripke.AllFrameClass

instance LO.IntProp.Hilbert.KC.Kripke.complete : Complete (Hilbert.KC ℕ) Kripke.ConfluentFrameClass

instance LO.IntProp.Hilbert.LC.Kripke.complete : Complete (Hilbert.LC ℕ) Kripke.ConnectedFrameClass