Basic

def LO.Modal.Formula.TrivTranslation {α : Type u_1} : Formula α → Formula α

Imported declaration from the Incompleteness formalization.

Equations

• LO.Modal.Formula.atom aᵀ = LO.Modal.Formula.atom a
• φ.boxᵀ = φᵀ
• LO.Modal.Formula.falsumᵀ = ⊥
• φ.imp ψᵀ = φᵀ ==> ψᵀ

def LO.Modal.Formula.«term_ᵀ» : Lean.TrailingParserDescr

Imported declaration from the Incompleteness formalization.

Equations

• LO.Modal.Formula.«term_ᵀ» = Lean.ParserDescr.trailingNode `LO.Modal.Formula.«term_ᵀ» 75 75 (Lean.ParserDescr.symbol "ᵀ")

@[simp]

theorem LO.Modal.Formula.TrivTranslation.degree_zero {α✝ : Type u_1} {φ : Formula α✝} : φᵀ.degree = 0

@[simp]

theorem LO.Modal.Formula.TrivTranslation.back {α✝ : Type u_1} {φ : Formula α✝} : (φᵀᴾ) ⋯ᴹ = φᵀ

def LO.Modal.Formula.VerTranslation {α : Type u_1} : Formula α → Formula α

Imported declaration from the Incompleteness formalization.

Equations

• LO.Modal.Formula.atom aⱽ = LO.Modal.Formula.atom a
• φ.boxⱽ = ⊤
• LO.Modal.Formula.falsumⱽ = ⊥
• φ.imp ψⱽ = φⱽ ==> ψⱽ

def LO.Modal.Formula.«term_ⱽ» : Lean.TrailingParserDescr

Imported declaration from the Incompleteness formalization.

Equations

• LO.Modal.Formula.«term_ⱽ» = Lean.ParserDescr.trailingNode `LO.Modal.Formula.«term_ⱽ» 75 75 (Lean.ParserDescr.symbol "ⱽ")

@[simp]

theorem LO.Modal.Formula.VerTranslation.degree_zero {α✝ : Type u_1} {φ : Formula α✝} : φⱽ.degree = 0

@[simp]

theorem LO.Modal.Formula.VerTranslation.back {α✝ : Type u_1} {φ : Formula α✝} : (φⱽᴾ) ⋯ᴹ = φⱽ

theorem LO.Modal.Hilbert.provable_of_classical_provable {mH : Hilbert ℕ} {φ : IntProp.Formula ℕ} : IntProp.Hilbert.Cl ⊢! φ → mH ⊢! φᴹ

theorem LO.Modal.Hilbert.Triv.iff_trivTranslated {φ : Formula ℕ} : Hilbert.Triv ⊢! φ <=> φᵀ

theorem LO.Modal.Hilbert.Triv.classical_reducible {φ : Formula ℕ} : Hilbert.Triv ⊢! φ ↔ IntProp.Hilbert.Cl ⊢! (φᵀᴾ) ⋯

theorem LO.Modal.Hilbert.Ver.iff_verTranslated {φ : Formula ℕ} : Hilbert.Ver ⊢! φ <=> φⱽ

theorem LO.Modal.Hilbert.Ver.classical_reducible {φ : Formula ℕ} : Hilbert.Ver ⊢! φ ↔ IntProp.Hilbert.Cl ⊢! (φⱽᴾ) ⋯