Basic

structure LO.Modal.Kripke.Frame : Type 1

Imported declaration from the Incompleteness formalization.

• World : Type

  Imported declaration from the Incompleteness formalization.

• Rel : _root_.Rel self.World self.World

  Imported declaration from the Incompleteness formalization.

• world_nonempty : Nonempty self.World

@[implicit_reducible]

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

Equations

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

@[implicit_reducible]

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

Equations

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

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

@[reducible, inline]

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

Imported declaration from the Incompleteness formalization.

Equations

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

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

Imported declaration from the Incompleteness formalization.

Equations

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

@[reducible, inline]

abbrev LO.Modal.Kripke.Frame.RelItr' {F : Frame} (n : ℕ) : F.World → F.World → Prop

Imported declaration from the Incompleteness formalization.

Equations

• LO.Modal.Kripke.Frame.RelItr' n = F.Rel.iterate n

def LO.Modal.Kripke.«term_≺^[_]_» : Lean.TrailingParserDescr

Imported declaration from the Incompleteness formalization.

Equations

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

@[reducible, inline]

abbrev LO.Modal.Kripke.FrameClass : Type 1

Imported declaration from the Incompleteness formalization.

Equations

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

@[reducible, inline]

abbrev LO.Modal.Kripke.FrameClass.nonempty (C : FrameClass) : Prop

Imported declaration from the Incompleteness formalization.

Equations

• C.nonempty = ∃ (F : LO.Modal.Kripke.Frame), F ∈ C

@[reducible, inline]

abbrev LO.Modal.Kripke.Valuation (F : Frame) : Type

Imported declaration from the Incompleteness formalization.

Equations

• LO.Modal.Kripke.Valuation F = (F.World → ℕ → Prop)

structure LO.Modal.Kripke.Modelextends 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
• Val : Valuation self.toFrame

  Imported declaration from the Incompleteness formalization.

@[implicit_reducible]

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

Equations

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

def LO.Modal.Formula.Kripke.Satisfies (M : Kripke.Model) (x : M.World) : Formula ℕ → Prop

Imported declaration from the Incompleteness formalization.

Equations

• LO.Modal.Formula.Kripke.Satisfies M x (LO.Modal.Formula.atom a) = M.Val x a
• LO.Modal.Formula.Kripke.Satisfies M x LO.Modal.Formula.falsum = False
• LO.Modal.Formula.Kripke.Satisfies M x (φ.imp ψ) = LO.Modal.Formula.Kripke.Satisfies M x φ ==> LO.Modal.Formula.Kripke.Satisfies M x ψ
• LO.Modal.Formula.Kripke.Satisfies M x φ.box = ∀ (y : M.World), x ≺ y → LO.Modal.Formula.Kripke.Satisfies M y φ

@[implicit_reducible]

instance LO.Modal.Formula.Kripke.Satisfies.semantics {M : Kripke.Model} : Semantics (Formula ℕ) M.World

Equations

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

@[simp]

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

@[simp]

theorem LO.Modal.Formula.Kripke.Satisfies.atom_def {M : Kripke.Model} {x : M.World} {a : ℕ} : Satisfies M x (atom a) ↔ M.Val x a

theorem LO.Modal.Formula.Kripke.Satisfies.bot_def {M : Kripke.Model} {x : M.World} : ¬x ⊧ ⊥

theorem LO.Modal.Formula.Kripke.Satisfies.imp_def {M : Kripke.Model} {x : M.World} {φ ψ : Formula ℕ} : x ⊧ φ ==> ψ ↔ x ⊧ φ → x ⊧ ψ

theorem LO.Modal.Formula.Kripke.Satisfies.imp_def₂ {M : Kripke.Model} {x : M.World} {φ ψ : Formula ℕ} : x ⊧ φ ==> ψ ↔ ¬x ⊧ φ ∨ x ⊧ ψ

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

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

theorem LO.Modal.Formula.Kripke.Satisfies.not_def {M : Kripke.Model} {x : M.World} {φ : Formula ℕ} : x ⊧ ∼φ ↔ ¬x ⊧ φ

theorem LO.Modal.Formula.Kripke.Satisfies.top_def {M : Kripke.Model} {x : M.World} : x ⊧ ⊤

@[simp]

theorem LO.Modal.Formula.Kripke.Satisfies.box_def {M : Kripke.Model} {x : M.World} {φ : Formula ℕ} : Satisfies M x (□φ) ↔ ∀ (y : M.World), x ≺ y → y ⊧ φ

@[simp]

theorem LO.Modal.Formula.Kripke.Satisfies.dia_def {M : Kripke.Model} {x : M.World} {φ : Formula ℕ} : Satisfies M x (◇φ) ↔ ∃ (y : M.World), x ≺ y ∧ y ⊧ φ

