mathlib3 documentation

order.heyting.regular

Heyting regular elements #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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 #

is_regular: a is Heyting-regular if aᶜᶜ = a.
regular: The subtype of Heyting-regular elements.
regular.boolean_algebra: Heyting-regular elements form a boolean algebra.

References #

Francis Borceux, Handbook of Categorical Algebra III

def heyting.is_regular {α : Type u_1} [has_compl α] (a : α) :

Prop

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

Equations

heyting.is_regular a = (aᶜ ᶜ = a)

Instances for heyting.is_regular

heyting.is_regular.decidable_pred

@[protected]

theorem heyting.is_regular.eq {α : Type u_1} [has_compl α] {a : α} :

heyting.is_regular a → aᶜ ᶜ = a

@[protected, instance]

def heyting.is_regular.decidable_pred {α : Type u_1} [has_compl α] [decidable_eq α] :

decidable_pred heyting.is_regular

Equations

heyting.is_regular.decidable_pred = λ (_x : α), _inst_2 _xᶜ ᶜ _x

theorem heyting.is_regular_bot {α : Type u_1} [heyting_algebra α] :

heyting.is_regular ⊥

theorem heyting.is_regular_top {α : Type u_1} [heyting_algebra α] :

heyting.is_regular ⊤

theorem heyting.is_regular.inf {α : Type u_1} [heyting_algebra α] {a b : α} (ha : heyting.is_regular a) (hb : heyting.is_regular b) :

heyting.is_regular (a ⊓ b)

theorem heyting.is_regular.himp {α : Type u_1} [heyting_algebra α] {a b : α} (ha : heyting.is_regular a) (hb : heyting.is_regular b) :

heyting.is_regular (a ⇨ b)

theorem heyting.is_regular_compl {α : Type u_1} [heyting_algebra α] (a : α) :

heyting.is_regular aᶜ

@[protected]

theorem heyting.is_regular.disjoint_compl_left_iff {α : Type u_1} [heyting_algebra α] {a b : α} (ha : heyting.is_regular a) :

disjoint aᶜ b ↔ b ≤ a

@[protected]

theorem heyting.is_regular.disjoint_compl_right_iff {α : Type u_1} [heyting_algebra α] {a b : α} (hb : heyting.is_regular b) :

disjoint a bᶜ ↔ a ≤ b

@[reducible]

def boolean_algebra.of_regular {α : Type u_1} [heyting_algebra α] (h : ∀ (a : α), heyting.is_regular (a ⊔ aᶜ)) :

boolean_algebra α

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

Equations

boolean_algebra.of_regular h = have this : ∀ (a : α), is_compl a aᶜ, from _, {sup := heyting_algebra.sup _inst_1, le := heyting_algebra.le _inst_1, lt := heyting_algebra.lt _inst_1, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, le_sup_left := _, le_sup_right := _, sup_le := _, inf := heyting_algebra.inf _inst_1, inf_le_left := _, inf_le_right := _, le_inf := _, le_sup_inf := _, compl := heyting_algebra.compl _inst_1, sdiff := λ (x y : α), distrib_lattice.inf x (heyting_algebra.compl y), himp := heyting_algebra.himp _inst_1, top := heyting_algebra.top _inst_1, bot := heyting_algebra.bot _inst_1, inf_compl_le_bot := _, top_le_sup_compl := _, le_top := _, bot_le := _, sdiff_eq := _, himp_eq := _}

def heyting.regular (α : Type u_1) [heyting_algebra α] :

Type u_1

The boolean algebra of Heyting regular elements.

Equations

