Basic

structure LO.IntProp.Kripke.Frame : Type 1

Imported declaration from the Incompleteness formalization.

• World : Type

  Imported declaration from the Incompleteness formalization.

• world_nonempty : Nonempty self.World
• Rel : _root_.Rel self.World self.World

  Imported declaration from the Incompleteness formalization.

• rel_refl : Std.Refl self.Rel
• rel_trans : IsTrans self.World self.Rel

@[implicit_reducible]

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

Equations

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

@[implicit_reducible]

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

Equations

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

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

@[reducible, inline]

abbrev LO.IntProp.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.IntProp.Kripke.«term_≺_» : Lean.TrailingParserDescr

Imported declaration from the Incompleteness formalization.

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))

@[simp]

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

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

@[reducible, inline]

abbrev LO.IntProp.Kripke.pointFrame : Frame

Imported declaration from the Incompleteness formalization.

Equations

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

@[reducible, inline]

abbrev LO.IntProp.Kripke.FrameClass : Type 1

Imported declaration from the Incompleteness formalization.

Equations

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

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

Imported declaration from the Incompleteness formalization.

• Val : F.World → ℕ → Prop

  Imported declaration from the Incompleteness formalization.

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

@[implicit_reducible]

instance LO.IntProp.Kripke.instCoeFunValuationForallWorldForallNatProp {F : Frame} : CoeFun (Valuation F) fun (x : 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

Imported declaration from the Incompleteness formalization.

• World : Type
• world_nonempty : Nonempty self.World
• Rel : _root_.Rel self.World self.World
• rel_refl : Std.Refl self.Rel
• rel_trans : IsTrans self.World self.Rel
• Val : Valuation self.toFrame

  Imported declaration from the Incompleteness formalization.

@[implicit_reducible]

instance LO.IntProp.Kripke.instCoeFunModelForallWorldForallNatProp : CoeFun Model fun (M : 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 : Kripke.Model) (w : M.World) : Formula ℕ → Prop

Imported declaration from the Incompleteness formalization.

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.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 (φ.imp ψ) = ∀ {w' : M.World}, w ≺ w' → LO.IntProp.Formula.Kripke.Satisfies M w' φ → LO.IntProp.Formula.Kripke.Satisfies M w' ψ

@[implicit_reducible]

instance LO.IntProp.Formula.Kripke.Satisfies.semantics (M : Kripke.Model) : Semantics (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 : Kripke.Model} {w : M.World} {φ : Formula ℕ} : w ⊧ φ ↔ Satisfies M w φ

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

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

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

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

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

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

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

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

Imported declaration from the Incompleteness formalization.

Equations

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

@[implicit_reducible]

instance LO.IntProp.Formula.Kripke.ValidOnModel.semantics : Semantics (Formula ℕ) 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 : Kripke.Model} {φ : Formula ℕ} : M ⊧ φ ↔ ValidOnModel M φ

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Imported declaration from the Incompleteness formalization.

Equations

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

@[implicit_reducible]

instance LO.IntProp.Formula.Kripke.ValidOnFrame.semantics : Semantics (Formula ℕ) 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 : Kripke.Frame} {φ : Formula ℕ} : F ⊧ φ ↔ ValidOnFrame F φ

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

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

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

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

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

theorem LO.IntProp.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.IntProp.Formula.Kripke.ValidOnFrame.iff_not_exists_valuation.

theorem LO.IntProp.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.IntProp.Formula.Kripke.ValidOnFrame.iff_not_exists_valuation.

theorem LO.IntProp.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.IntProp.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.IntProp.Formula.Kripke.ValidOnFrame.iff_not_exists_valuation_world.

theorem LO.IntProp.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.IntProp.Formula.Kripke.ValidOnFrame.iff_not_exists_valuation_world.

theorem LO.IntProp.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.IntProp.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.IntProp.Formula.Kripke.ValidOnFrame.iff_not_exists_model_world.

theorem LO.IntProp.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.IntProp.Formula.Kripke.ValidOnFrame.iff_not_exists_model_world.

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Imported declaration from the Incompleteness formalization.

Equations

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

@[implicit_reducible]

instance LO.IntProp.Formula.Kripke.ValidOnFrameClass.semantics : Semantics (Formula ℕ) 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 : Kripke.FrameClass} {φ : Formula ℕ} : C ⊧ φ ↔ ValidOnFrameClass C φ

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

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

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

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

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

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

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

theorem LO.IntProp.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.IntProp.Formula.Kripke.ValidOnFrameClass.iff_not_exists_model.

theorem LO.IntProp.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.IntProp.Formula.Kripke.ValidOnFrameClass.iff_not_exists_model.

theorem LO.IntProp.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.IntProp.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.IntProp.Formula.Kripke.ValidOnFrameClass.iff_not_exists_model_world.

theorem LO.IntProp.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.IntProp.Formula.Kripke.ValidOnFrameClass.iff_not_exists_model_world.

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

Imported declaration from the Incompleteness formalization.

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

class LO.IntProp.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.IntProp.Kripke.FrameClass.DefinedByFormula (C : FrameClass) (φ : Formula ℕ) : Prop

Imported declaration from the Incompleteness formalization.

Equations

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

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

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

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

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

Imported declaration from the Incompleteness formalization.

• nonempty : Nonempty ↑C

@[reducible, inline]

abbrev LO.IntProp.Kripke.AllFrameClass : FrameClass

Imported declaration from the Incompleteness formalization.

Equations

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

instance LO.IntProp.Kripke.AllFrameClass.DefinedBy : AllFrameClass.DefinedByFormula (Axioms.EFQ (Formula.atom 0))

instance LO.IntProp.Kripke.AllFrameClass.IsNonempty : AllFrameClass.IsNonempty

theorem LO.IntProp.Kripke.FrameClass.definedBy_with_axiomEFQ {C : FrameClass} {Γ : Set (Formula ℕ)} (defines : C.DefinedBy Γ) : C.DefinedBy (insert (Axioms.EFQ (Formula.atom 0)) Γ)