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

• IsRegular: a is Heyting-regular if aᶜᶜ = a.
• Regular: The subtype of Heyting-regular elements.
• Regular.BooleanAlgebra: Heyting-regular elements form a boolean algebra.

References

• [Francis Borceux, Handbook of Categorical Algebra III][borceux-vol3]

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

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

Equations

• Heyting.IsRegular a = (aᶜᶜ = a)

theorem Heyting.IsRegular.eq {α : Type u_1} [HasCompl α] {a : α} : Heyting.IsRegular a → aᶜᶜ = a

instance Heyting.IsRegular.decidablePred {α : Type u_1} [HasCompl α] [DecidableEq α] : DecidablePred Heyting.IsRegular

Equations

• Heyting.IsRegular.decidablePred x = inst xᶜᶜ x

theorem Heyting.isRegular_bot {α : Type u_1} [HeytingAlgebra α] : Heyting.IsRegular ⊥

theorem Heyting.isRegular_top {α : Type u_1} [HeytingAlgebra α] : Heyting.IsRegular ⊤

theorem Heyting.IsRegular.inf {α : Type u_1} [HeytingAlgebra α] {a b : α} (ha : Heyting.IsRegular a) (hb : Heyting.IsRegular b) : Heyting.IsRegular (a ⊓ b)

theorem Heyting.IsRegular.himp {α : Type u_1} [HeytingAlgebra α] {a b : α} (ha : Heyting.IsRegular a) (hb : Heyting.IsRegular b) : Heyting.IsRegular (a ⇨ b)

theorem Heyting.isRegular_compl {α : Type u_1} [HeytingAlgebra α] (a : α) : Heyting.IsRegular aᶜ

theorem Heyting.IsRegular.disjoint_compl_left_iff {α : Type u_1} [HeytingAlgebra α] {a b : α} (ha : Heyting.IsRegular a) : Disjoint aᶜ b ↔ b ≤ a

theorem Heyting.IsRegular.disjoint_compl_right_iff {α : Type u_1} [HeytingAlgebra α] {a b : α} (hb : Heyting.IsRegular b) : Disjoint a bᶜ ↔ a ≤ b

@[reducible, inline]

abbrev BooleanAlgebra.ofRegular {α : Type u_1} [HeytingAlgebra α] (h : ∀ (a : α), Heyting.IsRegular (a ⊔ aᶜ)) : BooleanAlgebra α

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

Equations

• BooleanAlgebra.ofRegular h = BooleanAlgebra.mk ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

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

The boolean algebra of Heyting regular elements.

Equations

• Heyting.Regular α = { a : α // Heyting.IsRegular a }

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

The coercion Regular α → α

Equations

• Heyting.Regular.val = Subtype.val

theorem Heyting.Regular.prop {α : Type u_1} [HeytingAlgebra α] (a : Heyting.Regular α) : Heyting.IsRegular ↑a

instance Heyting.Regular.instCoeOut {α : Type u_1} [HeytingAlgebra α] : CoeOut (Heyting.Regular α) α

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 b : Heyting.Regular α} : ↑a = ↑b ↔ a = b

instance Heyting.Regular.top {α : Type u_1} [HeytingAlgebra α] : Top (Heyting.Regular α)

Equations

• Heyting.Regular.top = { top := ⟨⊤, ⋯⟩ }

instance Heyting.Regular.bot {α : Type u_1} [HeytingAlgebra α] : Bot (Heyting.Regular α)

Equations

• Heyting.Regular.bot = { bot := ⟨⊥, ⋯⟩ }

instance Heyting.Regular.inf {α : Type u_1} [HeytingAlgebra α] : Min (Heyting.Regular α)

Equations

• Heyting.Regular.inf = { min := fun (a b : Heyting.Regular α) => ⟨↑a ⊓ ↑b, ⋯⟩ }

