FiniteFrame

structure LO.Modal.Kripke.FiniteFrameextends LO.Modal.Kripke.Frame : Type 1

Imported declaration from the Incompleteness formalization.

• World : Type
• Rel : _root_.Rel self.World self.World
• world_nonempty : Nonempty self.World
• world_finite : Finite self.World

instance LO.Modal.Kripke.instFiniteWorld {F : FiniteFrame} : Finite F.World

def LO.Modal.Kripke.Frame.toFinite (F : Frame) [Finite F.World] : FiniteFrame

Imported declaration from the Incompleteness formalization.

Equations

• F.toFinite = { toFrame := F, world_finite := inst✝ }

@[reducible, inline]

abbrev LO.Modal.Kripke.FiniteFrameClass : Type 1

Imported declaration from the Incompleteness formalization.

Equations

• LO.Modal.Kripke.FiniteFrameClass = Set LO.Modal.Kripke.FiniteFrame

def LO.Modal.Kripke.FrameClass.restrictFinite (C : FrameClass) : FiniteFrameClass

Imported declaration from the Incompleteness formalization.

Equations

• C.restrictFinite = {F : LO.Modal.Kripke.FiniteFrame | F.toFrame ∈ C}

def LO.Modal.Kripke.FiniteFrameClass.toFrameClass (C : FiniteFrameClass) : FrameClass

Imported declaration from the Incompleteness formalization.

Equations

• C.toFrameClass = (fun (x : LO.Modal.Kripke.FiniteFrame) => x.toFrame) '' C

@[implicit_reducible]

instance LO.Modal.Kripke.instCoeFiniteFrameClassFrameClass : Coe FiniteFrameClass FrameClass

Equations

• LO.Modal.Kripke.instCoeFiniteFrameClassFrameClass = { coe := LO.Modal.Kripke.FiniteFrameClass.toFrameClass }

@[reducible, inline]

abbrev LO.Modal.Kripke.reflexivePointFrame : FiniteFrame

Imported declaration from the Incompleteness formalization.

Equations

• LO.Modal.Kripke.reflexivePointFrame = { World := Unit, Rel := fun (x x_1 : Unit) => True, world_nonempty := ⋯, world_finite := ⋯ }

@[reducible, inline]

abbrev LO.Modal.Kripke.irreflexivePointFrame : FiniteFrame

Imported declaration from the Incompleteness formalization.

Equations

• LO.Modal.Kripke.irreflexivePointFrame = { World := Unit, Rel := fun (x x_1 : Unit) => False, world_nonempty := ⋯, world_finite := ⋯ }

def LO.Modal.Formula.Kripke.ValidOnFiniteFrame (F : Kripke.FiniteFrame) (φ : Formula ℕ) : Prop

Imported declaration from the Incompleteness formalization.

Equations

• LO.Modal.Formula.Kripke.ValidOnFiniteFrame F φ = (F.toFrame ⊧ φ)

@[implicit_reducible]

instance LO.Modal.Formula.Kripke.ValidOnFiniteFrame.semantics : Semantics (Formula ℕ) Kripke.FiniteFrame

Equations

• LO.Modal.Formula.Kripke.ValidOnFiniteFrame.semantics = { Realize := fun (F : LO.Modal.Kripke.FiniteFrame) => LO.Modal.Formula.Kripke.ValidOnFiniteFrame F }

@[simp]

theorem LO.Modal.Formula.Kripke.ValidOnFiniteFrame.models_iff {F : Kripke.FiniteFrame} {φ : Formula ℕ} : F ⊧ φ ↔ ValidOnFiniteFrame F φ

theorem LO.Modal.Formula.Kripke.ValidOnFiniteFrame.models_set_iff {F : Kripke.FiniteFrame} {Φ : Set (Formula ℕ)} : F ⊧* Φ ↔ ∀ φ ∈ Φ, F ⊧ φ

theorem LO.Modal.Formula.Kripke.ValidOnFiniteFrame.top_def {F : Kripke.FiniteFrame} : F ⊧ ⊤

theorem LO.Modal.Formula.Kripke.ValidOnFiniteFrame.bot_def {F : Kripke.FiniteFrame} : ¬F ⊧ ⊥

