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} [Compl α] (a : α) : Prop

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

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

@[implicit_reducible]

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

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

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

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

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

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

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

theorem Heyting.IsRegular.disjoint_compl_right_iff {α : Type u_1} [HeytingAlgebra α] {a b : α} (hb : 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.

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

The Boolean algebra of Heyting regular elements.

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

The coercion Regular α → α

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

@[implicit_reducible]

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

theorem Heyting.Regular.coe_injective {α : Type u_1} [HeytingAlgebra α] : Function.Injective val

@[simp]

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

@[implicit_reducible]

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

@[implicit_reducible]

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

@[implicit_reducible]

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

@[implicit_reducible]

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

@[implicit_reducible]

instance Heyting.Regular.instCompl {α : Type u_1} [HeytingAlgebra α] : Compl (Regular α)

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

@[simp]

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

@[simp]

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

@[implicit_reducible]

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

@[implicit_reducible]

instance Heyting.Regular.instPartialOrder {α : Type u_1} [HeytingAlgebra α] : PartialOrder (Regular α)

@[implicit_reducible]

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

@[simp]

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

@[simp]

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

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

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

@[simp]

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

@[simp]

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

def Heyting.Regular.gi {α : Type u_1} [HeytingAlgebra α] : GaloisInsertion (⇑toRegular) val

The Galois insertion between Regular.toRegular and coe.

@[implicit_reducible]

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

@[simp]

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

@[implicit_reducible]

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

@[simp]

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

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

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

A decidable proposition is intuitionistically Heyting-regular.