Fixed-Point Theorem for Box and Diamond Formulas

Here we prove the fixed-point theorem for formulas of form □φ and ◇φ.

theorem semantic_substitution_lemma {α : Type} (M : Model α) (u : α) (n : ℕ) (φ ψ χ : Formula) : evaluate (M, u) ((fun (φ : Formula) => φ&□φ) ((~φ v ψ)&~ψ v φ)) → evaluate (M, u) ((~single n φ χ v single n ψ χ)&~single n ψ χ v single n φ χ)

Semantic Substitution Lemma for logics with transitive frames.

@[irreducible]

theorem GL_eval_not_box_prop {α : Type} {M : Model α} {u : α} {φ : Formula} : ¬evaluate (M, u) (□φ) → ∃ (w : α), M.R u w ∧ evaluate (M, w) (□φ) ∧ ¬evaluate (M, w) φ

On transitive and conversely well-founded frames: if u ⊭ □ φ then there is w such that u R w and w ⊨ □ φ.

theorem FPT_box_helper (φ : Formula) (n : ℕ) : ⊨(~(fun (φ : Formula) => φ&□φ) ((~at n v single n ⊤ (□φ))&~single n ⊤ (□φ)v at n)v(~at n v□φ)&~□φ v at n)

Helper lemma for the fixed point theorem for □φ.

theorem FPT_diamond_helper (φ : Formula) (n : ℕ) : ⊨(~(fun (φ : Formula) => φ&□φ) ((~at n v single n ⊥ (◇φ))&~single n ⊥ (◇φ)v at n)v(~at n v◇φ)&~◇φ v at n)

Helper lemma for the fixed point theorem for ◇φ.

theorem evaluate_box_dot_iff (φ : Formula) : ⊨(fun (φ : Formula) => φ&□φ) ((~φ v φ)&~φ v φ)

Simplification lemma for the fixed point theorem.

theorem FPT_box (φ : Formula) (n : ℕ) : ⊨((~single n ⊤ (□φ)v single n (□single n ⊤ φ) (□φ))&~single n (□single n ⊤ φ) (□φ)v single n ⊤ (□φ))

□ φ case of the fixed point theorem

theorem FPT_diamond (φ : Formula) (n : ℕ) : ⊨((~single n ⊥ (◇φ)v single n (◇single n ⊥ φ) (◇φ))&~single n (◇single n ⊥ φ) (◇φ)v single n ⊥ (◇φ))

◇ φ case of the fixed point theorem

theorem FPT_box_vocab (φ : Formula) (n : ℕ) : n ∉ (single n ⊤ (□φ)).vocab ∧ (single n ⊤ (□φ)).vocab ⊆ (□φ).vocab

Vocabulary condition for □ φ case of the fixed point theorem

theorem FPT_diamond_vocab (φ : Formula) (n : ℕ) : n ∉ (single n ⊥ (◇φ)).vocab ∧ (single n ⊥ (◇φ)).vocab ⊆ (◇φ).vocab

Vocabulary condition for ◇ φ case of the fixed point theorem

theorem fixed_point_theorem_box_or_dia (φ : Formula) (n : ℕ) (box_or_dia : φ.isBox = true ∨ φ.isDiamond = true) : ∃ (ψ : Formula), n ∉ ψ.vocab ∧ semEquiv ψ (single n ψ φ) ∧ ψ.vocab ⊆ φ.vocab

Fixed-point theorem for formulas □φ and ◇φ.