heyting.regular α = {a // heyting.is_regular a}

Instances for heyting.regular

@[protected, instance]

def heyting.regular.has_coe {α : Type u_1} [heyting_algebra α] :

has_coe (heyting.regular α) α

Equations

heyting.regular.has_coe = coe_subtype

theorem heyting.regular.coe_injective {α : Type u_1} [heyting_algebra α] :

function.injective coe

@[simp]

theorem heyting.regular.coe_inj {α : Type u_1} [heyting_algebra α] {a b : heyting.regular α} :

↑a = ↑b ↔ a = b

@[protected, instance]

def heyting.regular.has_top {α : Type u_1} [heyting_algebra α] :

has_top (heyting.regular α)

Equations

heyting.regular.has_top = {top := ⟨⊤, _⟩}

@[protected, instance]

def heyting.regular.has_bot {α : Type u_1} [heyting_algebra α] :

has_bot (heyting.regular α)

Equations

heyting.regular.has_bot = {bot := ⟨⊥, _⟩}

@[protected, instance]

def heyting.regular.has_inf {α : Type u_1} [heyting_algebra α] :

has_inf (heyting.regular α)

Equations

heyting.regular.has_inf = {inf := λ (a b : heyting.regular α), ⟨↑a ⊓ ↑b, _⟩}

@[protected, instance]

def heyting.regular.has_himp {α : Type u_1} [heyting_algebra α] :

has_himp (heyting.regular α)

Equations

heyting.regular.has_himp = {himp := λ (a b : heyting.regular α), ⟨↑a ⇨ ↑b, _⟩}

@[protected, instance]

def heyting.regular.has_compl {α : Type u_1} [heyting_algebra α] :

has_compl (heyting.regular α)

Equations

heyting.regular.has_compl = {compl := λ (a : heyting.regular α), ⟨(↑a)ᶜ, _⟩}

@[simp, norm_cast]

theorem heyting.regular.coe_top {α : Type u_1} [heyting_algebra α] :

@[simp, norm_cast]

theorem heyting.regular.coe_bot {α : Type u_1} [heyting_algebra α] :

@[simp, norm_cast]

theorem heyting.regular.coe_inf {α : Type u_1} [heyting_algebra α] (a b : heyting.regular α) :

↑(a ⊓ b) = ↑a ⊓ ↑b

@[simp, norm_cast]

theorem heyting.regular.coe_himp {α : Type u_1} [heyting_algebra α] (a b : heyting.regular α) :

↑(a ⇨ b) = ↑a ⇨ ↑b

@[simp, norm_cast]

theorem heyting.regular.coe_compl {α : Type u_1} [heyting_algebra α] (a : heyting.regular α) :

↑aᶜ = (↑a)ᶜ

@[protected, instance]

def heyting.regular.inhabited {α : Type u_1} [heyting_algebra α] :

inhabited (heyting.regular α)

Equations

heyting.regular.inhabited = {default := ⊥}

@[protected, instance]

def heyting.regular.semilattice_inf {α : Type u_1} [heyting_algebra α] :

semilattice_inf (heyting.regular α)

Equations

heyting.regular.semilattice_inf = function.injective.semilattice_inf coe heyting.regular.coe_injective heyting.regular.coe_inf

@[protected, instance]

def heyting.regular.bounded_order {α : Type u_1} [heyting_algebra α] :

bounded_order (heyting.regular α)

Equations

heyting.regular.bounded_order = bounded_order.lift coe heyting.regular.bounded_order._proof_1 heyting.regular.coe_top heyting.regular.coe_bot

@[simp, norm_cast]

theorem heyting.regular.coe_le_coe {α : Type u_1} [heyting_algebra α] {a b : heyting.regular α} :

↑a ≤ ↑b ↔ a ≤ b

@[simp, norm_cast]

theorem heyting.regular.coe_lt_coe {α : Type u_1} [heyting_algebra α] {a b : heyting.regular α} :

↑a < ↑b ↔ a < b

def heyting.regular.to_regular {α : Type u_1} [heyting_algebra α] :

α →o heyting.regular α

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

Equations

heyting.regular.to_regular = {to_fun := λ (a : α), ⟨aᶜ ᶜ, _⟩, monotone' := _}

@[simp, norm_cast]

theorem heyting.regular.coe_to_regular {α : Type u_1} [heyting_algebra α] (a : α) :

↑(⇑heyting.regular.to_regular a) = aᶜ ᶜ

@[simp]

theorem heyting.regular.to_regular_coe {α : Type u_1} [heyting_algebra α] (a : heyting.regular α) :

⇑heyting.regular.to_regular ↑a = a

def heyting.regular.gi {α : Type u_1} [heyting_algebra α] :

galois_insertion ⇑heyting.regular.to_regular coe

The Galois insertion between regular.to_regular and coe.

Equations

heyting.regular.gi = {choice := λ (a : α) (ha : ↑(⇑heyting.regular.to_regular a) ≤ a), ⟨a, _⟩, gc := _, le_l_u := _, choice_eq := _}

@[protected, instance]

def heyting.regular.lattice {α : Type u_1} [heyting_algebra α] :

lattice (heyting.regular α)

Equations

heyting.regular.lattice = heyting.regular.gi.lift_lattice

@[simp, norm_cast]

theorem heyting.regular.coe_sup {α : Type u_1} [heyting_algebra α] (a b : heyting.regular α) :

↑(a ⊔ b) = (↑a ⊔ ↑b)ᶜᶜ

@[protected, instance]

def heyting.regular.boolean_algebra {α : Type u_1} [heyting_algebra α] :

boolean_algebra (heyting.regular α)

Equations

heyting.regular.boolean_algebra = {sup := lattice.sup heyting.regular.lattice, le := lattice.le heyting.regular.lattice, lt := lattice.lt heyting.regular.lattice, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, le_sup_left := _, le_sup_right := _, sup_le := _, inf := lattice.inf heyting.regular.lattice, inf_le_left := _, inf_le_right := _, le_inf := _, le_sup_inf := _, compl := has_compl.compl heyting.regular.has_compl, sdiff := λ (x y : heyting.regular α), distrib_lattice.inf x yᶜ, himp := has_himp.himp heyting.regular.has_himp, top := bounded_order.top heyting.regular.bounded_order, bot := bounded_order.bot heyting.regular.bounded_order, inf_compl_le_bot := _, top_le_sup_compl := _, le_top := _, bot_le := _, sdiff_eq := _, himp_eq := _}

@[simp, norm_cast]

theorem heyting.regular.coe_sdiff {α : Type u_1} [heyting_algebra α] (a b : heyting.regular α) :

↑(a \ b) = ↑a ⊓ (↑b)ᶜ

theorem heyting.is_regular_of_boolean {α : Type u_1} [boolean_algebra α] (a : α) :

heyting.is_regular a

@[nolint]

theorem heyting.is_regular_of_decidable (p : Prop) [decidable p] :

heyting.is_regular p

A decidable proposition is intuitionistically Heyting-regular.