Documentation

Mathlib.Order.Heyting.Regular

Heyting regular elements #

This file defines Heyting regular elements, elements of an 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} [inst : HasCompl α] (a : α) :

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

Equations
theorem Heyting.IsRegular.eq {α : Type u_1} [inst : HasCompl α] {a : α} :
instance Heyting.IsRegular.decidablePred {α : Type u_1} [inst : HasCompl α] [inst : DecidableEq α] :
DecidablePred Heyting.IsRegular
Equations
theorem Heyting.IsRegular.inf {α : Type u_1} [inst : HeytingAlgebra α] {a : α} {b : α} (ha : Heyting.IsRegular a) (hb : Heyting.IsRegular b) :
theorem Heyting.IsRegular.himp {α : Type u_1} [inst : HeytingAlgebra α] {a : α} {b : α} (ha : Heyting.IsRegular a) (hb : Heyting.IsRegular b) :
theorem Heyting.isRegular_compl {α : Type u_1} [inst : HeytingAlgebra α] (a : α) :
theorem Heyting.IsRegular.disjoint_compl_left_iff {α : Type u_1} [inst : HeytingAlgebra α] {a : α} {b : α} (ha : Heyting.IsRegular a) :
Disjoint (a) b b a
theorem Heyting.IsRegular.disjoint_compl_right_iff {α : Type u_1} [inst : HeytingAlgebra α] {a : α} {b : α} (hb : Heyting.IsRegular b) :
Disjoint a (b) a b
def BooleanAlgebra.ofRegular {α : Type u_1} [inst : HeytingAlgebra α] (h : ∀ (a : α), Heyting.IsRegular (a a)) :

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

Equations
  • One or more equations did not get rendered due to their size.
def Heyting.Regular (α : Type u_1) [inst : HeytingAlgebra α] :
Type u_1

The boolean algebra of Heyting regular elements.

Equations
def Heyting.Regular.val {α : Type u_1} [inst : HeytingAlgebra α] :
Heyting.Regular αα

The coercion Regular α → α→ α

Equations
  • Heyting.Regular.val = Subtype.val
instance Heyting.Regular.instCoeRegular {α : Type u_1} [inst : HeytingAlgebra α] :
Equations
  • Heyting.Regular.instCoeRegular = { coe := Heyting.Regular.val }
theorem Heyting.Regular.coe_injective {α : Type u_1} [inst : HeytingAlgebra α] :
Function.Injective Heyting.Regular.val
@[simp]
theorem Heyting.Regular.coe_inj {α : Type u_1} [inst : HeytingAlgebra α] {a : Heyting.Regular α} {b : Heyting.Regular α} :
a = b a = b
instance Heyting.Regular.top {α : Type u_1} [inst : HeytingAlgebra α] :
Equations
instance Heyting.Regular.bot {α : Type u_1} [inst : HeytingAlgebra α] :
Equations
instance Heyting.Regular.inf {α : Type u_1} [inst : HeytingAlgebra α] :
Equations
  • Heyting.Regular.inf = { inf := fun a b => { val := a b, property := (_ : Heyting.IsRegular (a b)) } }
instance Heyting.Regular.himp {α : Type u_1} [inst : HeytingAlgebra α] :
Equations
  • Heyting.Regular.himp = { himp := fun a b => { val := a b, property := (_ : Heyting.IsRegular (a b)) } }
Equations
@[simp]
theorem Heyting.Regular.coe_top {α : Type u_1} [inst : HeytingAlgebra α] :
=
@[simp]
theorem Heyting.Regular.coe_bot {α : Type u_1} [inst : HeytingAlgebra α] :
=
@[simp]
theorem Heyting.Regular.coe_inf {α : Type u_1} [inst : HeytingAlgebra α] (a : Heyting.Regular α) (b : Heyting.Regular α) :
↑(a b) = a b
@[simp]
theorem Heyting.Regular.coe_himp {α : Type u_1} [inst : HeytingAlgebra α] (a : Heyting.Regular α) (b : Heyting.Regular α) :
↑(a b) = a b
@[simp]
theorem Heyting.Regular.coe_compl {α : Type u_1} [inst : HeytingAlgebra α] (a : Heyting.Regular α) :
↑(a) = a
Equations
  • Heyting.Regular.instInhabitedRegular = { default := }
Equations
  • One or more equations did not get rendered due to their size.
Equations
@[simp]
theorem Heyting.Regular.coe_le_coe {α : Type u_1} [inst : HeytingAlgebra α] {a : Heyting.Regular α} {b : Heyting.Regular α} :
a b a b
@[simp]
theorem Heyting.Regular.coe_lt_coe {α : Type u_1} [inst : HeytingAlgebra α] {a : Heyting.Regular α} {b : Heyting.Regular α} :
a < b a < b

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

Equations
  • One or more equations did not get rendered due to their size.
@[simp]
theorem Heyting.Regular.coe_toRegular {α : Type u_1} [inst : HeytingAlgebra α] (a : α) :
↑(Heyting.Regular.toRegular a) = a
@[simp]
theorem Heyting.Regular.toRegular_coe {α : Type u_1} [inst : HeytingAlgebra α] (a : Heyting.Regular α) :
Heyting.Regular.toRegular a = a
def Heyting.Regular.gi {α : Type u_1} [inst : HeytingAlgebra α] :
GaloisInsertion (Heyting.Regular.toRegular) Heyting.Regular.val

The Galois insertion between Regular.toRegular and coe.

Equations
  • One or more equations did not get rendered due to their size.
instance Heyting.Regular.lattice {α : Type u_1} [inst : HeytingAlgebra α] :
Equations
@[simp]
theorem Heyting.Regular.coe_sup {α : Type u_1} [inst : HeytingAlgebra α] (a : Heyting.Regular α) (b : Heyting.Regular α) :
↑(a b) = (a b)
Equations
  • One or more equations did not get rendered due to their size.
@[simp]
theorem Heyting.Regular.coe_sdiff {α : Type u_1} [inst : HeytingAlgebra α] (a : Heyting.Regular α) (b : Heyting.Regular α) :
↑(a \ b) = a b

A decidable proposition is intuitionistically Heyting-regular.