structure LO.IntProp.Kripke.Frame : Type 1

• World : Type
• Rel : Rel self.World self.World
• world_nonempty : Nonempty self.World
• rel_po : IsPartialOrder self.World self.Rel

instance LO.IntProp.Kripke.instCoeSortFrameType : CoeSort LO.IntProp.Kripke.Frame Type

Equations

• LO.IntProp.Kripke.instCoeSortFrameType = { coe := LO.IntProp.Kripke.Frame.World }

instance LO.IntProp.Kripke.instCoeFunFrameForallWorldForallProp : CoeFun LO.IntProp.Kripke.Frame fun (F : LO.IntProp.Kripke.Frame) => F.World → F.World → Prop

Equations

• LO.IntProp.Kripke.instCoeFunFrameForallWorldForallProp = { coe := LO.IntProp.Kripke.Frame.Rel }

instance LO.IntProp.Kripke.instNonemptyWorld {F : LO.IntProp.Kripke.Frame} : Nonempty F.World

Equations

• ⋯ = ⋯

instance LO.IntProp.Kripke.instIsPartialOrderWorldRel {F : LO.IntProp.Kripke.Frame} : IsPartialOrder F.World F.Rel

Equations

• ⋯ = ⋯

@[reducible, inline]

abbrev LO.IntProp.Kripke.Frame.Rel' {F : LO.IntProp.Kripke.Frame} (x y : F.World) : Prop

Equations

• (x ≺ y) = F.Rel x y

def LO.IntProp.Kripke.«term_≺_» : Lean.TrailingParserDescr

Equations

• LO.IntProp.Kripke.«term_≺_» = Lean.ParserDescr.trailingNode `LO.IntProp.Kripke.«term_≺_» 45 46 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ≺ ") (Lean.ParserDescr.cat `term 46))

theorem LO.IntProp.Kripke.Frame.rel_trans {F : LO.IntProp.Kripke.Frame} {x y z : F.World} : x ≺ y → y ≺ z → x ≺ z

theorem LO.IntProp.Kripke.Frame.rel_trans' {F : LO.IntProp.Kripke.Frame} : Transitive F.Rel

@[simp]

theorem LO.IntProp.Kripke.Frame.rel_refl {F : LO.IntProp.Kripke.Frame} {x : F.World} : x ≺ x

theorem LO.IntProp.Kripke.Frame.rel_refl' {F : LO.IntProp.Kripke.Frame} : Reflexive F.Rel

@[simp]

theorem LO.IntProp.Kripke.Frame.rel_antisymm {F : LO.IntProp.Kripke.Frame} {x y : F.World} : x ≺ y → y ≺ x → x = y

theorem LO.IntProp.Kripke.Frame.rel_antisymm' {F : LO.IntProp.Kripke.Frame} : Antisymmetric F.Rel

@[reducible, inline]

abbrev LO.IntProp.Kripke.pointFrame : LO.IntProp.Kripke.Frame

Equations

• LO.IntProp.Kripke.pointFrame = LO.IntProp.Kripke.Frame.mk Unit fun (x x : Unit) => True

@[reducible, inline]

abbrev LO.IntProp.Kripke.FrameClass : Type 1

Equations

• LO.IntProp.Kripke.FrameClass = Set LO.IntProp.Kripke.Frame

@[reducible, inline]

abbrev LO.IntProp.Kripke.AllFrameClass : LO.IntProp.Kripke.FrameClass

Equations

• LO.IntProp.Kripke.AllFrameClass = Set.univ

@[reducible, inline]

abbrev LO.IntProp.Kripke.SymmetricFrameClass : LO.IntProp.Kripke.FrameClass

Equations

• LO.IntProp.Kripke.SymmetricFrameClass = {F : LO.IntProp.Kripke.Frame | Symmetric F.Rel}

@[reducible, inline]

abbrev LO.IntProp.Kripke.ConfluentFrameClass : LO.IntProp.Kripke.FrameClass

Equations

• LO.IntProp.Kripke.ConfluentFrameClass = {F : LO.IntProp.Kripke.Frame | Confluent F.Rel}

@[reducible, inline]

