Documentation

Foundation.IntProp.Kripke.Completeness

source
def LO.IntProp.Hilbert.Kripke.canonicalFrameOf (H : LO.IntProp.Hilbert ℕ) [H.Consistent] [H.IncludeEFQ] :
LO.IntProp.Kripke.Frame
Equations
Instances For
    source
    theorem LO.IntProp.Hilbert.Kripke.canonicalFrame.is_confluent {H : LO.IntProp.Hilbert ℕ} [H.IncludeEFQ] [H.Consistent] [LO.System.HasAxiomWeakLEM H] :
    Confluent (LO.IntProp.Hilbert.Kripke.canonicalFrameOf H).Rel
    source
    theorem LO.IntProp.Hilbert.Kripke.canonicalFrame.is_connected {H : LO.IntProp.Hilbert ℕ} [H.IncludeEFQ] [H.Consistent] [LO.System.HasAxiomDummett H] :
    Connected (LO.IntProp.Hilbert.Kripke.canonicalFrameOf H).Rel
    source
    def LO.IntProp.Hilbert.Kripke.canonicalModelOf (H : LO.IntProp.Hilbert ℕ) [H.Consistent] [H.IncludeEFQ] :
    LO.IntProp.Kripke.Model
    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      theorem LO.IntProp.Hilbert.Kripke.truthlemma {H : LO.IntProp.Hilbert ℕ} {φ : LO.IntProp.Formula ℕ} [H.IncludeEFQ] [H.Consistent] {t : (LO.IntProp.Hilbert.Kripke.canonicalModelOf H).World} :
      t ⊧ φ ↔ φ ∈ t.tableau.1
      source
      theorem LO.IntProp.Hilbert.Kripke.deducible_of_validOnCanonicelModel {H : LO.IntProp.Hilbert ℕ} {φ : LO.IntProp.Formula ℕ} [H.IncludeEFQ] [H.Consistent] :
      LO.IntProp.Hilbert.Kripke.canonicalModelOf H ⊧ φ ↔ H ⊢! φ
      source
      theorem LO.IntProp.Hilbert.Kripke.complete_of_canonical {H : LO.IntProp.Hilbert ℕ} {φ : LO.IntProp.Formula ℕ} [H.IncludeEFQ] [H.Consistent] {C : LO.IntProp.Kripke.FrameClass} (hC : LO.IntProp.Hilbert.Kripke.canonicalFrameOf H ∈ C) :
      C ⊧ φ → H ⊢! φ
      source
      instance LO.IntProp.Hilbert.Kripke.instCompleteOfCanonical {H : LO.IntProp.Hilbert ℕ} [H.IncludeEFQ] [H.Consistent] {C : LO.IntProp.Kripke.FrameClass} (hC : LO.IntProp.Hilbert.Kripke.canonicalFrameOf H ∈ C) :
      LO.Complete H C
      Equations
      • ⋯ = ⋯
      source
      instance LO.IntProp.Hilbert.Int.Kripke.complete :
      LO.Complete (LO.IntProp.Hilbert.Int ℕ) LO.IntProp.Kripke.AllFrameClass
      Equations
      source
      instance LO.IntProp.Hilbert.KC.Kripke.complete :
      LO.Complete (LO.IntProp.Hilbert.KC ℕ) LO.IntProp.Kripke.ConfluentFrameClass
      Equations
      source
      instance LO.IntProp.Hilbert.LC.Kripke.complete :
      LO.Complete (LO.IntProp.Hilbert.LC ℕ) LO.IntProp.Kripke.ConnectedFrameClass
      Equations