instance LO.Modal.Formula.Kripke.Satisfies.instTarskiWorldNat {M : Kripke.Model} : Semantics.Tarski M.World

theorem LO.Modal.Formula.Kripke.Satisfies.iff_def {M : Kripke.Model} {x : M.World} {φ ψ : Formula ℕ} : x ⊧ φ <=> ψ ↔ (x ⊧ φ ↔ x ⊧ ψ)

@[simp]

theorem LO.Modal.Formula.Kripke.Satisfies.negneg_def {M : Kripke.Model} {x : M.World} {φ : Formula ℕ} : Satisfies M x (∼∼φ) ↔ x ⊧ φ

theorem LO.Modal.Formula.Kripke.Satisfies.multibox_def {M : Kripke.Model} {x : M.World} {φ : Formula ℕ} {n : ℕ} : x ⊧ □^[n]φ ↔ ∀ {y : M.World}, x ≺^[n] y → y ⊧ φ

theorem LO.Modal.Formula.Kripke.Satisfies.multidia_def {M : Kripke.Model} {x : M.World} {φ : Formula ℕ} {n : ℕ} : x ⊧ ◇^[n]φ ↔ ∃ (y : M.World), x ≺^[n] y ∧ y ⊧ φ

theorem LO.Modal.Formula.Kripke.Satisfies.trans {M : Kripke.Model} {x : M.World} {φ ψ χ : Formula ℕ} (hpq : x ⊧ φ ==> ψ) (hqr : x ⊧ ψ ==> χ) : x ⊧ φ ==> χ

theorem LO.Modal.Formula.Kripke.Satisfies.mdp {M : Kripke.Model} {x : M.World} {φ ψ : Formula ℕ} (hpq : x ⊧ φ ==> ψ) (hp : x ⊧ φ) : x ⊧ ψ

theorem LO.Modal.Formula.Kripke.Satisfies.diaDual {M : Kripke.Model} {x : M.World} {φ : Formula ℕ} : x ⊧ ◇φ ↔ x ⊧ ∼□(∼φ)

theorem LO.Modal.Formula.Kripke.Satisfies.box_dual {M : Kripke.Model} {x : M.World} {φ : Formula ℕ} : x ⊧ □φ ↔ x ⊧ ∼◇(∼φ)

theorem LO.Modal.Formula.Kripke.Satisfies.not_imp {M : Kripke.Model} {x : M.World} {φ ψ : Formula ℕ} : ¬x ⊧ φ ==> ψ ↔ x ⊧ φ ⋏ ∼ψ

theorem LO.Modal.Formula.Kripke.Satisfies.iff_subst_self {φ : Formula ℕ} {F : Kripke.Frame} {V : Kripke.Valuation F} {x : F.World} (s : Substitution ℕ) : Satisfies { toFrame := F, Val := fun (w : F.World) (a : ℕ) => Satisfies { toFrame := F, Val := V } w (atom a⟦s⟧) } x φ ↔ Satisfies { toFrame := F, Val := V } x (φ⟦s⟧)

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

Imported declaration from the Incompleteness formalization.

Equations

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

@[implicit_reducible]

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

Equations

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

@[simp]

theorem LO.Modal.Formula.Kripke.ValidOnModel.iff_models {f : Formula ℕ} {M : Kripke.Model} : M ⊧ f ↔ ValidOnModel M f

theorem LO.Modal.Formula.Kripke.ValidOnModel.bot_def {M : Kripke.Model} : ¬M ⊧ ⊥

theorem LO.Modal.Formula.Kripke.ValidOnModel.top_def {M : Kripke.Model} : M ⊧ ⊤

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

instance LO.Modal.Formula.Kripke.ValidOnModel.instTopModelNat : Semantics.Top Kripke.Model

theorem LO.Modal.Formula.Kripke.ValidOnModel.iff_not_exists_world {φ : Formula ℕ} {M : Kripke.Model} : ¬M ⊧ φ ↔ ∃ (x : M.World), ¬x ⊧ φ

theorem LO.Modal.Formula.Kripke.ValidOnModel.not_of_exists_world {φ : Formula ℕ} {M : Kripke.Model} : (∃ (x : M.World), ¬x ⊧ φ) → ¬M ⊧ φ

Alias of the reverse direction of LO.Modal.Formula.Kripke.ValidOnModel.iff_not_exists_world.

theorem LO.Modal.Formula.Kripke.ValidOnModel.exists_world_of_not {φ : Formula ℕ} {M : Kripke.Model} : ¬M ⊧ φ → ∃ (x : M.World), ¬x ⊧ φ