abbrev LO.IntProp.Kripke.ConnectedFrameClass : LO.IntProp.Kripke.FrameClass

Equations

• LO.IntProp.Kripke.ConnectedFrameClass = {F : LO.IntProp.Kripke.Frame | Connected F.Rel}

@[reducible, inline]

abbrev LO.IntProp.Kripke.EuclideanFrameClass : LO.IntProp.Kripke.FrameClass

Equations

• LO.IntProp.Kripke.EuclideanFrameClass = {F : LO.IntProp.Kripke.Frame | Euclidean F.Rel}

structure LO.IntProp.Kripke.Valuation (F : LO.IntProp.Kripke.Frame) : Type

• Val : F.World → ℕ → Prop
• hereditary : ∀ {w₁ w₂ : F.World}, w₁ ≺ w₂ → ∀ {a : ℕ}, self.Val w₁ a → self.Val w₂ a

instance LO.IntProp.Kripke.instCoeFunValuationForallWorldForallNatProp {F : LO.IntProp.Kripke.Frame} : CoeFun (LO.IntProp.Kripke.Valuation F) fun (x : LO.IntProp.Kripke.Valuation F) => F.World → ℕ → Prop

Equations

• LO.IntProp.Kripke.instCoeFunValuationForallWorldForallNatProp = { coe := LO.IntProp.Kripke.Valuation.Val }

structure LO.IntProp.Kripke.Modelextends LO.IntProp.Kripke.Frame : Type 1

• World : Type
• Rel : Rel self.World self.World
• world_nonempty : Nonempty self.World
• rel_po : IsPartialOrder self.World self.Rel
• Val : LO.IntProp.Kripke.Valuation self.toFrame

instance LO.IntProp.Kripke.instCoeFunModelForallWorldForallNatProp : CoeFun LO.IntProp.Kripke.Model fun (M : LO.IntProp.Kripke.Model) => M.World → ℕ → Prop

Equations

• LO.IntProp.Kripke.instCoeFunModelForallWorldForallNatProp = { coe := fun (m : LO.IntProp.Kripke.Model) => m.Val.Val }

def LO.IntProp.Formula.Kripke.Satisfies (M : LO.IntProp.Kripke.Model) (w : M.World) : LO.IntProp.Formula ℕ → Prop

Equations