instance LO.Modal.Formula.Kripke.ValidOnFiniteFrame.instTopFiniteFrameNat : Semantics.Top Kripke.FiniteFrame

instance LO.Modal.Formula.Kripke.ValidOnFiniteFrame.instBotFiniteFrameNat : Semantics.Bot Kripke.FiniteFrame

theorem LO.Modal.Formula.Kripke.ValidOnFiniteFrame.iff_not_exists_valuation {F : Kripke.FiniteFrame} {φ : Formula ℕ} : ¬F ⊧ φ ↔ ∃ (V : Kripke.Valuation F.toFrame), ¬{ toFrame := F.toFrame, Val := V } ⊧ φ

theorem LO.Modal.Formula.Kripke.ValidOnFiniteFrame.not_of_exists_valuation {F : Kripke.FiniteFrame} {φ : Formula ℕ} : (∃ (V : Kripke.Valuation F.toFrame), ¬{ toFrame := F.toFrame, Val := V } ⊧ φ) → ¬F ⊧ φ

Alias of the reverse direction of LO.Modal.Formula.Kripke.ValidOnFiniteFrame.iff_not_exists_valuation.

theorem LO.Modal.Formula.Kripke.ValidOnFiniteFrame.exists_valuation_of_not {F : Kripke.FiniteFrame} {φ : Formula ℕ} : ¬F ⊧ φ → ∃ (V : Kripke.Valuation F.toFrame), ¬{ toFrame := F.toFrame, Val := V } ⊧ φ

Alias of the forward direction of LO.Modal.Formula.Kripke.ValidOnFiniteFrame.iff_not_exists_valuation.

theorem LO.Modal.Formula.Kripke.ValidOnFiniteFrame.iff_not_exists_valuation_world {F : Kripke.FiniteFrame} {φ : Formula ℕ} : ¬F ⊧ φ ↔ ∃ (V : Kripke.Valuation F.toFrame) (x : { toFrame := F.toFrame, Val := V }.World), ¬Satisfies { toFrame := F.toFrame, Val := V } x φ

theorem LO.Modal.Formula.Kripke.ValidOnFiniteFrame.not_of_exists_valuation_world {F : Kripke.FiniteFrame} {φ : Formula ℕ} : (∃ (V : Kripke.Valuation F.toFrame) (x : { toFrame := F.toFrame, Val := V }.World), ¬Satisfies { toFrame := F.toFrame, Val := V } x φ) → ¬F ⊧ φ

Alias of the reverse direction of LO.Modal.Formula.Kripke.ValidOnFiniteFrame.iff_not_exists_valuation_world.

theorem LO.Modal.Formula.Kripke.ValidOnFiniteFrame.exists_valuation_world_of_not {F : Kripke.FiniteFrame} {φ : Formula ℕ} : ¬F ⊧ φ → ∃ (V : Kripke.Valuation F.toFrame) (x : { toFrame := F.toFrame, Val := V }.World), ¬Satisfies { toFrame := F.toFrame, Val := V } x φ

Alias of the forward direction of LO.Modal.Formula.Kripke.ValidOnFiniteFrame.iff_not_exists_valuation_world.

def LO.Modal.Formula.Kripke.ValidOnFiniteFrameClass (C : Kripke.FiniteFrameClass) (φ : Formula ℕ) : Prop

Imported declaration from the Incompleteness formalization.

Equations

• LO.Modal.Formula.Kripke.ValidOnFiniteFrameClass C φ = (C.toFrameClass ⊧ φ)

@[implicit_reducible]

instance LO.Modal.Formula.Kripke.ValidOnFiniteFrameClass.semantics : Semantics (Formula ℕ) Kripke.FiniteFrameClass

Equations

• LO.Modal.Formula.Kripke.ValidOnFiniteFrameClass.semantics = { Realize := fun (C : LO.Modal.Kripke.FiniteFrameClass) => LO.Modal.Formula.Kripke.ValidOnFrameClass C.toFrameClass }

@[simp]

theorem LO.Modal.Formula.Kripke.ValidOnFiniteFrameClass.models_iff {C : Kripke.FiniteFrameClass} {φ : Formula ℕ} : C ⊧ φ ↔ ValidOnFrameClass C.toFrameClass φ

