def LO.Modal.independency {α : Type u_1} (φ : Formula α) : Formula α

Equations

• LO.Modal.independency φ = ∼□φ ⋏ ∼□(∼φ)

def LO.Modal.higherIndependency {α : Type u_1} (φ : Formula α) : ℕ → Formula α

Equations

• LO.Modal.higherIndependency φ 0 = φ
• LO.Modal.higherIndependency φ n.succ = LO.Modal.independency (LO.Modal.higherIndependency φ n)

theorem LO.Modal.Hilbert.GL.unprovable_notbox {φ : Formula ℕ} : Hilbert.GL ℕ ⊬ ∼□φ

theorem LO.Modal.Hilbert.GL.unprovable_independency {φ : Formula ℕ} : Hilbert.GL ℕ ⊬ independency φ

theorem LO.Modal.Hilbert.GL.unprovable_not_independency_of_consistency : Hilbert.GL ℕ ⊬ ∼independency (∼□⊥)

theorem LO.Modal.Hilbert.GL.undecidable_independency_of_consistency : System.Undecidable (Hilbert.GL ℕ) (independency (∼□⊥))

theorem LO.Modal.Hilbert.GL.unprovable_higherIndependency_of_consistency {n : ℕ} : Hilbert.GL ℕ ⊬ higherIndependency (∼□⊥) n

theorem LO.Modal.Hilbert.GL.unprovable_not_higherIndependency_of_consistency {n : ℕ} : Hilbert.GL ℕ ⊬ ∼higherIndependency (∼□⊥) n

theorem LO.Modal.Hilbert.GL.undecidable_higherIndependency_of_consistency {n : ℕ} : System.Undecidable (Hilbert.GL ℕ) (higherIndependency (∼□⊥) n)