Alias of the forward direction of LO.Modal.Formula.Kripke.ValidOnModel.iff_not_exists_world.

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

theorem LO.Modal.Formula.Kripke.ValidOnModel.nec {M : Kripke.Model} {φ : Formula ℕ} (h : M ⊧ φ) : M ⊧ □φ

theorem LO.Modal.Formula.Kripke.ValidOnModel.imply₁ {M : Kripke.Model} {φ ψ : Formula ℕ} : M ⊧ Axioms.Imply₁ φ ψ

theorem LO.Modal.Formula.Kripke.ValidOnModel.imply₂ {M : Kripke.Model} {φ ψ χ : Formula ℕ} : M ⊧ Axioms.Imply₂ φ ψ χ

theorem LO.Modal.Formula.Kripke.ValidOnModel.elimContra {M : Kripke.Model} {φ ψ : Formula ℕ} : M ⊧ Axioms.ElimContra φ ψ

theorem LO.Modal.Formula.Kripke.ValidOnModel.axiomK {M : Kripke.Model} {φ ψ : Formula ℕ} : M ⊧ Axioms.K φ ψ

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

Imported declaration from the Incompleteness formalization.

Equations

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

@[implicit_reducible]

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

Equations

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

@[simp]

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

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

theorem LO.Modal.Formula.Kripke.ValidOnFrame.top_def {F : Kripke.Frame} : F ⊧ ⊤

theorem LO.Modal.Formula.Kripke.ValidOnFrame.bot_def {F : Kripke.Frame} : ¬F ⊧ ⊥

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

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

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

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

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

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

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

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

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

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

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

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

theorem LO.Modal.Formula.Kripke.ValidOnFrame.iff_not_exists_model_world {F : Kripke.Frame} {φ : Formula ℕ} : ¬F ⊧ φ ↔ ∃ (M : Kripke.Model) (x : M.World), M.toFrame = F ∧ ¬x ⊧ φ

theorem LO.Modal.Formula.Kripke.ValidOnFrame.exists_model_world_of_not {F : Kripke.Frame} {φ : Formula ℕ} : ¬F ⊧ φ → ∃ (M : Kripke.Model) (x : M.World), M.toFrame = F ∧ ¬x ⊧ φ

Alias of the forward direction of LO.Modal.Formula.Kripke.ValidOnFrame.iff_not_exists_model_world.

theorem LO.Modal.Formula.Kripke.ValidOnFrame.not_of_exists_model_world {F : Kripke.Frame} {φ : Formula ℕ} : (∃ (M : Kripke.Model) (x : M.World), M.toFrame = F ∧ ¬x ⊧ φ) → ¬F ⊧ φ

Alias of the reverse direction of LO.Modal.Formula.Kripke.ValidOnFrame.iff_not_exists_model_world.

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

theorem LO.Modal.Formula.Kripke.ValidOnFrame.nec {F : Kripke.Frame} {φ : Formula ℕ} (h : F ⊧ φ) : F ⊧ □φ

theorem LO.Modal.Formula.Kripke.ValidOnFrame.subst {F : Kripke.Frame} {φ : Formula ℕ} {s : Substitution ℕ} (h : F ⊧ φ) : F ⊧ φ⟦s⟧

theorem LO.Modal.Formula.Kripke.ValidOnFrame.imply₁ {F : Kripke.Frame} {φ ψ : Formula ℕ} : F ⊧ Axioms.Imply₁ φ ψ

theorem LO.Modal.Formula.Kripke.ValidOnFrame.imply₂ {F : Kripke.Frame} {φ ψ χ : Formula ℕ} : F ⊧ Axioms.Imply₂ φ ψ χ

theorem LO.Modal.Formula.Kripke.ValidOnFrame.elimContra {F : Kripke.Frame} {φ ψ : Formula ℕ} : F ⊧ Axioms.ElimContra φ ψ

theorem LO.Modal.Formula.Kripke.ValidOnFrame.axiomK {F : Kripke.Frame} {φ ψ : Formula ℕ} : F ⊧ Axioms.K φ ψ

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

Imported declaration from the Incompleteness formalization.

Equations

• LO.Modal.Formula.Kripke.ValidOnFrameClass C φ = ∀ {F : LO.Modal.Kripke.Frame}, F ∈ C → F ⊧ φ

@[implicit_reducible]

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

Equations

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

@[simp]

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

theorem LO.Modal.Formula.Kripke.ValidOnFrameClass.top_def {C : Kripke.FrameClass} : C ⊧ ⊤

instance LO.Modal.Formula.Kripke.ValidOnFrameClass.instTopFrameClassNat : Semantics.Top Kripke.FrameClass

