Documentation

Logic.Propositional.Superintuitionistic.Kripke.Completeness

source
def LO.Propositional.Superintuitionistic.Kripke.CanonicalFrame {α : Type u} (Λ : LO.Propositional.Superintuitionistic.DeductionParameter α) [Nonempty (LO.Propositional.Superintuitionistic.SCT Λ)] :
LO.Kripke.Frame.Dep α
Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    theorem LO.Propositional.Superintuitionistic.Kripke.CanonicalFrame.reflexive {α : Type u} {Λ : LO.Propositional.Superintuitionistic.DeductionParameter α} [Nonempty (LO.Propositional.Superintuitionistic.SCT Λ)] :
    Reflexive (LO.Propositional.Superintuitionistic.Kripke.CanonicalFrame Λ).Rel
    source
    theorem LO.Propositional.Superintuitionistic.Kripke.CanonicalFrame.antisymmetric {α : Type u} {Λ : LO.Propositional.Superintuitionistic.DeductionParameter α} [Nonempty (LO.Propositional.Superintuitionistic.SCT Λ)] :
    Antisymmetric (LO.Propositional.Superintuitionistic.Kripke.CanonicalFrame Λ).Rel
    source
    theorem LO.Propositional.Superintuitionistic.Kripke.CanonicalFrame.transitive {α : Type u} {Λ : LO.Propositional.Superintuitionistic.DeductionParameter α} [Nonempty (LO.Propositional.Superintuitionistic.SCT Λ)] :
    Transitive (LO.Propositional.Superintuitionistic.Kripke.CanonicalFrame Λ).Rel
    source
    theorem LO.Propositional.Superintuitionistic.Kripke.CanonicalFrame.confluent {α : Type u} [DecidableEq α] [Encodable α] {Λ : LO.Propositional.Superintuitionistic.DeductionParameter α} [Λ.IncludeEFQ] [Nonempty (LO.Propositional.Superintuitionistic.SCT Λ)] [LO.System.HasAxiomWeakLEM Λ] :
    Confluent (LO.Propositional.Superintuitionistic.Kripke.CanonicalFrame Λ).Rel
    source
    theorem LO.Propositional.Superintuitionistic.Kripke.CanonicalFrame.connected {α : Type u} [DecidableEq α] {Λ : LO.Propositional.Superintuitionistic.DeductionParameter α} [Nonempty (LO.Propositional.Superintuitionistic.SCT Λ)] [LO.System.HasAxiomDummett Λ] :
    Connected (LO.Propositional.Superintuitionistic.Kripke.CanonicalFrame Λ).Rel
    source
    def LO.Propositional.Superintuitionistic.Kripke.CanonicalModel {α : Type u} (Λ : LO.Propositional.Superintuitionistic.DeductionParameter α) [Nonempty (LO.Propositional.Superintuitionistic.SCT Λ)] :
    LO.Kripke.Model α
    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      theorem LO.Propositional.Superintuitionistic.Kripke.CanonicalModel.hereditary {α : Type u} {Λ : LO.Propositional.Superintuitionistic.DeductionParameter α} [Nonempty (LO.Propositional.Superintuitionistic.SCT Λ)] :
      (LO.Propositional.Superintuitionistic.Kripke.CanonicalModel Λ).Valuation.atomic_hereditary
      source
      @[reducible]
      instance LO.Propositional.Superintuitionistic.Kripke.CanonicalModel.instSemanticsFormulaWorld {α : Type u} {Λ : LO.Propositional.Superintuitionistic.DeductionParameter α} [Nonempty (LO.Propositional.Superintuitionistic.SCT Λ)] :
      LO.Semantics (LO.Propositional.Superintuitionistic.Formula α) (LO.Propositional.Superintuitionistic.Kripke.CanonicalModel Λ).World
      Equations
      • One or more equations did not get rendered due to their size.
      source
      @[simp]
      theorem LO.Propositional.Superintuitionistic.Kripke.CanonicalModel.frame_def {α : Type u} {Λ : LO.Propositional.Superintuitionistic.DeductionParameter α} [Nonempty (LO.Propositional.Superintuitionistic.SCT Λ)] {t₁ : LO.Propositional.Superintuitionistic.SCT Λ} {t₂ : LO.Propositional.Superintuitionistic.SCT Λ} :
      (LO.Propositional.Superintuitionistic.Kripke.CanonicalModel Λ).Frame.Rel t₁ t₂ ↔ t₁.tableau.1 ⊆ t₂.tableau.1
      source
      @[simp]
      theorem LO.Propositional.Superintuitionistic.Kripke.CanonicalModel.valuation_def {α : Type u} {Λ : LO.Propositional.Superintuitionistic.DeductionParameter α} [Nonempty (LO.Propositional.Superintuitionistic.SCT Λ)] {t : LO.Propositional.Superintuitionistic.SCT Λ} {a : α} :
      (LO.Propositional.Superintuitionistic.Kripke.CanonicalModel Λ).Valuation t a ↔ LO.Propositional.Superintuitionistic.Formula.atom a ∈ t.tableau.1
      source
      theorem LO.Propositional.Superintuitionistic.Kripke.truthlemma {α : Type u} [DecidableEq α] [Encodable α] {Λ : LO.Propositional.Superintuitionistic.DeductionParameter α} [Λ.IncludeEFQ] [Nonempty (LO.Propositional.Superintuitionistic.SCT Λ)] {p : LO.Propositional.Superintuitionistic.Formula α} {t : (LO.Propositional.Superintuitionistic.Kripke.CanonicalModel Λ).World} :
      t ⊧ p ↔ p ∈ t.tableau.1
      source
      theorem LO.Propositional.Superintuitionistic.Kripke.deducible_of_validOnCanonicelModel {α : Type u} [DecidableEq α] [Encodable α] {Λ : LO.Propositional.Superintuitionistic.DeductionParameter α} [Λ.IncludeEFQ] [Nonempty (LO.Propositional.Superintuitionistic.SCT Λ)] {p : LO.Propositional.Superintuitionistic.Formula α} :
      LO.Propositional.Superintuitionistic.Kripke.CanonicalModel Λ ⊧ p ↔ Λ ⊢! p
      source
      theorem LO.Propositional.Superintuitionistic.Kripke.complete {α : Type u} {Λ : LO.Propositional.Superintuitionistic.DeductionParameter α} [Λ.IncludeEFQ] [Nonempty (LO.Propositional.Superintuitionistic.SCT Λ)] [DecidableEq α] [Encodable α] {𝔽 : LO.Kripke.FrameClass} (H : LO.Propositional.Superintuitionistic.Kripke.CanonicalFrame Λ ∈ 𝔽) {p : LO.Propositional.Superintuitionistic.Formula α} :
      𝔽#α ⊧ p → Λ ⊢! p
      source
      instance LO.Propositional.Superintuitionistic.Kripke.instComplete {α : Type u} {Λ : LO.Propositional.Superintuitionistic.DeductionParameter α} [Λ.IncludeEFQ] [Nonempty (LO.Propositional.Superintuitionistic.SCT Λ)] [DecidableEq α] [Encodable α] {𝔽 : LO.Kripke.FrameClass} (H : LO.Propositional.Superintuitionistic.Kripke.CanonicalFrame Λ ∈ 𝔽) :
      LO.Complete Λ 𝔽#α
      Equations
      • ⋯ = ⋯
      source
      instance LO.Propositional.Superintuitionistic.Kripke.Int_complete {α : Type u} [DecidableEq α] [Encodable α] :
      LO.Complete 𝐈𝐧𝐭 LO.Kripke.ReflexiveTransitiveFrameClass#α
      Equations
      • ⋯ = ⋯
      source
      @[deprecated]
      theorem LO.Propositional.Superintuitionistic.Kripke.Int_complete_aux {α : Type u} {p : LO.Propositional.Superintuitionistic.Formula α} [DecidableEq α] [Encodable α] :
      LO.Kripke.ReflexiveTransitiveFrameClass#α ⊧ p → 𝐈𝐧𝐭 ⊢! p
      source
      instance LO.Propositional.Superintuitionistic.Kripke.LC_complete {α : Type u} [DecidableEq α] [Encodable α] :
      LO.Complete 𝐋𝐂 LO.Kripke.ReflexiveTransitiveConnectedFrameClass#α
      Equations
      • ⋯ = ⋯
      source
      instance LO.Propositional.Superintuitionistic.Kripke.KC_complete {α : Type u} [DecidableEq α] [Encodable α] :
      LO.Complete 𝐊𝐂 LO.Kripke.ReflexiveTransitiveConfluentFrameClass#α
      Equations
      • ⋯ = ⋯