theorem LO.Modal.Formula.Kripke.ValidOnFiniteFrameClass.iff_not_exists_frame {C : Kripke.FiniteFrameClass} {φ : Formula ℕ} : ¬C ⊧ φ ↔ ∃ F ∈ C, ¬F ⊧ φ

theorem LO.Modal.Formula.Kripke.ValidOnFiniteFrameClass.exists_frame_of_not {C : Kripke.FiniteFrameClass} {φ : Formula ℕ} : ¬C ⊧ φ → ∃ F ∈ C, ¬F ⊧ φ

Alias of the forward direction of LO.Modal.Formula.Kripke.ValidOnFiniteFrameClass.iff_not_exists_frame.

theorem LO.Modal.Formula.Kripke.ValidOnFiniteFrameClass.not_of_exists_frame {C : Kripke.FiniteFrameClass} {φ : Formula ℕ} : (∃ F ∈ C, ¬F ⊧ φ) → ¬C ⊧ φ

Alias of the reverse direction of LO.Modal.Formula.Kripke.ValidOnFiniteFrameClass.iff_not_exists_frame.

class LO.Modal.Kripke.FiniteFrameClass.DefinedBy (C : FiniteFrameClass) (Γ : Set (Formula ℕ)) : Prop

Imported declaration from the Incompleteness formalization.

• defines (F : FiniteFrame) : F ∈ C ↔ ∀ φ ∈ Γ, F ⊧ φ

class LO.Modal.Kripke.FiniteFrameClass.FiniteDefinedBy (C : FiniteFrameClass) (Γ : Set (Formula ℕ)) extends C.DefinedBy Γ : Prop

Imported declaration from the Incompleteness formalization.

• defines (F : FiniteFrame) : F ∈ C ↔ ∀ φ ∈ Γ, F ⊧ φ
• finite : Γ.Finite

@[reducible, inline]

abbrev LO.Modal.Kripke.FiniteFrameClass.DefinedByFormula (C : FiniteFrameClass) (φ : Formula ℕ) : Prop

Imported declaration from the Incompleteness formalization.

Equations

• C.DefinedByFormula φ = C.DefinedBy {φ}

theorem LO.Modal.Kripke.FiniteFrameClass.definedByFormula_of_iff_mem_validate {C : FiniteFrameClass} {φ : Formula ℕ} (h : ∀ (F : FiniteFrame), F ∈ C ↔ F ⊧ φ) : C.DefinedByFormula φ

instance LO.Modal.Kripke.FiniteFrameClass.definedBy_inter (C₁ : FiniteFrameClass) (Γ₁ : Set (Formula ℕ)) [h₁ : C₁.DefinedBy Γ₁] (C₂ : FiniteFrameClass) (Γ₂ : Set (Formula ℕ)) [h₂ : C₂.DefinedBy Γ₂] : (C₁ ∩ C₂).DefinedBy (Γ₁ ∪ Γ₂)

class LO.Modal.Kripke.FiniteFrameClass.IsNonempty (C : FiniteFrameClass) : Prop

Imported declaration from the Incompleteness formalization.

• nonempty : Nonempty ↑C

@[reducible, inline]

abbrev LO.Modal.Kripke.AllFiniteFrameClass : FiniteFrameClass

Imported declaration from the Incompleteness formalization.

Equations

• LO.Modal.Kripke.AllFiniteFrameClass = Set.univ

instance LO.Modal.Kripke.AllFiniteFrameClass.DefinedBy : AllFiniteFrameClass.DefinedByFormula (Axioms.K (Formula.atom 0) (Formula.atom 1))

instance LO.Modal.Kripke.AllFiniteFrameClass.IsNonempty : AllFiniteFrameClass.IsNonempty

theorem LO.Modal.Kripke.FiniteFrameClass.definedBy_with_axiomK {C : FiniteFrameClass} {Γ : Set (Formula ℕ)} (defines : C.DefinedBy Γ) : C.DefinedBy (insert (Axioms.K (Formula.atom 0) (Formula.atom 1)) Γ)