theorem LO.Modal.Hilbert.NNFormula.iff_neg {φ : NNFormula ℕ} : Modal.K ⊢ ∼φ.toFormula ⭤ (∼φ).toFormula

theorem LO.Modal.Hilbert.NNFormula.exists_iff {φ : Formula ℕ} : ∃ (ψ : NNFormula ℕ), Modal.K ⊢ φ ⭤ ψ.toFormula

theorem LO.Modal.Hilbert.NNFormula.exists_of_provable {φ : Formula ℕ} (h : Modal.K ⊢ φ) : ∃ (ψ : NNFormula ℕ), Modal.K ⊢ ψ.toFormula

theorem LO.Modal.Hilbert.NNFormula.exists_CNF (φ : NNFormula ℕ) : ∃ (ψ : NNFormula ℕ), ψ.isModalCNF ∧ Modal.K ⊢ φ.toFormula ⭤ ψ.toFormula

theorem LO.Modal.Hilbert.NNFormula.exists_DNF (φ : NNFormula ℕ) : ∃ (ψ : NNFormula ℕ), ψ.isModalDNF ∧ Modal.K ⊢ φ.toFormula ⭤ ψ.toFormula