def LO.Propositional.Kripke.canonicalFrame {S : Type u_1} [Entailment S (Formula ℕ)] (𝓢 : S) [Entailment.Consistent 𝓢] [Entailment.Int 𝓢] : Frame

Equations

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

theorem LO.Propositional.Kripke.canonicalFrame.rel₁ {S : Type u_1} [Entailment S (Formula ℕ)] {𝓢 : S} [Entailment.Consistent 𝓢] [Entailment.Int 𝓢] {x y : (canonicalFrame 𝓢).World} : x ≺ y ↔ (↑x).1 ⊆ (↑y).1

theorem LO.Propositional.Kripke.canonicalFrame.rel₂ {S : Type u_1} [Entailment S (Formula ℕ)] {𝓢 : S} [Entailment.Consistent 𝓢] [Entailment.Int 𝓢] {x y : (canonicalFrame 𝓢).World} : x ≺ y ↔ (↑y).2 ⊆ (↑x).2

def LO.Propositional.Kripke.canonicalModel {S : Type u_1} [Entailment S (Formula ℕ)] (𝓢 : S) [Entailment.Consistent 𝓢] [Entailment.Int 𝓢] : Model

Equations

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

theorem LO.Propositional.Kripke.truthlemma {S : Type u_1} [Entailment S (Formula ℕ)] {𝓢 : S} [Entailment.Consistent 𝓢] [Entailment.Int 𝓢] {φ : Formula ℕ} {t : (canonicalModel 𝓢).World} : t ⊧ φ ↔ φ ∈ (↑t).1

theorem LO.Propositional.Kripke.iff_valid_on_canonicalModel_deducible {S : Type u_1} [Entailment S (Formula ℕ)] {𝓢 : S} [Entailment.Consistent 𝓢] [Entailment.Int 𝓢] {φ : Formula ℕ} : canonicalModel 𝓢 ⊧ φ ↔ 𝓢 ⊢ φ

class LO.Propositional.Kripke.Canonical {S : Type u_1} [Entailment S (Formula ℕ)] (𝓢 : S) [Entailment.Consistent 𝓢] [Entailment.Int 𝓢] (C : FrameClass) : Prop

• canonical : canonicalFrame 𝓢 ∈ C

instance LO.Propositional.Kripke.instCompleteOfCanonical {S : Type u_1} [Entailment S (Formula ℕ)] {𝓢 : S} [Entailment.Consistent 𝓢] [Entailment.Int 𝓢] {C : FrameClass} [Canonical 𝓢 C] : Complete 𝓢 C