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

Equations

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

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

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} {φ : LO.Modal.Formula α✝} : φᵀ.degree = 0

@[simp]

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

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

Equations

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

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

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} {φ : LO.Modal.Formula α✝} : φⱽ.degree = 0

@[simp]

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

theorem LO.Modal.Hilbert.provable_of_classical_provable {α : Type u_1} [DecidableEq α] {mH : LO.Modal.Hilbert α} {φ : LO.IntProp.Formula α} : LO.IntProp.Hilbert.Cl α ⊢! φ → mH ⊢! φᴹ

theorem LO.Modal.Hilbert.Triv.iff_trivTranslated {α : Type u_1} [DecidableEq α] {φ : LO.Modal.Formula α} : LO.Modal.Hilbert.Triv α ⊢! φ ⭤ φᵀ

theorem LO.Modal.Hilbert.Triv.classical_reducible {α : Type u_1} [DecidableEq α] {φ : LO.Modal.Formula α} : LO.Modal.Hilbert.Triv α ⊢! φ ↔ LO.IntProp.Hilbert.Cl α ⊢! (φᵀᴾ) ⋯

theorem LO.Modal.Hilbert.Ver.iff_verTranslated {α : Type u_1} [DecidableEq α] {φ : LO.Modal.Formula α} : LO.Modal.Hilbert.Ver α ⊢! φ ⭤ φⱽ

theorem LO.Modal.Hilbert.Ver.classical_reducible {α : Type u_1} [DecidableEq α] {φ : LO.Modal.Formula α} : LO.Modal.Hilbert.Ver α ⊢! φ ↔ LO.IntProp.Hilbert.Cl α ⊢! (φⱽᴾ) ⋯