Filtration and the finite model property

DefinitionSubformulas#✓fully proved

The finite set \(\mathrm{sub}(\varphi)\) of subformulas of a modal formula \(\varphi\), including \(\varphi\) itself, is defined by recursion: \(\mathrm{sub}(p) = \{p\}\) for an atom \(p\), \(\mathrm{sub}(\bot) = \{\bot\}\), \(\mathrm{sub}(\varphi \to \psi) = \{\varphi \to \psi\} \cup \mathrm{sub}(\varphi) \cup \mathrm{sub}(\psi)\), and \(\mathrm{sub}(\Box\varphi) = \{\Box\varphi\} \cup \mathrm{sub}(\varphi)\).

def sub : Formula Atom → Finset (Formula Atom)
  | .atom p => {.atom p}
  | .bot => {.bot}
  | .imp phi psi => insert (.imp phi psi) (sub phi ∪ sub psi)
  | .box phi => insert (.box phi) (sub phi)

Uses 1 · Used by 27

Statement usesModal formulas

Used byFinite-check criterion for K-theorems · K-theorems via finite models on sets of subformulas · S4-provability via finite reflexive transitive models · S5-provability via finite equivalence models · T-provability via finite reflexive models · Finite model property of K · Finite model property of S4 · Finite model property of S5 · Finite model property of T · Filtration worlds are realized types · Smallest filtration of a Kripke model · Worlds of the filtration · Finite validity check for K · Finite validity check for a frame condition · The finite check covers the filtration worlds · Filtration relations · The smallest filtration is a filtration · The Lemmon relation is a filtration of a transitive model · The S5 relation is a filtration of an equivalence model · Lemmon filtration relation · A filtration refutes what the model refutes · S5 filtration relation · Filtration lemma for the smallest filtration · Filtration lemma · Worlds of the same type agree on subformulas · The subformula relation is transitive · Type of a world

TheoremThe subformula relation is transitive#✓fully proved

If \(\psi\) is a subformula of a modal formula \(\varphi\), then every subformula of \(\psi\) is a subformula of \(\varphi\).

theorem sub_subset_of_mem {phi psi : Formula Atom} (h : psi ∈ phi.sub) : psi.sub ⊆ phi.sub

Uses 2 · Used by 3

Statement usesModal formulas · Subformulas

Used byThe smallest filtration is a filtration · The Lemmon relation is a filtration of a transitive model · Filtration lemma

DefinitionFinite Kripke model on sets of formulas#✓fully proved

Let \(U\) be a nonempty finite set of finite sets of formulas and \(R\) a finite set of pairs of finite sets of formulas. The Kripke model on \(U\) with relation \(R\) has the elements of \(U\) as worlds, a world \(s\) sees a world \(t\) iff \((s, t) \in R\), and an atom \(p\) is true at \(s\) iff \(p \in s\).