theorem LO.Modal.Formula.Kripke.ValidOnFrameClass.bot_def {C : Kripke.FrameClass} (h : Set.Nonempty C) : ¬C ⊧ ⊥

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

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

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

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

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

theorem LO.Modal.Formula.Kripke.ValidOnFrameClass.iff_not_exists_model {φ : Formula ℕ} {C : Kripke.FrameClass} : ¬C ⊧ φ ↔ ∃ (M : Kripke.Model), M.toFrame ∈ C ∧ ¬M ⊧ φ

theorem LO.Modal.Formula.Kripke.ValidOnFrameClass.exists_model_of_not {φ : Formula ℕ} {C : Kripke.FrameClass} : ¬C ⊧ φ → ∃ (M : Kripke.Model), M.toFrame ∈ C ∧ ¬M ⊧ φ

Alias of the forward direction of LO.Modal.Formula.Kripke.ValidOnFrameClass.iff_not_exists_model.

theorem LO.Modal.Formula.Kripke.ValidOnFrameClass.not_of_exists_model {φ : Formula ℕ} {C : Kripke.FrameClass} : (∃ (M : Kripke.Model), M.toFrame ∈ C ∧ ¬M ⊧ φ) → ¬C ⊧ φ

Alias of the reverse direction of LO.Modal.Formula.Kripke.ValidOnFrameClass.iff_not_exists_model.

theorem LO.Modal.Formula.Kripke.ValidOnFrameClass.iff_not_exists_model_world {φ : Formula ℕ} {C : Kripke.FrameClass} : ¬C ⊧ φ ↔ ∃ (M : Kripke.Model) (x : M.World), M.toFrame ∈ C ∧ ¬x ⊧ φ

theorem LO.Modal.Formula.Kripke.ValidOnFrameClass.exists_model_world_of_not {φ : Formula ℕ} {C : Kripke.FrameClass} : ¬C ⊧ φ → ∃ (M : Kripke.Model) (x : M.World), M.toFrame ∈ C ∧ ¬x ⊧ φ

Alias of the forward direction of LO.Modal.Formula.Kripke.ValidOnFrameClass.iff_not_exists_model_world.

theorem LO.Modal.Formula.Kripke.ValidOnFrameClass.not_of_exists_model_world {φ : Formula ℕ} {C : Kripke.FrameClass} : (∃ (M : Kripke.Model) (x : M.World), M.toFrame ∈ C ∧ ¬x ⊧ φ) → ¬C ⊧ φ

Alias of the reverse direction of LO.Modal.Formula.Kripke.ValidOnFrameClass.iff_not_exists_model_world.

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

Imported declaration from the Incompleteness formalization.

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

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

Imported declaration from the Incompleteness formalization.

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

@[reducible, inline]

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

Imported declaration from the Incompleteness formalization.

Equations

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

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

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

instance LO.Modal.Kripke.FrameClass.definedByFormula_inter (C₁ : FrameClass) (φ₁ : Formula ℕ) [C₁.DefinedByFormula φ₁] (C₂ : FrameClass) (φ₂ : Formula ℕ) [C₂.DefinedByFormula φ₂] : (C₁ ∩ C₂).DefinedBy {φ₁, φ₂}

theorem LO.Modal.Kripke.FrameClass.definedBy_triinter (C₁ : FrameClass) (Γ₁ : Set (Formula ℕ)) [C₁.DefinedBy Γ₁] (C₂ : FrameClass) (Γ₂ : Set (Formula ℕ)) [C₂.DefinedBy Γ₂] (C₃ : FrameClass) (Γ₃ : Set (Formula ℕ)) [C₃.DefinedBy Γ₃] : (C₁ ∩ C₂ ∩ C₃).DefinedBy (Γ₁ ∪ Γ₂ ∪ Γ₃)

theorem LO.Modal.Kripke.FrameClass.definedByFormula_triinter (C₁ : FrameClass) (φ₁ : Formula ℕ) [C₁.DefinedByFormula φ₁] (C₂ : FrameClass) (φ₂ : Formula ℕ) [C₂.DefinedByFormula φ₂] (C₃ : FrameClass) (φ₃ : Formula ℕ) [C₃.DefinedByFormula φ₃] : (C₁ ∩ C₂ ∩ C₃).DefinedBy {φ₁, φ₂, φ₃}

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

Imported declaration from the Incompleteness formalization.

• nonempty : Nonempty ↑C

@[reducible, inline]

abbrev LO.Modal.Kripke.AllFrameClass : FrameClass

Imported declaration from the Incompleteness formalization.

Equations

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

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

instance LO.Modal.Kripke.AllFrameClass.IsNonempty : AllFrameClass.IsNonempty

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