• LO.IntProp.Formula.Kripke.Satisfies M w (LO.IntProp.Formula.atom a) = M.Val.Val w a
• LO.IntProp.Formula.Kripke.Satisfies M w LO.IntProp.Formula.verum = True
• LO.IntProp.Formula.Kripke.Satisfies M w LO.IntProp.Formula.falsum = False
• LO.IntProp.Formula.Kripke.Satisfies M w (φ.and ψ) = (LO.IntProp.Formula.Kripke.Satisfies M w φ ∧ LO.IntProp.Formula.Kripke.Satisfies M w ψ)
• LO.IntProp.Formula.Kripke.Satisfies M w (φ.or ψ) = (LO.IntProp.Formula.Kripke.Satisfies M w φ ∨ LO.IntProp.Formula.Kripke.Satisfies M w ψ)
• LO.IntProp.Formula.Kripke.Satisfies M w φ.neg = ∀ {w' : M.World}, w ≺ w' → ¬LO.IntProp.Formula.Kripke.Satisfies M w' φ
• LO.IntProp.Formula.Kripke.Satisfies M w (φ.imp ψ) = ∀ {w' : M.World}, w ≺ w' → LO.IntProp.Formula.Kripke.Satisfies M w' φ → LO.IntProp.Formula.Kripke.Satisfies M w' ψ

instance LO.IntProp.Formula.Kripke.Satisfies.semantics (M : LO.IntProp.Kripke.Model) : LO.Semantics (LO.IntProp.Formula ℕ) M.World

Equations

• LO.IntProp.Formula.Kripke.Satisfies.semantics M = { Realize := fun (w : M.World) => LO.IntProp.Formula.Kripke.Satisfies M w }

@[simp]

theorem LO.IntProp.Formula.Kripke.Satisfies.iff_models {M : LO.IntProp.Kripke.Model} {w : M.World} {φ : LO.IntProp.Formula ℕ} : w ⊧ φ ↔ LO.IntProp.Formula.Kripke.Satisfies M w φ

@[simp]

theorem LO.IntProp.Formula.Kripke.Satisfies.atom_def {M : LO.IntProp.Kripke.Model} {w : M.World} {a : ℕ} : w ⊧ LO.IntProp.Formula.atom a ↔ M.Val.Val w a

@[simp]

theorem LO.IntProp.Formula.Kripke.Satisfies.top_def {M : LO.IntProp.Kripke.Model} {w : M.World} : w ⊧ ⊤ ↔ True

@[simp]

theorem LO.IntProp.Formula.Kripke.Satisfies.bot_def {M : LO.IntProp.Kripke.Model} {w : M.World} : w ⊧ ⊥ ↔ False

@[simp]

theorem LO.IntProp.Formula.Kripke.Satisfies.and_def {M : LO.IntProp.Kripke.Model} {w : M.World} {φ ψ : LO.IntProp.Formula ℕ} : w ⊧ φ ⋏ ψ ↔ w ⊧ φ ∧ w ⊧ ψ

@[simp]

theorem LO.IntProp.Formula.Kripke.Satisfies.or_def {M : LO.IntProp.Kripke.Model} {w : M.World} {φ ψ : LO.IntProp.Formula ℕ} : w ⊧ φ ⋎ ψ ↔ w ⊧ φ ∨ w ⊧ ψ

@[simp]

theorem LO.IntProp.Formula.Kripke.Satisfies.imp_def {M : LO.IntProp.Kripke.Model} {w : M.World} {φ ψ : LO.IntProp.Formula ℕ} : w ⊧ φ ➝ ψ ↔ ∀ {w' : M.World}, w ≺ w' → w' ⊧ φ → w' ⊧ ψ

@[simp]

theorem LO.IntProp.Formula.Kripke.Satisfies.neg_def {M : LO.IntProp.Kripke.Model} {w : M.World} {φ : LO.IntProp.Formula ℕ} : w ⊧ ∼φ ↔ ∀ {w' : M.World}, w ≺ w' → ¬w' ⊧ φ

instance LO.IntProp.Formula.Kripke.Satisfies.instTopWorldNat {M : LO.IntProp.Kripke.Model} : LO.Semantics.Top M.World

Equations

• ⋯ = ⋯

instance LO.IntProp.Formula.Kripke.Satisfies.instBotWorldNat {M : LO.IntProp.Kripke.Model} : LO.Semantics.Bot M.World

Equations

• ⋯ = ⋯

instance LO.IntProp.Formula.Kripke.Satisfies.instAndWorldNat {M : LO.IntProp.Kripke.Model} : LO.Semantics.And M.World

Equations

• ⋯ = ⋯

instance LO.IntProp.Formula.Kripke.Satisfies.instOrWorldNat {M : LO.IntProp.Kripke.Model} : LO.Semantics.Or M.World

Equations

• ⋯ = ⋯

theorem LO.IntProp.Formula.Kripke.Satisfies.formula_hereditary {M : LO.IntProp.Kripke.Model} {w w' : M.World} {φ : LO.IntProp.Formula ℕ} (hw : w ≺ w') : w ⊧ φ → w' ⊧ φ

theorem LO.IntProp.Formula.Kripke.Satisfies.neg_equiv {M : LO.IntProp.Kripke.Model} {w : M.World} {φ : LO.IntProp.Formula ℕ} : w ⊧ ∼φ ↔ w ⊧ φ ➝ ⊥

def LO.IntProp.Formula.Kripke.ValidOnModel (M : LO.IntProp.Kripke.Model) (φ : LO.IntProp.Formula ℕ) : Prop

Equations

• LO.IntProp.Formula.Kripke.ValidOnModel M φ = ∀ (w : M.World), w ⊧ φ

instance LO.IntProp.Formula.Kripke.ValidOnModel.semantics : LO.Semantics (LO.IntProp.Formula ℕ) LO.IntProp.Kripke.Model

Equations

• LO.IntProp.Formula.Kripke.ValidOnModel.semantics = { Realize := fun (M : LO.IntProp.Kripke.Model) => LO.IntProp.Formula.Kripke.ValidOnModel M }

@[simp]

theorem LO.IntProp.Formula.Kripke.ValidOnModel.iff_models {M : LO.IntProp.Kripke.Model} {φ : LO.IntProp.Formula ℕ} : M ⊧ φ ↔ LO.IntProp.Formula.Kripke.ValidOnModel M φ

theorem LO.IntProp.Formula.Kripke.ValidOnModel.verum {M : LO.IntProp.Kripke.Model} : M ⊧ ⊤

theorem LO.IntProp.Formula.Kripke.ValidOnModel.andElim₁ {M : LO.IntProp.Kripke.Model} {φ ψ : LO.IntProp.Formula ℕ} : M ⊧ φ ⋏ ψ ➝ φ

theorem LO.IntProp.Formula.Kripke.ValidOnModel.andElim₂ {M : LO.IntProp.Kripke.Model} {φ ψ : LO.IntProp.Formula ℕ} : M ⊧ φ ⋏ ψ ➝ ψ

theorem LO.IntProp.Formula.Kripke.ValidOnModel.andInst₃ {M : LO.IntProp.Kripke.Model} {φ ψ : LO.IntProp.Formula ℕ} : M ⊧ φ ➝ ψ ➝ φ ⋏ ψ

theorem LO.IntProp.Formula.Kripke.ValidOnModel.orInst₁ {M : LO.IntProp.Kripke.Model} {φ ψ : LO.IntProp.Formula ℕ} : M ⊧ φ ➝ φ ⋎ ψ

theorem LO.IntProp.Formula.Kripke.ValidOnModel.orInst₂ {M : LO.IntProp.Kripke.Model} {φ ψ : LO.IntProp.Formula ℕ} : M ⊧ ψ ➝ φ ⋎ ψ

theorem LO.IntProp.Formula.Kripke.ValidOnModel.orElim {M : LO.IntProp.Kripke.Model} {φ ψ χ : LO.IntProp.Formula ℕ} : M ⊧ (φ ➝ χ) ➝ (ψ ➝ χ) ➝ φ ⋎ ψ ➝ χ

theorem LO.IntProp.Formula.Kripke.ValidOnModel.imply₁ {M : LO.IntProp.Kripke.Model} {φ ψ : LO.IntProp.Formula ℕ} : M ⊧ φ ➝ ψ ➝ φ

theorem LO.IntProp.Formula.Kripke.ValidOnModel.imply₂ {M : LO.IntProp.Kripke.Model} {φ ψ χ : LO.IntProp.Formula ℕ} : M ⊧ (φ ➝ ψ ➝ χ) ➝ (φ ➝ ψ) ➝ φ ➝ χ

theorem LO.IntProp.Formula.Kripke.ValidOnModel.mdp {M : LO.IntProp.Kripke.Model} {φ ψ : LO.IntProp.Formula ℕ} (hpq : M ⊧ φ ➝ ψ) (hp : M ⊧ φ) : M ⊧ ψ

theorem LO.IntProp.Formula.Kripke.ValidOnModel.bot {M : LO.IntProp.Kripke.Model} : ¬M ⊧ ⊥

instance LO.IntProp.Formula.Kripke.ValidOnModel.instBotModelNat : LO.Semantics.Bot LO.IntProp.Kripke.Model

Equations

• LO.IntProp.Formula.Kripke.ValidOnModel.instBotModelNat = ⋯

theorem LO.IntProp.Formula.Kripke.ValidOnModel.efq {M : LO.IntProp.Kripke.Model} {φ : LO.IntProp.Formula ℕ} : M ⊧ LO.Axioms.EFQ φ

theorem LO.IntProp.Formula.Kripke.ValidOnModel.neg_equiv {M : LO.IntProp.Kripke.Model} {φ : LO.IntProp.Formula ℕ} : M ⊧ LO.Axioms.NegEquiv φ

theorem LO.IntProp.Formula.Kripke.ValidOnModel.lem {M : LO.IntProp.Kripke.Model} {φ : LO.IntProp.Formula ℕ} : Symmetric M.Rel → M ⊧ LO.Axioms.LEM φ

theorem LO.IntProp.Formula.Kripke.ValidOnModel.dum {M : LO.IntProp.Kripke.Model} {φ ψ : LO.IntProp.Formula ℕ} : Connected M.Rel → M ⊧ LO.Axioms.Dummett φ ψ

theorem LO.IntProp.Formula.Kripke.ValidOnModel.wlem {M : LO.IntProp.Kripke.Model} {φ : LO.IntProp.Formula ℕ} : Confluent M.Rel → M ⊧ LO.Axioms.WeakLEM φ

def LO.IntProp.Formula.Kripke.ValidOnFrame (F : LO.IntProp.Kripke.Frame) (φ : LO.IntProp.Formula ℕ) : Prop

Equations

• LO.IntProp.Formula.Kripke.ValidOnFrame F φ = ∀ {V : LO.IntProp.Kripke.Valuation F}, { toFrame := F, Val := V } ⊧ φ

instance LO.IntProp.Formula.Kripke.ValidOnFrame.semantics : LO.Semantics (LO.IntProp.Formula ℕ) LO.IntProp.Kripke.Frame

Equations

• LO.IntProp.Formula.Kripke.ValidOnFrame.semantics = { Realize := fun (F : LO.IntProp.Kripke.Frame) => LO.IntProp.Formula.Kripke.ValidOnFrame F }

@[simp]

theorem LO.IntProp.Formula.Kripke.ValidOnFrame.models_iff {F : LO.IntProp.Kripke.Frame} {φ : LO.IntProp.Formula ℕ} : F ⊧ φ ↔ LO.IntProp.Formula.Kripke.ValidOnFrame F φ

theorem LO.IntProp.Formula.Kripke.ValidOnFrame.verum {F : LO.IntProp.Kripke.Frame} : F ⊧ ⊤

theorem LO.IntProp.Formula.Kripke.ValidOnFrame.andElim₁ {F : LO.IntProp.Kripke.Frame} {φ ψ : LO.IntProp.Formula ℕ} : F ⊧ φ ⋏ ψ ➝ φ

theorem LO.IntProp.Formula.Kripke.ValidOnFrame.andElim₂ {F : LO.IntProp.Kripke.Frame} {φ ψ : LO.IntProp.Formula ℕ} : F ⊧ φ ⋏ ψ ➝ ψ

theorem LO.IntProp.Formula.Kripke.ValidOnFrame.andInst₃ {F : LO.IntProp.Kripke.Frame} {φ ψ : LO.IntProp.Formula ℕ} : F ⊧ φ ➝ ψ ➝ φ ⋏ ψ

theorem LO.IntProp.Formula.Kripke.ValidOnFrame.orInst₁ {F : LO.IntProp.Kripke.Frame} {φ ψ : LO.IntProp.Formula ℕ} : F ⊧ φ ➝ φ ⋎ ψ

theorem LO.IntProp.Formula.Kripke.ValidOnFrame.orInst₂ {F : LO.IntProp.Kripke.Frame} {φ ψ : LO.IntProp.Formula ℕ} : F ⊧ ψ ➝ φ ⋎ ψ

theorem LO.IntProp.Formula.Kripke.ValidOnFrame.orElim {F : LO.IntProp.Kripke.Frame} {φ ψ χ : LO.IntProp.Formula ℕ} : F ⊧ (φ ➝ χ) ➝ (ψ ➝ χ) ➝ φ ⋎ ψ ➝ χ

theorem LO.IntProp.Formula.Kripke.ValidOnFrame.imply₁ {F : LO.IntProp.Kripke.Frame} {φ ψ : LO.IntProp.Formula ℕ} : F ⊧ φ ➝ ψ ➝ φ

theorem LO.IntProp.Formula.Kripke.ValidOnFrame.imply₂ {F : LO.IntProp.Kripke.Frame} {φ ψ χ : LO.IntProp.Formula ℕ} : F ⊧ (φ ➝ ψ ➝ χ) ➝ (φ ➝ ψ) ➝ φ ➝ χ

theorem LO.IntProp.Formula.Kripke.ValidOnFrame.mdp {F : LO.IntProp.Kripke.Frame} {φ ψ : LO.IntProp.Formula ℕ} (hpq : F ⊧ φ ➝ ψ) (hp : F ⊧ φ) : F ⊧ ψ

theorem LO.IntProp.Formula.Kripke.ValidOnFrame.efq {F : LO.IntProp.Kripke.Frame} {φ : LO.IntProp.Formula ℕ} : F ⊧ LO.Axioms.EFQ φ

theorem LO.IntProp.Formula.Kripke.ValidOnFrame.neg_equiv {F : LO.IntProp.Kripke.Frame} {φ : LO.IntProp.Formula ℕ} : F ⊧ LO.Axioms.NegEquiv φ

theorem LO.IntProp.Formula.Kripke.ValidOnFrame.lem {F : LO.IntProp.Kripke.Frame} {φ : LO.IntProp.Formula ℕ} (F_symm : Symmetric F.Rel) : F ⊧ LO.Axioms.LEM φ

theorem LO.IntProp.Formula.Kripke.ValidOnFrame.dum {F : LO.IntProp.Kripke.Frame} {φ ψ : LO.IntProp.Formula ℕ} (F_conn : Connected F.Rel) : F ⊧ LO.Axioms.Dummett φ ψ

theorem LO.IntProp.Formula.Kripke.ValidOnFrame.wlem {F : LO.IntProp.Kripke.Frame} {φ : LO.IntProp.Formula ℕ} (F_conf : Confluent F.Rel) : F ⊧ LO.Axioms.WeakLEM φ

theorem LO.IntProp.Formula.Kripke.ValidOnFrame.top {F : LO.IntProp.Kripke.Frame} : F ⊧ ⊤

instance LO.IntProp.Formula.Kripke.ValidOnFrame.instTopFrameNat : LO.Semantics.Top LO.IntProp.Kripke.Frame

Equations

• LO.IntProp.Formula.Kripke.ValidOnFrame.instTopFrameNat = ⋯

theorem LO.IntProp.Formula.Kripke.ValidOnFrame.bot {F : LO.IntProp.Kripke.Frame} : ¬F ⊧ ⊥

instance LO.IntProp.Formula.Kripke.ValidOnFrame.instBotFrameNat : LO.Semantics.Bot LO.IntProp.Kripke.Frame

Equations

• LO.IntProp.Formula.Kripke.ValidOnFrame.instBotFrameNat = ⋯

def LO.IntProp.Formula.Kripke.ValidOnFrameClass (C : LO.IntProp.Kripke.FrameClass) (φ : LO.IntProp.Formula ℕ) : Prop

Equations

• LO.IntProp.Formula.Kripke.ValidOnFrameClass C φ = ∀ F ∈ C, F ⊧ φ

instance LO.IntProp.Formula.Kripke.ValidOnFrameClass.semantics : LO.Semantics (LO.IntProp.Formula ℕ) LO.IntProp.Kripke.FrameClass

Equations

• LO.IntProp.Formula.Kripke.ValidOnFrameClass.semantics = { Realize := fun (C : LO.IntProp.Kripke.FrameClass) => LO.IntProp.Formula.Kripke.ValidOnFrameClass C }

@[simp]

theorem LO.IntProp.Formula.Kripke.ValidOnFrameClass.models_iff {C : LO.IntProp.Kripke.FrameClass} {φ : LO.IntProp.Formula ℕ} : C ⊧ φ ↔ LO.IntProp.Formula.Kripke.ValidOnFrameClass C φ

theorem LO.IntProp.Formula.Kripke.ValidOnFrameClass.bot {C : LO.IntProp.Kripke.FrameClass} (h_nonempty : Set.Nonempty C) : ¬C ⊧ ⊥

def LO.IntProp.Kripke.Frame.theorems (F : LO.IntProp.Kripke.Frame) : Set (LO.IntProp.Formula ℕ)

A set of formula that valid on frame F.

Equations

• F.theorems = {φ : LO.IntProp.Formula ℕ | F ⊧ φ}

def LO.IntProp.Kripke.FrameClass.DefinedBy (C : LO.IntProp.Kripke.FrameClass) (T : Set (LO.IntProp.Formula ℕ)) : Prop

Equations

• C.DefinedBy T = ∀ (F : LO.IntProp.Kripke.Frame), F ∈ C ↔ F ⊧* T

theorem LO.IntProp.Hilbert.Kripke.sound_hilbert_of_frameclass {φ : LO.IntProp.Formula ℕ} {C : LO.IntProp.Kripke.FrameClass} {T : Set (LO.IntProp.Formula ℕ)} (definedBy : C.DefinedBy T) : { axioms := 𝗘𝗙𝗤 ∪ T } ⊢! φ → C ⊧ φ

theorem LO.IntProp.Hilbert.Kripke.sound_of_equiv_frameclass_hilbert {H : LO.IntProp.Hilbert ℕ} {φ : LO.IntProp.Formula ℕ} {C : LO.IntProp.Kripke.FrameClass} {T : Set (LO.IntProp.Formula ℕ)} (definedBy : C.DefinedBy T) (heq : { axioms := 𝗘𝗙𝗤 ∪ T } =ₛ H) : H ⊢! φ → C ⊧ φ

instance LO.IntProp.Hilbert.Kripke.instSound {H : LO.IntProp.Hilbert ℕ} {C : LO.IntProp.Kripke.FrameClass} {T : Set (LO.IntProp.Formula ℕ)} (definedBy : C.DefinedBy T) (heq : { axioms := 𝗘𝗙𝗤 ∪ T } =ₛ H) : LO.Sound H C

Equations

• ⋯ = ⋯

theorem LO.IntProp.Hilbert.Kripke.unprovable_bot {H : LO.IntProp.Hilbert ℕ} {C : LO.IntProp.Kripke.FrameClass} [sound : LO.Sound H C] (hNonempty : Set.Nonempty C) : H ⊬ ⊥

theorem LO.IntProp.Hilbert.Kripke.consistent {H : LO.IntProp.Hilbert ℕ} {C : LO.IntProp.Kripke.FrameClass} [LO.Sound H C] (h_nonempty : Set.Nonempty C) : H.Consistent

instance LO.IntProp.Hilbert.Int.Kripke.sound : LO.Sound (LO.IntProp.Hilbert.Int ℕ) LO.IntProp.Kripke.AllFrameClass

Equations

• LO.IntProp.Hilbert.Int.Kripke.sound = ⋯

instance LO.IntProp.Hilbert.Int.instConsistentNat : (LO.IntProp.Hilbert.Int ℕ).Consistent

Equations

• LO.IntProp.Hilbert.Int.instConsistentNat = ⋯

instance LO.IntProp.Hilbert.KC.Kripke.sound : LO.Sound (LO.IntProp.Hilbert.KC ℕ) LO.IntProp.Kripke.ConfluentFrameClass

Equations

• LO.IntProp.Hilbert.KC.Kripke.sound = ⋯

instance LO.IntProp.Hilbert.KC.instConsistentNat : (LO.IntProp.Hilbert.KC ℕ).Consistent

Equations

• LO.IntProp.Hilbert.KC.instConsistentNat = ⋯

instance LO.IntProp.Hilbert.LC.Kripke.sound : LO.Sound (LO.IntProp.Hilbert.LC ℕ) LO.IntProp.Kripke.ConnectedFrameClass

Equations

• LO.IntProp.Hilbert.LC.Kripke.sound = ⋯

instance LO.IntProp.Hilbert.LC.instConsistentNat : (LO.IntProp.Hilbert.LC ℕ).Consistent

Equations

• LO.IntProp.Hilbert.LC.instConsistentNat = ⋯

instance LO.IntProp.Hilbert.Cl.Kripke.sound : LO.Sound (LO.IntProp.Hilbert.Cl ℕ) LO.IntProp.Kripke.EuclideanFrameClass

Equations

• LO.IntProp.Hilbert.Cl.Kripke.sound = ⋯

instance LO.IntProp.Hilbert.Cl.instConsistentNat : (LO.IntProp.Hilbert.Cl ℕ).Consistent

Equations

• LO.IntProp.Hilbert.Cl.instConsistentNat = ⋯