The de Jongh–Sambin fixed point theorem for GL

References

• [SV82, Lemma 4.3, Theorem 4.4]

theorem FFL.ProvabilityLogic.Logic.GL.fixpoint_unique {α : Type u} [DecidableEq α] {p : α} {A D E : Formula α} (hA : Formula.ModalizedIn p A) (hD : 𝐆𝐋 ⊢ Formula.subst (Formula.Substitution.single p D) A 🡘 D) (hE : 𝐆𝐋 ⊢ Formula.subst (Formula.Substitution.single p E) A 🡘 E) : 𝐆𝐋 ⊢ D 🡘 E

• [SV82, Lemma 4.3]

theorem FFL.ProvabilityLogic.Logic.GL.exists_fixpoint {α : Type u} [DecidableEq α] {p q : α} {A : Formula α} (hpq : p ≠ q) (hA : Formula.ModalizedIn p A) (hq : q ∉ A.atoms) : ∃ (D : Formula α), D.atoms ⊆ A.atoms.erase p ∧ 𝐆𝐋 ⊢ Formula.subst (Formula.Substitution.single p D) A 🡘 D

• [SV82, Theorem 4.4]

theorem FFL.ProvabilityLogic.Logic.GL.fixpoint_theorem {α : Type u} [DecidableEq α] {p q : α} {A : Formula α} (hpq : p ≠ q) (hA : Formula.ModalizedIn p A) (hq : q ∉ A.atoms) : ∃ (D : Formula α), D.atoms ⊆ A.atoms.erase p ∧ 𝐆𝐋 ⊢ Formula.subst (Formula.Substitution.single p D) A 🡘 D ∧ ∀ (E : Formula α), 𝐆𝐋 ⊢ Formula.subst (Formula.Substitution.single p E) A 🡘 E → 𝐆𝐋 ⊢ D 🡘 E

• [SV82, Lemma 4.3, Theorem 4.4]