def finModel (U : Finset (Finset (Formula Atom))) (R : Finset (Finset (Formula Atom) ×
    Finset (Formula Atom))) (hU : U.Nonempty) : KripkeModel {s // s ∈ U} Atom where
  nonempty_world := let ⟨s, hs⟩ := hU; ⟨⟨s, hs⟩⟩
  rel s t := (s.1, t.1) ∈ R
  valuation s p := Formula.atom p ∈ s.1

Uses 2 · Used by 12

Statement usesModal formulas · Kripke model

Used byFinite-check criterion for K-theorems · K-theorems via finite models on sets of subformulas · S4-provability via finite reflexive transitive models · S5-provability via finite equivalence models · T-provability via finite reflexive models · Finite model property of S4 · Finite model property of S5 · Finite model property of T · Smallest filtration of a Kripke model · The finite check covers the filtration worlds · A filtration refutes what the model refutes · Filtration lemma

DefinitionBoolean evaluation in a finite model#✓fully proved

Given a finite set \(U\) of finite sets of formulas, a finite set \(R\) of pairs of such sets and a finite set \(s\) of formulas, the Boolean value of a formula at \(s\) is defined by recursion on the formula: an atom \(p\) is true iff \(p \in s\); \(\bot\) is false; \(\varphi \to \psi\) is true iff \(\varphi\) is false or \(\psi\) is true at \(s\); and \(\Box\varphi\) is true iff \(\varphi\) is true at every \(t \in U\) with \((s, t) \in R\).

For \(s \in U\) this computes satisfaction at \(s\) in the finite Kripke model on \(U\) with relation \(R\) in which an atom is true at a world iff it belongs to it.

def evalFin (U : Finset (Finset (Formula Atom))) (R : Finset (Finset (Formula Atom) ×
    Finset (Formula Atom))) (s : Finset (Formula Atom)) : Formula Atom → Bool
  | .atom p => decide (Formula.atom p ∈ s)
  | .bot => false
  | .imp phi psi => !evalFin U R s phi || evalFin U R s psi
  | .box phi => decide (∀ t ∈ U, (s, t) ∈ R → evalFin U R t phi = true)

Uses 1 · Used by 8

Statement usesModal formulas

Used byFinite-check criterion for K-theorems · K-theorems via finite models on sets of subformulas · S4-provability via finite reflexive transitive models · S5-provability via finite equivalence models · T-provability via finite reflexive models · Finite validity check for K · Finite validity check for a frame condition · The finite check covers the filtration worlds

DefinitionType of a world#✓fully proved

Given a Kripke model \(M\) and a modal formula \(\varphi\), the type (or \(\Sigma\)-type, for \(\Sigma\) the set of subformulas of \(\varphi\)) of a world \(w\) of \(M\) is the finite set of subformulas of \(\varphi\) that hold at \(w\) in \(M\).

noncomputable def subType (w : World) : Finset (Formula Atom) := by
  classical exact phi.sub.filter fun psi ↦ M.Satisfies w psi

Uses 4 · Used by 20

Statement usesModal formulas · Subformulas · Kripke model · Satisfaction in a Kripke model

Used byFinite-check criterion for K-theorems · T-provability via finite reflexive models · Finite model property of K · Finite model property of S4 · Finite model property of S5 · Finite model property of T · Filtration worlds are realized types · Smallest filtration of a Kripke model · Smallest filtration relation · Worlds of the filtration · Filtrations of reflexive models are reflexive · The finite check covers the filtration worlds · Filtration relations · The smallest filtration is a filtration · The Lemmon relation is a filtration of a transitive model · The S5 relation is a filtration of an equivalence model · A filtration refutes what the model refutes · Filtration lemma for the smallest filtration · Filtration lemma · Worlds of the same type agree on subformulas

DefinitionWorlds of the filtration#✓fully proved

Let \(M\) be a Kripke model and \(\varphi\) a modal formula. The worlds of the filtration of \(M\) through the subformulas of \(\varphi\) form the finite set of types occurring in \(M\): the subsets \(s\) of the set \(\mathrm{sub}(\varphi)\) of subformulas of \(\varphi\) such that \(s\) is the set of subformulas of \(\varphi\) satisfied at some world of \(M\).

noncomputable def filtrationWorlds : Finset (Finset (Formula Atom)) := by
  classical exact phi.sub.powerset.filter fun s ↦ ∃ w, subType M phi w = s

Uses 4 · Used by 21

Statement usesModal formulas · Subformulas · Kripke model · Type of a world

Used byFinite-check criterion for K-theorems · S4-provability via finite reflexive transitive models · S5-provability via finite equivalence models · T-provability via finite reflexive models · Finite model property of K · Finite model property of S4 · Finite model property of S5 · Finite model property of T · Filtration worlds are realized types · Smallest filtration of a Kripke model · Smallest filtration relation · Filtrations of reflexive models are reflexive · The finite check covers the filtration worlds · The smallest filtration is a filtration · The Lemmon relation is a filtration of a transitive model · The S5 relation is a filtration of an equivalence model · Lemmon filtration relation · A filtration refutes what the model refutes · S5 filtration relation · Filtration lemma for the smallest filtration · Filtration lemma

DefinitionSmallest filtration relation#✓fully proved

Let \(M\) be a Kripke model and \(\varphi\) a modal formula, and call the set of subformulas of \(\varphi\) satisfied at a world \(w\) of \(M\) the type of \(w\). The smallest filtration relation is the finite set of pairs \((s, t)\) of types such that there are worlds \(w\) and \(w'\) of \(M\) of types \(s\) and \(t\) with \(w'\) accessible from \(w\).

noncomputable def filtrationRel : Finset (Finset (Formula Atom) × Finset (Formula Atom)) := by
  classical exact (filtrationWorlds M phi ×ˢ filtrationWorlds M phi).filter fun st ↦
    ∃ w w', subType M phi w = st.1 ∧ subType M phi w' = st.2 ∧ M.rel w w'

Uses 4 · Used by 6

Statement usesModal formulas · Kripke model · Worlds of the filtration · Type of a world

Used byFinite-check criterion for K-theorems · T-provability via finite reflexive models · Finite model property of T · Smallest filtration of a Kripke model · The smallest filtration is a filtration · Filtration lemma for the smallest filtration

TheoremFiltration worlds are realized types#✓fully proved

Let \(M\) be a Kripke model and \(\varphi\) a modal formula, and call the set of subformulas of \(\varphi\) satisfied at a world \(w\) of \(M\) the type of \(w\). Every world \(s\) of the filtration of \(M\) through the subformulas of \(\varphi\), that is, every element of the finite set of types occurring in \(M\), is the type of some world of \(M\).

theorem exists_subType_eq {s : Finset (Formula Atom)} (hs : s ∈ filtrationWorlds M phi) :
    ∃ w, subType M phi w = s

Uses 5 · Used by 2

Statement usesModal formulas · Kripke model · Worlds of the filtration · Type of a world

Proof usesSubformulas

Used byFiltrations of reflexive models are reflexive · Filtration lemma

TheoremWorlds of the same type agree on subformulas#✓fully proved

Let \(M\) be a Kripke model and \(\varphi\) a modal formula, and call the set of subformulas of \(\varphi\) true at a world \(w\) of \(M\) the type of \(w\). If two worlds \(w\) and \(v\) of \(M\) have the same type, then every subformula \(\psi\) of \(\varphi\) holds at \(w\) iff it holds at \(v\).

theorem satisfies_iff_of_subType_eq {w v : World} (h : subType M phi w = subType M phi v)
    {psi : Formula Atom} (hpsi : psi ∈ phi.sub) : M.Satisfies w psi ↔ M.Satisfies v psi

Uses 5 · Used by 1

Statement usesModal formulas · Subformulas · Kripke model · Satisfaction in a Kripke model · Type of a world

Used byThe smallest filtration is a filtration

StructureFiltration relations#✓fully proved

Let \(M\) be a Kripke model, \(\varphi\) a modal formula, \(\Sigma\) the set of subformulas of \(\varphi\), and for a world \(w\) let \([w]\), the type of \(w\), be the set of formulas of \(\Sigma\) true at \(w\) in \(M\). A relation \(R\) on finite sets of formulas is a filtration of \(M\) through \(\Sigma\) when (min) for all worlds \(w, v\) related in \(M\), the pair \(([w], [v])\) is in \(R\), and (max) for all worlds \(w, v\) with \(([w], [v]) \in R\) and every formula \(\psi\) with \(\Box\psi \in \Sigma\), if \(\Box\psi\) holds at \(w\) in \(M\) then \(\psi\) holds at \(v\) in \(M\).

These are conditions (ii) and (iii) of Blackburn–de Rijke–Venema, Definition 2.36, in \(\Box\) form; conditions (i) and (iv) (worlds are the \(\Sigma\)-types, atoms of \(\Sigma\) true where they belong) are built into the construction of the finite model.

structure IsFiltration (R : Finset (Finset (Formula Atom) × Finset (Formula Atom))) : Prop where
  min : ∀ {w v}, M.rel w v → (subType M phi w, subType M phi v) ∈ R
  max : ∀ {w v}, (subType M phi w, subType M phi v) ∈ R → ∀ {psi}, Formula.box psi ∈ phi.sub →
    M.Satisfies w (.box psi) → M.Satisfies v psi

Uses 5 · Used by 12

Statement usesModal formulas · Subformulas · Kripke model · Satisfaction in a Kripke model · Type of a world

Used byS4-provability via finite reflexive transitive models · S5-provability via finite equivalence models · T-provability via finite reflexive models · Finite model property of S4 · Finite model property of S5 · Finite model property of T · Filtrations of reflexive models are reflexive · The smallest filtration is a filtration · The Lemmon relation is a filtration of a transitive model · The S5 relation is a filtration of an equivalence model · A filtration refutes what the model refutes · Filtration lemma

TheoremFiltration lemma#✓fully proved

Let \(M\) be a Kripke model, \(\varphi\) a modal formula, and for a world \(w\) let \([w]\), the type of \(w\), be the set of subformulas of \(\varphi\) true at \(w\) in \(M\). Let \(R\) be a filtration of \(M\) through the subformulas of \(\varphi\), and let \(M^R\) be the Kripke model whose worlds are the types of the worlds of \(M\), with accessibility relation \(R\) and an atom true at a type iff the type contains it. Then for every subformula \(\psi\) of \(\varphi\) and every world \(w\) of \(M\), \(\psi\) holds at \([w]\) in \(M^R\) iff \(\psi\) holds at \(w\) in \(M\).

theorem satisfies_finModel_filtrationWorlds_iff
    {R : Finset (Finset (Formula Atom) × Finset (Formula Atom))} (hR : IsFiltration M phi R)
    {psi : Formula Atom} (hpsi : psi ∈ phi.sub) (w : World) :
    (finModel (filtrationWorlds M phi) R (filtrationWorlds_nonempty M phi)).Satisfies
      ⟨subType M phi w, subType_mem_filtrationWorlds M phi w⟩ psi ↔ M.Satisfies w psi

Uses 10 · Used by 2

Statement usesModal formulas · Subformulas · Filtration relations · Kripke model · Satisfaction in a Kripke model · Worlds of the filtration · Finite Kripke model on sets of formulas · Type of a world

Proof usesThe subformula relation is transitive · Filtration worlds are realized types

Used byA filtration refutes what the model refutes · Filtration lemma for the smallest filtration

TheoremThe smallest filtration is a filtration#✓fully proved

Let \(M\) be a Kripke model and \(\varphi\) a modal formula, and call the set of subformulas of \(\varphi\) true at a world \(w\) the type of \(w\). The relation that relates two types when some worlds of those types are related in \(M\) is a filtration of \(M\) through the set of subformulas of \(\varphi\).

theorem isFiltration_filtrationRel : IsFiltration M phi (filtrationRel M phi)

Uses 10 · Used by 3

Statement usesModal formulas · Filtration relations · Kripke model · Smallest filtration relation

Proof usesSubformulas · The subformula relation is transitive · Satisfaction in a Kripke model · Worlds of the filtration · Worlds of the same type agree on subformulas · Type of a world

Used byT-provability via finite reflexive models · Finite model property of T · Filtration lemma for the smallest filtration

DefinitionSmallest filtration of a Kripke model#✓fully proved

Let \(M\) be a Kripke model and \(\varphi\) a modal formula, and call the set of subformulas of \(\varphi\) satisfied at a world \(w\) of \(M\) the type of \(w\). The filtration of \(M\) through the subformulas of \(\varphi\) is the Kripke model whose worlds are the types occurring in \(M\), in which a type \(s\) sees a type \(t\) iff some world of type \(s\) sees some world of type \(t\) in \(M\), and in which an atom \(p\) is true at \(s\) iff \(p \in s\).

noncomputable def filtration : KripkeModel {s // s ∈ filtrationWorlds M phi} Atom :=
  finModel (filtrationWorlds M phi) (filtrationRel M phi) (filtrationWorlds_nonempty M phi)

Uses 8 · Used by 3

Statement usesModal formulas · Subformulas · Kripke model · Satisfaction in a Kripke model · Smallest filtration relation · Worlds of the filtration · Finite Kripke model on sets of formulas · Type of a world

Used byFinite-check criterion for K-theorems · Finite model property of K · Filtration lemma for the smallest filtration

TheoremFiltration lemma for the smallest filtration#✓fully proved

Let \(M\) be a Kripke model, \(\varphi\) a modal formula, and for a world \(w\) let \([w]\), the type of \(w\), be the set of subformulas of \(\varphi\) true at \(w\) in \(M\). For every subformula \(\psi\) of \(\varphi\) and every world \(w\) of \(M\), \(\psi\) holds at \([w]\) in the smallest filtration of \(M\) through the subformulas of \(\varphi\) iff \(\psi\) holds at \(w\) in \(M\).

theorem satisfies_filtration_iff {psi : Formula Atom} (hpsi : psi ∈ phi.sub) (w : World) :
    (filtration M phi).Satisfies ⟨subType M phi w, subType_mem_filtrationWorlds M phi w⟩ psi ↔
      M.Satisfies w psi

Uses 10 · Used by 2

Statement usesModal formulas · Subformulas · Kripke model · Satisfaction in a Kripke model · Smallest filtration of a Kripke model · Worlds of the filtration · Type of a world

Proof usesSmallest filtration relation · The smallest filtration is a filtration · Filtration lemma

Used byFinite-check criterion for K-theorems · Finite model property of K

TheoremCompleteness of K, countermodel form#✓fully proved

A modal formula that is not a theorem of K fails at some world of some Kripke model.

theorem exists_not_satisfies_of_not_derivable_K {phi : Formula Atom}
    (h : ¬Derivable Axioms.K phi) :
    ∃ (W : Type u) (M : KripkeModel W Atom) (w : W), ¬M.Satisfies w phi

Uses 7 · Used by 2

Statement usesExtra axioms of the modal logic K · Theorems of a normal modal logic · Modal formulas · Kripke model · Satisfaction in a Kripke model

Proof usesGlobal validity in a Kripke model · Soundness and completeness of K

Used byFinite-check criterion for K-theorems · Finite model property of K

TheoremFinite model property of K#✓fully proved

A formula that is not a K-theorem fails in a Kripke model with at most 2 ^ |sub φ| worlds.

theorem exists_finite_countermodel {phi : Formula Atom} (h : ¬Derivable Axioms.K phi) :
    ∃ (W : Type u) (_ : Fintype W) (M : KripkeModel W Atom),
      Fintype.card W ≤ 2 ^ phi.sub.card ∧ ¬M.Valid phi

Uses 12

Statement usesExtra axioms of the modal logic K · Theorems of a normal modal logic · Modal formulas · Subformulas · Kripke model · Global validity in a Kripke model

Proof usesSatisfaction in a Kripke model · Completeness of K, countermodel form · Smallest filtration of a Kripke model · Worlds of the filtration · Filtration lemma for the smallest filtration · Type of a world

DefinitionFinite validity check for K#✓fully proved

A modal formula \(\varphi\) passes the finite check when, for every nonempty set \(U\) of subsets of the set \(\mathrm{sub}(\varphi)\) of subformulas of \(\varphi\), every relation \(R \subseteq U \times U\) and every \(s \in U\), the formula \(\varphi\) is true at \(s\) in the Kripke model with set of worlds \(U\), accessibility relation \(R\), and an atom \(p\) true at a world \(t\) iff \(p \in t\); truth is computed by recursion on \(\varphi\).

def FinValid (phi : Formula Atom) : Prop :=
  ∀ U ∈ phi.sub.powerset.powerset, U.Nonempty → ∀ R ∈ (U ×ˢ U).powerset, ∀ s ∈ U,
    evalFin U R s phi = true

Uses 3 · Used by 2

Statement usesModal formulas · Subformulas · Boolean evaluation in a finite model

Used byFinite-check criterion for K-theorems · K-theorems via finite models on sets of subformulas

TheoremFinite-check criterion for K-theorems#✓fully proved

A modal formula \(\varphi\) is a theorem of K iff it passes the following finite check: for every nonempty set \(U\) of subsets of the set \(\mathrm{sub}(\varphi)\) of subformulas of \(\varphi\), every relation \(R \subseteq U \times U\) and every \(s \in U\), \(\varphi\) evaluates to true at \(s\) in the finite Kripke model on \(U\) with relation \(R\) in which an atom \(p\) is true at \(s\) iff \(p \in s\).

theorem derivable_K_iff_finValid {phi : Formula Atom} :
    Derivable Axioms.K phi ↔ FinValid phi

Uses 16 · Used by 1

Statement usesExtra axioms of the modal logic K · Theorems of a normal modal logic · Finite validity check for K · Modal formulas

Proof usesSoundness of K for Kripke models · Subformulas · Kripke model · Satisfaction in a Kripke model · Boolean evaluation in a finite model · Completeness of K, countermodel form · Smallest filtration of a Kripke model · Smallest filtration relation · Worlds of the filtration · Finite Kripke model on sets of formulas · Filtration lemma for the smallest filtration · Type of a world

Used byK-theorems via finite models on sets of subformulas

TheoremK-theorems via finite models on sets of subformulas#✓fully proved

A modal formula \(\varphi\) is a theorem of K iff for every nonempty set \(U\) of subsets of the set \(\mathrm{sub}(\varphi)\) of subformulas of \(\varphi\) and every finite set \(R\) of pairs of finite sets of formulas, \(\varphi\) holds at every world of the Kripke model whose worlds are the elements of \(U\), in which \(s\) sees \(t\) iff \((s, t) \in R\), and in which an atom \(p\) is true at \(s\) iff \(p \in s\).

theorem derivable_K_iff_forall_finModel {phi : Formula Atom} :
    Derivable Axioms.K phi ↔
      ∀ U ⊆ phi.sub.powerset, ∀ (hU : U.Nonempty) (R : Finset (Finset (Formula Atom) ×
        Finset (Formula Atom))), (finModel U R hU).Valid phi

Uses 12

Statement usesExtra axioms of the modal logic K · Theorems of a normal modal logic · Modal formulas · Subformulas · Global validity in a Kripke model · Finite Kripke model on sets of formulas

Proof usesSoundness of K for Kripke models · Finite validity check for K · Kripke model · Satisfaction in a Kripke model · Finite-check criterion for K-theorems · Boolean evaluation in a finite model

TheoremA filtration refutes what the model refutes#✓fully proved

Let \(M\) be a Kripke model, \(\varphi\) a formula and \(R\) a filtration of \(M\) through the subformulas of \(\varphi\). If \(\varphi\) fails at some world of \(M\), then \(\varphi\) is not valid in the finite model whose worlds are the types of worlds of \(M\) (the sets of subformulas of \(\varphi\) satisfied at a world), with relation \(R\) and an atom true at a type iff it belongs to it.

theorem not_valid_finModel_of_isFiltration
    {R : Finset (Finset (Formula Atom) × Finset (Formula Atom))} (hR : IsFiltration M phi R)
    {w : World} (hw : ¬M.Satisfies w phi) :
    ¬(finModel (filtrationWorlds M phi) R (filtrationWorlds_nonempty M phi)).Valid phi

Uses 10 · Used by 6

Statement usesModal formulas · Subformulas · Filtration relations · Kripke model · Satisfaction in a Kripke model · Global validity in a Kripke model · Worlds of the filtration · Finite Kripke model on sets of formulas · Type of a world

Proof usesFiltration lemma

Used byS4-provability via finite reflexive transitive models · S5-provability via finite equivalence models · T-provability via finite reflexive models · Finite model property of S4 · Finite model property of S5 · Finite model property of T

DefinitionLemmon filtration relation#✓fully proved

Let \(M\) be a Kripke model and \(\varphi\) a formula, and let \(U_\varphi\) be the set of types of worlds of \(M\) (the sets of subformulas of \(\varphi\) satisfied at a world). The Lemmon relation is the relation \(R\) on \(U_\varphi\) such that \(s \mathrel{R} t\) iff for every formula \(\psi\) with \(\Box\psi\) a subformula of \(\varphi\), \(\Box\psi \in s\) implies \(\Box\psi \in t\) and \(\psi \in t\).

This is the \(\Box\) form of Blackburn–de Rijke–Venema's transitive filtration \(R^t\) (Lemma 2.42).

noncomputable def lemmonRel : Finset (Finset (Formula Atom) × Finset (Formula Atom)) := by
  classical exact (filtrationWorlds M phi ×ˢ filtrationWorlds M phi).filter fun st ↦
    ∀ psi, Formula.box psi ∈ phi.sub → Formula.box psi ∈ st.1 →
      Formula.box psi ∈ st.2 ∧ psi ∈ st.2

Uses 4 · Used by 3

Statement usesModal formulas · Subformulas · Kripke model · Worlds of the filtration

Used byS4-provability via finite reflexive transitive models · Finite model property of S4 · The Lemmon relation is a filtration of a transitive model

DefinitionS5 filtration relation#✓fully proved

Let \(M\) be a Kripke model and \(\varphi\) a formula, and let \(U_\varphi\) be the set of types of worlds of \(M\) (the sets of subformulas of \(\varphi\) satisfied at a world). The S5 relation is the relation \(R\) on \(U_\varphi\) such that \(s \mathrel{R} t\) iff for every formula \(\psi\) with \(\Box\psi\) a subformula of \(\varphi\), \(\Box\psi \in s\) iff \(\Box\psi \in t\).

noncomputable def s5Rel : Finset (Finset (Formula Atom) × Finset (Formula Atom)) := by
  classical exact (filtrationWorlds M phi ×ˢ filtrationWorlds M phi).filter fun st ↦
    ∀ psi, Formula.box psi ∈ phi.sub → (Formula.box psi ∈ st.1 ↔ Formula.box psi ∈ st.2)

Uses 4 · Used by 3

Statement usesModal formulas · Subformulas · Kripke model · Worlds of the filtration

Used byS5-provability via finite equivalence models · Finite model property of S5 · The S5 relation is a filtration of an equivalence model

TheoremThe Lemmon relation is a filtration of a transitive model#✓fully proved

For every Kripke model \(M\) with a transitive accessibility relation and every formula \(\varphi\), the Lemmon relation of \(M\) and \(\varphi\) is a filtration of \(M\) through the subformulas of \(\varphi\).

theorem isFiltration_lemmonRel (htrans : ∀ {a b c}, M.rel a b → M.rel b c → M.rel a c) :
    IsFiltration M phi (lemmonRel M phi)

Uses 9 · Used by 2

Statement usesModal formulas · Filtration relations · Kripke model · Lemmon filtration relation

Proof usesSubformulas · The subformula relation is transitive · Satisfaction in a Kripke model · Worlds of the filtration · Type of a world

Used byS4-provability via finite reflexive transitive models · Finite model property of S4

TheoremThe S5 relation is a filtration of an equivalence model#✓fully proved

For every Kripke model \(M\) whose accessibility relation is an equivalence relation and every formula \(\varphi\), the S5 relation of \(M\) and \(\varphi\) is a filtration of \(M\) through the subformulas of \(\varphi\).

theorem isFiltration_s5Rel (hequiv : Equivalence M.rel) : IsFiltration M phi (s5Rel M phi)

Uses 8 · Used by 2

Statement usesModal formulas · Filtration relations · Kripke model · S5 filtration relation

Proof usesSubformulas · Satisfaction in a Kripke model · Worlds of the filtration · Type of a world

Used byS5-provability via finite equivalence models · Finite model property of S5

DefinitionReflexivity on a finite set of worlds#✓fully proved

Let \(U\) be a finite set of finite sets of modal formulas and \(R\) a finite set of pairs of such sets. Then \(R\) is reflexive on \(U\) when \((s, s) \in R\) for every \(s \in U\).

def FinRefl (U : Finset (Finset (Formula Atom)))
    (R : Finset (Finset (Formula Atom) × Finset (Formula Atom))) : Prop :=
  ∀ s ∈ U, (s, s) ∈ R

Uses 1 · Used by 7

Statement usesModal formulas

Used byS4-provability via finite reflexive transitive models · S5-provability via finite equivalence models · T-provability via finite reflexive models · Finite model property of S4 · Finite model property of S5 · Finite model property of T · Filtrations of reflexive models are reflexive

DefinitionTransitivity on a finite set of worlds#✓fully proved

Let \(U\) be a finite set of finite sets of modal formulas and \(R\) a finite set of pairs of such sets. Then \(R\) is transitive on \(U\) when \((s, r) \in R\) for all \(s, t, r \in U\) with \((s, t) \in R\) and \((t, r) \in R\).

def FinTrans (U : Finset (Finset (Formula Atom)))
    (R : Finset (Finset (Formula Atom) × Finset (Formula Atom))) : Prop :=
  ∀ s ∈ U, ∀ t ∈ U, ∀ r ∈ U, (s, t) ∈ R → (t, r) ∈ R → (s, r) ∈ R

Uses 1 · Used by 4

Statement usesModal formulas

Used byS4-provability via finite reflexive transitive models · S5-provability via finite equivalence models · Finite model property of S4 · Finite model property of S5

DefinitionSymmetry on a finite set of worlds#✓fully proved

Let \(U\) be a finite set of finite sets of modal formulas and \(R\) a finite set of pairs of such sets. Then \(R\) is symmetric on \(U\) when \((t, s) \in R\) for all \(s, t \in U\) with \((s, t) \in R\).

def FinSymm (U : Finset (Finset (Formula Atom)))
    (R : Finset (Finset (Formula Atom) × Finset (Formula Atom))) : Prop :=
  ∀ s ∈ U, ∀ t ∈ U, (s, t) ∈ R → (t, s) ∈ R

Uses 1 · Used by 2

Statement usesModal formulas

Used byS5-provability via finite equivalence models · Finite model property of S5

TheoremFiltrations of reflexive models are reflexive#✓fully proved

Let \(M\) be a Kripke model whose accessibility relation is reflexive, let \(\varphi\) be a modal formula, and let \(R\) be a filtration of \(M\) through the subformulas of \(\varphi\). Then \((s, s) \in R\) for every set \(s\) that is the set of subformulas of \(\varphi\) true at some world of \(M\).

theorem finRefl_of_isFiltration {R : Finset (Finset (Formula Atom) × Finset (Formula Atom))}
    (hR : IsFiltration M phi R) (hrefl : ∀ w, M.rel w w) : FinRefl (filtrationWorlds M phi) R

Uses 7 · Used by 6

Statement usesReflexivity on a finite set of worlds · Modal formulas · Filtration relations · Kripke model · Worlds of the filtration

Proof usesFiltration worlds are realized types · Type of a world

Used byS4-provability via finite reflexive transitive models · S5-provability via finite equivalence models · T-provability via finite reflexive models · Finite model property of S4 · Finite model property of S5 · Finite model property of T

TheoremFinite model property of T#✓fully proved

If a modal formula \(\varphi\) is not a theorem of T, then there is a Kripke model with finitely many worlds, at most \(2^{|\mathrm{sub}(\varphi)|}\) of them, where \(\mathrm{sub}(\varphi)\) is the set of subformulas of \(\varphi\), whose accessibility relation is reflexive and in which \(\varphi\) is false at some world.

theorem exists_finite_countermodel_T (h : ¬Derivable Axioms.T phi) :
    ∃ (W : Type u) (_ : Fintype W) (M : KripkeModel W Atom),
      Fintype.card W ≤ 2 ^ phi.sub.card ∧ (∀ w, M.rel w w) ∧ ¬M.Valid phi

Uses 17

Statement usesExtra axioms of T · Theorems of a normal modal logic · Modal formulas · Subformulas · Kripke model · Global validity in a Kripke model

Proof usesReflexivity on a finite set of worlds · Filtration relations · Satisfaction in a Kripke model · Soundness and completeness of T · Smallest filtration relation · Worlds of the filtration · Finite Kripke model on sets of formulas · Filtrations of reflexive models are reflexive · The smallest filtration is a filtration · A filtration refutes what the model refutes · Type of a world

TheoremFinite model property of S4#✓fully proved

If a modal formula \(\varphi\) is not a theorem of S4, then there is a Kripke model with finitely many worlds, at most \(2^{|\mathrm{sub}(\varphi)|}\) of them, where \(\mathrm{sub}(\varphi)\) is the set of subformulas of \(\varphi\), whose accessibility relation is reflexive and transitive and in which \(\varphi\) is false at some world.

theorem exists_finite_countermodel_S4 (h : ¬Derivable Axioms.S4 phi) :
    ∃ (W : Type u) (_ : Fintype W) (M : KripkeModel W Atom),
      Fintype.card W ≤ 2 ^ phi.sub.card ∧ ((∀ w, M.rel w w) ∧
        ∀ {a b c}, M.rel a b → M.rel b c → M.rel a c) ∧ ¬M.Valid phi

Uses 18

Statement usesExtra axioms of S4 · Theorems of a normal modal logic · Modal formulas · Subformulas · Kripke model · Global validity in a Kripke model

Proof usesReflexivity on a finite set of worlds · Transitivity on a finite set of worlds · Filtration relations · Satisfaction in a Kripke model · Soundness and completeness of S4 · Worlds of the filtration · Finite Kripke model on sets of formulas · Filtrations of reflexive models are reflexive · The Lemmon relation is a filtration of a transitive model · Lemmon filtration relation · A filtration refutes what the model refutes · Type of a world

TheoremFinite model property of S5#✓fully proved

If a modal formula \(\varphi\) is not a theorem of S5, then there is a Kripke model with finitely many worlds, at most \(2^{|\mathrm{sub}(\varphi)|}\) of them, where \(\mathrm{sub}(\varphi)\) is the set of subformulas of \(\varphi\), whose accessibility relation is an equivalence relation and in which \(\varphi\) is false at some world.

theorem exists_finite_countermodel_S5 (h : ¬Derivable Axioms.S5 phi) :
    ∃ (W : Type u) (_ : Fintype W) (M : KripkeModel W Atom),
      Fintype.card W ≤ 2 ^ phi.sub.card ∧ Equivalence M.rel ∧ ¬M.Valid phi

Uses 19

Statement usesExtra axioms of S5 · Theorems of a normal modal logic · Modal formulas · Subformulas · Kripke model · Global validity in a Kripke model

Proof usesReflexivity on a finite set of worlds · Symmetry on a finite set of worlds · Transitivity on a finite set of worlds · Filtration relations · Satisfaction in a Kripke model · Soundness and completeness of S5 · Worlds of the filtration · Finite Kripke model on sets of formulas · Filtrations of reflexive models are reflexive · The S5 relation is a filtration of an equivalence model · A filtration refutes what the model refutes · S5 filtration relation · Type of a world

DefinitionFinite validity check for a frame condition#✓fully proved

Given a condition \(C\) on pairs \((U, R)\) of a finite set \(U\) of sets of formulas and a finite set \(R\) of pairs of such sets, a formula \(\varphi\) passes the finite check for \(C\) when, for every nonempty set \(U\) of subsets of the subformulas of \(\varphi\) and every relation \(R \subseteq U \times U\) with \(C(U, R)\), \(\varphi\) holds at every \(s \in U\) in the Kripke model with worlds \(U\), accessibility relation \(R\), and an atom true at \(s\) iff it belongs to \(s\).

def FinValidWith (C : Finset (Finset (Formula Atom)) →
    Finset (Finset (Formula Atom) × Finset (Formula Atom)) → Prop) (phi : Formula Atom) : Prop :=
  ∀ U ∈ phi.sub.powerset.powerset, U.Nonempty → ∀ R ∈ (U ×ˢ U).powerset, C U R → ∀ s ∈ U,
    evalFin U R s phi = true

Uses 3 · Used by 4

Statement usesModal formulas · Subformulas · Boolean evaluation in a finite model

Used byS4-provability via finite reflexive transitive models · S5-provability via finite equivalence models · T-provability via finite reflexive models · The finite check covers the filtration worlds

TheoremThe finite check covers the filtration worlds#✓fully proved

Let \(C\) be a condition on pairs \((U, R)\) of a finite set \(U\) of sets of formulas and a finite relation \(R\) on such sets, and let \(\varphi\) be a formula that passes the finite check for \(C\). Let \(M\) be a Kripke model, let \(U_\varphi\) be the set of types of worlds of \(M\) (the sets of subformulas of \(\varphi\) satisfied at a world), and let \(R \subseteq U_\varphi \times U_\varphi\) satisfy \(C(U_\varphi, R)\). Then \(\varphi\) is valid in the finite model on \(U_\varphi\) with relation \(R\), in which an atom holds at \(s\) iff it belongs to \(s\).

theorem finValidWith_apply {C : Finset (Finset (Formula Atom)) →
    Finset (Finset (Formula Atom) × Finset (Formula Atom)) → Prop} {phi : Formula Atom}
    (h : FinValidWith C phi) {World : Type v} (M : KripkeModel World Atom)
    {R : Finset (Finset (Formula Atom) × Finset (Formula Atom))}
    (hRsub : R ⊆ filtrationWorlds M phi ×ˢ filtrationWorlds M phi)
    (hC : C (filtrationWorlds M phi) R) :
    (finModel (filtrationWorlds M phi) R (filtrationWorlds_nonempty M phi)).Valid phi

Uses 10 · Used by 3

Statement usesFinite validity check for a frame condition · Modal formulas · Subformulas · Kripke model · Satisfaction in a Kripke model · Global validity in a Kripke model · Worlds of the filtration · Finite Kripke model on sets of formulas · Type of a world

Proof usesBoolean evaluation in a finite model

Used byS4-provability via finite reflexive transitive models · S5-provability via finite equivalence models · T-provability via finite reflexive models

TheoremT-provability via finite reflexive models#✓fully proved

A modal formula \(\varphi\) is a theorem of T if and only if, for every nonempty set \(U\) of subsets of \(\mathrm{sub}(\varphi)\), the set of subformulas of \(\varphi\), and every relation \(R \subseteq U \times U\) that is reflexive on \(U\), the formula \(\varphi\) is true at every world \(s \in U\) of the finite model with worlds \(U\), accessibility relation \(R\), and each atom true at \(s\) exactly when it belongs to \(s\).

theorem derivable_T_iff_finValidWith : Derivable Axioms.T phi ↔ FinValidWith FinRefl phi

Uses 21

Statement usesExtra axioms of T · Theorems of a normal modal logic · Reflexivity on a finite set of worlds · Finite validity check for a frame condition · Modal formulas

Proof usesSoundness of T for reflexive Kripke models · Subformulas · Filtration relations · Kripke model · Satisfaction in a Kripke model · Global validity in a Kripke model · Soundness and completeness of T · Boolean evaluation in a finite model · Smallest filtration relation · Worlds of the filtration · Finite Kripke model on sets of formulas · Filtrations of reflexive models are reflexive · The finite check covers the filtration worlds · The smallest filtration is a filtration · A filtration refutes what the model refutes · Type of a world

TheoremS4-provability via finite reflexive transitive models#✓fully proved

A modal formula \(\varphi\) is a theorem of S4 if and only if, for every nonempty set \(U\) of subsets of \(\mathrm{sub}(\varphi)\), the set of subformulas of \(\varphi\), and every relation \(R \subseteq U \times U\) that is reflexive and transitive on \(U\), the formula \(\varphi\) is true at every world \(s \in U\) of the finite model with worlds \(U\), accessibility relation \(R\), and each atom true at \(s\) exactly when it belongs to \(s\).

theorem derivable_S4_iff_finValidWith :
    Derivable Axioms.S4 phi ↔ FinValidWith (fun U R ↦ FinRefl U R ∧ FinTrans U R) phi

Uses 21

Statement usesExtra axioms of S4 · Theorems of a normal modal logic · Reflexivity on a finite set of worlds · Transitivity on a finite set of worlds · Finite validity check for a frame condition · Modal formulas

Proof usesSoundness of S4 for reflexive transitive Kripke models · Subformulas · Filtration relations · Kripke model · Satisfaction in a Kripke model · Global validity in a Kripke model · Soundness and completeness of S4 · Boolean evaluation in a finite model · Worlds of the filtration · Finite Kripke model on sets of formulas · Filtrations of reflexive models are reflexive · The finite check covers the filtration worlds · The Lemmon relation is a filtration of a transitive model · Lemmon filtration relation · A filtration refutes what the model refutes

TheoremS5-provability via finite equivalence models#✓fully proved

A modal formula \(\varphi\) is a theorem of S5 if and only if, for every nonempty set \(U\) of subsets of \(\mathrm{sub}(\varphi)\), the set of subformulas of \(\varphi\), and every relation \(R \subseteq U \times U\) that is reflexive, symmetric and transitive on \(U\), the formula \(\varphi\) is true at every world \(s \in U\) of the finite model with worlds \(U\), accessibility relation \(R\), and each atom true at \(s\) exactly when it belongs to \(s\).

theorem derivable_S5_iff_finValidWith :
    Derivable Axioms.S5 phi ↔
      FinValidWith (fun U R ↦ FinRefl U R ∧ FinSymm U R ∧ FinTrans U R) phi

Uses 22

Statement usesExtra axioms of S5 · Theorems of a normal modal logic · Reflexivity on a finite set of worlds · Symmetry on a finite set of worlds · Transitivity on a finite set of worlds · Finite validity check for a frame condition · Modal formulas

Proof usesSoundness of S5 for Kripke models with an equivalence relation · Subformulas · Filtration relations · Kripke model · Satisfaction in a Kripke model · Global validity in a Kripke model · Soundness and completeness of S5 · Boolean evaluation in a finite model · Worlds of the filtration · Finite Kripke model on sets of formulas · Filtrations of reflexive models are reflexive · The finite check covers the filtration worlds · The S5 relation is a filtration of an equivalence model · A filtration refutes what the model refutes · S5 filtration relation

36 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.