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

• 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]

ink

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

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

Equations

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

ink

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

ink

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

Equations

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

ink

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

ink

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

ink

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

ink

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

ink

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

ink

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

ink

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

ink

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

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

Equations

• One or more equations did not get rendered due to their size.

ink

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

The boolean algebra of Heyting regular elements.

Equations

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

ink

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

The coercion Regular α → α→ α

Equations

• Heyting.Regular.val = Subtype.val

ink

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

ink

instance Heyting.Regular.instCoeRegular {α : Type u_1} [inst : HeytingAlgebra α] : Coe (Heyting.Regular α) α

Equations

• Heyting.Regular.instCoeRegular = { coe := Heyting.Regular.val }

ink

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

ink

@[simp]

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

ink

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

Equations

• Heyting.Regular.top = { top := { val := ⊤, property := (_ : Heyting.IsRegular ⊤) } }

ink

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

Equations

• Heyting.Regular.bot = { bot := { val := ⊥, property := (_ : Heyting.IsRegular ⊥) } }

ink

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

Equations

• Heyting.Regular.inf = { inf := fun a b => { val := ↑a ⊓ ↑b, property := (_ : Heyting.IsRegular (↑a ⊓ ↑b)) } }

ink

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

Equations

• Heyting.Regular.himp = { himp := fun a b => { val := ↑a ⇨ ↑b, property := (_ : Heyting.IsRegular (↑a ⇨ ↑b)) } }

ink

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

Equations

• Heyting.Regular.hasCompl = { compl := fun a => { val := ↑aᶜ, property := (_ : Heyting.IsRegular (↑aᶜ)) } }

ink

@[simp]

theorem Heyting.Regular.coe_top {α : Type u_1} [inst : HeytingAlgebra α] : ↑⊤ = ⊤

ink

@[simp]

theorem Heyting.Regular.coe_bot {α : Type u_1} [inst : HeytingAlgebra α] : ↑⊥ = ⊥

ink

@[simp]

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

ink

@[simp]

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

ink

@[simp]

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

ink

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

Equations

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

ink

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

Equations

• One or more equations did not get rendered due to their size.

ink

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

Equations

• Heyting.Regular.boundedOrder = BoundedOrder.lift Heyting.Regular.val (_ : ∀ (x x_1 : Heyting.Regular α), ↑x ≤ ↑x_1 → ↑x ≤ ↑x_1) (_ : ↑⊤ = ⊤) (_ : ↑⊥ = ⊥)

ink

@[simp]

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

ink

@[simp]

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

ink

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

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

Equations

• One or more equations did not get rendered due to their size.

ink

@[simp]

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

ink

@[simp]

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

ink

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.

ink

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

Equations

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

ink

@[simp]

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

ink

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

Equations

• One or more equations did not get rendered due to their size.

ink

@[simp]

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

ink

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

ink

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

A decidable proposition is intuitionistically Heyting-regular.