def LO.IntProp.Kripke.CanonicalFrame {α : Type u} (Λ : LO.IntProp.Hilbert α) [Nonempty (LO.IntProp.SCT Λ)] : LO.Kripke.Frame.Dep α

Equations

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

theorem LO.IntProp.Kripke.CanonicalFrame.reflexive {α : Type u} {Λ : LO.IntProp.Hilbert α} [Nonempty (LO.IntProp.SCT Λ)] : Reflexive (LO.IntProp.Kripke.CanonicalFrame Λ).Rel

theorem LO.IntProp.Kripke.CanonicalFrame.antisymmetric {α : Type u} {Λ : LO.IntProp.Hilbert α} [Nonempty (LO.IntProp.SCT Λ)] : Antisymmetric (LO.IntProp.Kripke.CanonicalFrame Λ).Rel

theorem LO.IntProp.Kripke.CanonicalFrame.transitive {α : Type u} {Λ : LO.IntProp.Hilbert α} [Nonempty (LO.IntProp.SCT Λ)] : Transitive (LO.IntProp.Kripke.CanonicalFrame Λ).Rel

theorem LO.IntProp.Kripke.CanonicalFrame.confluent {α : Type u} [DecidableEq α] [Encodable α] {Λ : LO.IntProp.Hilbert α} [Λ.IncludeEFQ] [Nonempty (LO.IntProp.SCT Λ)] [LO.System.HasAxiomWeakLEM Λ] : Confluent (LO.IntProp.Kripke.CanonicalFrame Λ).Rel

theorem LO.IntProp.Kripke.CanonicalFrame.connected {α : Type u} [DecidableEq α] {Λ : LO.IntProp.Hilbert α} [Nonempty (LO.IntProp.SCT Λ)] [LO.System.HasAxiomDummett Λ] : Connected (LO.IntProp.Kripke.CanonicalFrame Λ).Rel

def LO.IntProp.Kripke.CanonicalModel {α : Type u} (Λ : LO.IntProp.Hilbert α) [Nonempty (LO.IntProp.SCT Λ)] : LO.Kripke.Model α

Equations

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

theorem LO.IntProp.Kripke.CanonicalModel.hereditary {α : Type u} {Λ : LO.IntProp.Hilbert α} [Nonempty (LO.IntProp.SCT Λ)] : (LO.IntProp.Kripke.CanonicalModel Λ).Valuation.atomic_hereditary

@[reducible]

instance LO.IntProp.Kripke.CanonicalModel.instSemanticsFormulaWorld {α : Type u} {Λ : LO.IntProp.Hilbert α} [Nonempty (LO.IntProp.SCT Λ)] : LO.Semantics (LO.IntProp.Formula α) (LO.IntProp.Kripke.CanonicalModel Λ).World

Equations

• LO.IntProp.Kripke.CanonicalModel.instSemanticsFormulaWorld = LO.IntProp.Formula.Kripke.Satisfies.semantics (LO.IntProp.Kripke.CanonicalModel Λ)

@[simp]

theorem LO.IntProp.Kripke.CanonicalModel.frame_def {α : Type u} {Λ : LO.IntProp.Hilbert α} [Nonempty (LO.IntProp.SCT Λ)] {t₁ : LO.IntProp.SCT Λ} {t₂ : LO.IntProp.SCT Λ} : (LO.IntProp.Kripke.CanonicalModel Λ).Frame.Rel t₁ t₂ ↔ t₁.tableau.1 ⊆ t₂.tableau.1

@[simp]

theorem LO.IntProp.Kripke.CanonicalModel.valuation_def {α : Type u} {Λ : LO.IntProp.Hilbert α} [Nonempty (LO.IntProp.SCT Λ)] {t : LO.IntProp.SCT Λ} {a : α} : (LO.IntProp.Kripke.CanonicalModel Λ).Valuation t a ↔ LO.IntProp.Formula.atom a ∈ t.tableau.1

theorem LO.IntProp.Kripke.truthlemma {α : Type u} [DecidableEq α] [Encodable α] {Λ : LO.IntProp.Hilbert α} [Λ.IncludeEFQ] [Nonempty (LO.IntProp.SCT Λ)] {p : LO.IntProp.Formula α} {t : (LO.IntProp.Kripke.CanonicalModel Λ).World} : t ⊧ p ↔ p ∈ t.tableau.1

theorem LO.IntProp.Kripke.deducible_of_validOnCanonicelModel {α : Type u} [DecidableEq α] [Encodable α] {Λ : LO.IntProp.Hilbert α} [Λ.IncludeEFQ] [Nonempty (LO.IntProp.SCT Λ)] {p : LO.IntProp.Formula α} : LO.IntProp.Kripke.CanonicalModel Λ ⊧ p ↔ Λ ⊢! p

theorem LO.IntProp.Kripke.complete {α : Type u} {Λ : LO.IntProp.Hilbert α} [Λ.IncludeEFQ] [Nonempty (LO.IntProp.SCT Λ)] [DecidableEq α] [Encodable α] {𝔽 : LO.Kripke.FrameClass} (H : LO.IntProp.Kripke.CanonicalFrame Λ ∈ 𝔽) {p : LO.IntProp.Formula α} : 𝔽#α ⊧ p → Λ ⊢! p

instance LO.IntProp.Kripke.instComplete {α : Type u} {Λ : LO.IntProp.Hilbert α} [Λ.IncludeEFQ] [Nonempty (LO.IntProp.SCT Λ)] [DecidableEq α] [Encodable α] {𝔽 : LO.Kripke.FrameClass} (H : LO.IntProp.Kripke.CanonicalFrame Λ ∈ 𝔽) : LO.Complete Λ 𝔽#α

Equations

• ⋯ = ⋯

instance LO.IntProp.Kripke.Int_complete {α : Type u} [DecidableEq α] [Encodable α] : LO.Complete 𝐈𝐧𝐭 LO.Kripke.ReflexiveTransitiveFrameClass#α

Equations

• ⋯ = ⋯

instance LO.IntProp.Kripke.LC_complete {α : Type u} [DecidableEq α] [Encodable α] : LO.Complete 𝐋𝐂 LO.Kripke.ReflexiveTransitiveConnectedFrameClass#α

Equations

• ⋯ = ⋯

instance LO.IntProp.Kripke.KC_complete {α : Type u} [DecidableEq α] [Encodable α] : LO.Complete 𝐊𝐂 LO.Kripke.ReflexiveTransitiveConfluentFrameClass#α

Equations

• ⋯ = ⋯