Documentation

Foundation.Modal.Hilbert.Maximal.Basic

source
def LO.Modal.Formula.TrivTranslation {α : Type u_1} :
Formula α → Formula α
Equations
Instances For
    source
    def LO.Modal.Formula.«term_ᵀ» :
    Lean.TrailingParserDescr
    Equations
    Instances For
      source
      @[simp]
      theorem LO.Modal.Formula.TrivTranslation.degree_zero {α✝ : Type u_1} {φ : Formula α✝} :
      φᵀ.degree = 0
      source
      @[simp]
      theorem LO.Modal.Formula.TrivTranslation.back {α✝ : Type u_1} {φ : Formula α✝} :
      (φᵀᴾ) ⋯ᴹ = φᵀ
      source
      def LO.Modal.Formula.VerTranslation {α : Type u_1} :
      Formula α → Formula α
      Equations
      Instances For
        source
        def LO.Modal.Formula.«term_ⱽ» :
        Lean.TrailingParserDescr
        Equations
        Instances For
          source
          @[simp]
          theorem LO.Modal.Formula.VerTranslation.degree_zero {α✝ : Type u_1} {φ : Formula α✝} :
          φⱽ.degree = 0
          source
          @[simp]
          theorem LO.Modal.Formula.VerTranslation.back {α✝ : Type u_1} {φ : Formula α✝} :
          (φⱽᴾ) ⋯ᴹ = φⱽ
          source
          theorem LO.Modal.Hilbert.provable_of_classical_provable {α : Type u_1} [DecidableEq α] {mH : Hilbert α} {φ : IntProp.Formula α} :
          IntProp.Hilbert.Cl α ⊢! φ → mH ⊢! φᴹ
          source
          theorem LO.Modal.Hilbert.Triv.iff_trivTranslated {α : Type u_1} [DecidableEq α] {φ : Formula α} :
          Hilbert.Triv α ⊢! φ ⭤ φᵀ
          source
          theorem LO.Modal.Hilbert.Triv.classical_reducible {α : Type u_1} [DecidableEq α] {φ : Formula α} :
          Hilbert.Triv α ⊢! φ ↔ IntProp.Hilbert.Cl α ⊢! (φᵀᴾ) ⋯
          source
          theorem LO.Modal.Hilbert.Ver.iff_verTranslated {α : Type u_1} [DecidableEq α] {φ : Formula α} :
          Hilbert.Ver α ⊢! φ ⭤ φⱽ
          source
          theorem LO.Modal.Hilbert.Ver.classical_reducible {α : Type u_1} [DecidableEq α] {φ : Formula α} :
          Hilbert.Ver α ⊢! φ ↔ IntProp.Hilbert.Cl α ⊢! (φⱽᴾ) ⋯