Documentation

Mathlib.Order.Heyting.Regular

Heyting regular elements #

This file defines Heyting regular elements, elements of a Heyting algebra that are their own double complement, and proves that they form a boolean algebra.

From a logic standpoint, this means that we can perform classical logic within intuitionistic logic by simply double-negating all propositions. This is practical for synthetic computability theory.

Main declarations #

References #

def Heyting.IsRegular {α : Type u_1} [HasCompl α] (a : α) :

An element of a Heyting algebra is regular if its double complement is itself.

Equations
Instances For
    theorem Heyting.IsRegular.eq {α : Type u_1} [HasCompl α] {a : α} :
    instance Heyting.IsRegular.decidablePred {α : Type u_1} [HasCompl α] [DecidableEq α] :
    DecidablePred Heyting.IsRegular
    Equations
    theorem Heyting.IsRegular.inf {α : Type u_1} [HeytingAlgebra α] {a : α} {b : α} (ha : Heyting.IsRegular a) (hb : Heyting.IsRegular b) :
    theorem Heyting.IsRegular.himp {α : Type u_1} [HeytingAlgebra α] {a : α} {b : α} (ha : Heyting.IsRegular a) (hb : Heyting.IsRegular b) :
    theorem Heyting.IsRegular.disjoint_compl_left_iff {α : Type u_1} [HeytingAlgebra α] {a : α} {b : α} (ha : Heyting.IsRegular a) :
    @[reducible, inline]
    abbrev BooleanAlgebra.ofRegular {α : Type u_1} [HeytingAlgebra α] (h : ∀ (a : α), Heyting.IsRegular (a a)) :

    A Heyting algebra with regular excluded middle is a boolean algebra.

    Equations
    Instances For
      def Heyting.Regular (α : Type u_1) [HeytingAlgebra α] :
      Type u_1

      The boolean algebra of Heyting regular elements.

      Equations
      Instances For

        The coercion Regular α → α

        Equations
        • Heyting.Regular.val = Subtype.val
        Instances For
          Equations
          • Heyting.Regular.instCoeOut = { coe := Heyting.Regular.val }
          theorem Heyting.Regular.coe_injective {α : Type u_1} [HeytingAlgebra α] :
          Function.Injective Heyting.Regular.val
          @[simp]
          theorem Heyting.Regular.coe_inj {α : Type u_1} [HeytingAlgebra α] {a : Heyting.Regular α} {b : Heyting.Regular α} :
          a = b a = b
          Equations
          • Heyting.Regular.top = { top := , }
          Equations
          • Heyting.Regular.bot = { bot := , }
          Equations
          Equations
          Equations
          @[simp]
          theorem Heyting.Regular.coe_top {α : Type u_1} [HeytingAlgebra α] :
          =
          @[simp]
          theorem Heyting.Regular.coe_bot {α : Type u_1} [HeytingAlgebra α] :
          =
          @[simp]
          theorem Heyting.Regular.coe_inf {α : Type u_1} [HeytingAlgebra α] (a : Heyting.Regular α) (b : Heyting.Regular α) :
          (a b) = a b
          @[simp]
          theorem Heyting.Regular.coe_himp {α : Type u_1} [HeytingAlgebra α] (a : Heyting.Regular α) (b : Heyting.Regular α) :
          (a b) = a b
          @[simp]
          theorem Heyting.Regular.coe_compl {α : Type u_1} [HeytingAlgebra α] (a : Heyting.Regular α) :
          a = (↑a)
          Equations
          • Heyting.Regular.instInhabited = { default := }
          Equations
          Equations
          @[simp]
          theorem Heyting.Regular.coe_le_coe {α : Type u_1} [HeytingAlgebra α] {a : Heyting.Regular α} {b : Heyting.Regular α} :
          a b a b
          @[simp]
          theorem Heyting.Regular.coe_lt_coe {α : Type u_1} [HeytingAlgebra α] {a : Heyting.Regular α} {b : Heyting.Regular α} :
          a < b a < b

          Regularization of a. The smallest regular element greater than a.

          Equations
          • Heyting.Regular.toRegular = { toFun := fun (a : α) => a, , monotone' := }
          Instances For
            @[simp]
            theorem Heyting.Regular.coe_toRegular {α : Type u_1} [HeytingAlgebra α] (a : α) :
            (Heyting.Regular.toRegular a) = a
            @[simp]
            theorem Heyting.Regular.toRegular_coe {α : Type u_1} [HeytingAlgebra α] (a : Heyting.Regular α) :
            Heyting.Regular.toRegular a = a
            def Heyting.Regular.gi {α : Type u_1} [HeytingAlgebra α] :
            GaloisInsertion (⇑Heyting.Regular.toRegular) Heyting.Regular.val

            The Galois insertion between Regular.toRegular and coe.

            Equations
            • Heyting.Regular.gi = { choice := fun (a : α) (ha : (Heyting.Regular.toRegular a) a) => a, , gc := , le_l_u := , choice_eq := }
            Instances For
              Equations
              • Heyting.Regular.lattice = Heyting.Regular.gi.liftLattice
              @[simp]
              theorem Heyting.Regular.coe_sup {α : Type u_1} [HeytingAlgebra α] (a : Heyting.Regular α) (b : Heyting.Regular α) :
              (a b) = (a b)
              Equations
              @[simp]
              theorem Heyting.Regular.coe_sdiff {α : Type u_1} [HeytingAlgebra α] (a : Heyting.Regular α) (b : Heyting.Regular α) :
              (a \ b) = a (↑b)

              A decidable proposition is intuitionistically Heyting-regular.