instance Heyting.Regular.himp {α : Type u_1} [HeytingAlgebra α] : HImp (Heyting.Regular α)

Equations

• Heyting.Regular.himp = { himp := fun (a b : Heyting.Regular α) => ⟨↑a ⇨ ↑b, ⋯⟩ }

instance Heyting.Regular.hasCompl {α : Type u_1} [HeytingAlgebra α] : HasCompl (Heyting.Regular α)

Equations

• Heyting.Regular.hasCompl = { compl := fun (a : Heyting.Regular α) => ⟨(↑a)ᶜ, ⋯⟩ }

@[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 b : Heyting.Regular α) : ↑(a ⊓ b) = ↑a ⊓ ↑b

@[simp]

theorem Heyting.Regular.coe_himp {α : Type u_1} [HeytingAlgebra α] (a b : Heyting.Regular α) : ↑(a ⇨ b) = ↑a ⇨ ↑b

@[simp]

theorem Heyting.Regular.coe_compl {α : Type u_1} [HeytingAlgebra α] (a : Heyting.Regular α) : ↑aᶜ = (↑a)ᶜ

instance Heyting.Regular.instInhabited {α : Type u_1} [HeytingAlgebra α] : Inhabited (Heyting.Regular α)

Equations

• Heyting.Regular.instInhabited = { default := ⊥ }

instance Heyting.Regular.instSemilatticeInf {α : Type u_1} [HeytingAlgebra α] : SemilatticeInf (Heyting.Regular α)

Equations

• Heyting.Regular.instSemilatticeInf = Function.Injective.semilatticeInf Heyting.Regular.val ⋯ ⋯

instance Heyting.Regular.boundedOrder {α : Type u_1} [HeytingAlgebra α] : BoundedOrder (Heyting.Regular α)

Equations

• Heyting.Regular.boundedOrder = BoundedOrder.lift Heyting.Regular.val ⋯ ⋯ ⋯

@[simp]

theorem Heyting.Regular.coe_le_coe {α : Type u_1} [HeytingAlgebra α] {a b : Heyting.Regular α} : ↑a ≤ ↑b ↔ a ≤ b

@[simp]

theorem Heyting.Regular.coe_lt_coe {α : Type u_1} [HeytingAlgebra α] {a b : Heyting.Regular α} : ↑a < ↑b ↔ a < b

def Heyting.Regular.toRegular {α : Type u_1} [HeytingAlgebra α] : α →o Heyting.Regular α

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

Equations

• Heyting.Regular.toRegular = { toFun := fun (a : α) => ⟨aᶜᶜ, ⋯⟩, monotone' := ⋯ }

@[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 := ⋯ }

instance Heyting.Regular.lattice {α : Type u_1} [HeytingAlgebra α] : Lattice (Heyting.Regular α)

Equations

• Heyting.Regular.lattice = Heyting.Regular.gi.liftLattice

@[simp]

theorem Heyting.Regular.coe_sup {α : Type u_1} [HeytingAlgebra α] (a b : Heyting.Regular α) : ↑(a ⊔ b) = (↑a ⊔ ↑b)ᶜᶜ

instance Heyting.Regular.instBooleanAlgebra {α : Type u_1} [HeytingAlgebra α] : BooleanAlgebra (Heyting.Regular α)

Equations

• Heyting.Regular.instBooleanAlgebra = BooleanAlgebra.mk ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

@[simp]

theorem Heyting.Regular.coe_sdiff {α : Type u_1} [HeytingAlgebra α] (a b : Heyting.Regular α) : ↑(a \ b) = ↑a ⊓ (↑b)ᶜ

theorem Heyting.isRegular_of_boolean {α : Type u_1} [BooleanAlgebra α] (a : α) : Heyting.IsRegular a

theorem Heyting.isRegular_of_decidable (p : Prop) [Decidable p] : Heyting.IsRegular p

A decidable proposition is intuitionistically Heyting-regular.