Documentation

Mathlib.Order.Heyting.Regular

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 #

References #

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

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

Equations
theorem Heyting.IsRegular.eq {α : Type u_1} [HasCompl α] {a : α} :
IsRegular aa = a
theorem Heyting.IsRegular.inf {α : Type u_1} [HeytingAlgebra α] {a b : α} (ha : IsRegular a) (hb : IsRegular b) :
IsRegular (ab)
theorem Heyting.IsRegular.himp {α : Type u_1} [HeytingAlgebra α] {a b : α} (ha : IsRegular a) (hb : IsRegular b) :
@[reducible, inline]
abbrev BooleanAlgebra.ofRegular {α : Type u_1} [HeytingAlgebra α] (h : ∀ (a : α), Heyting.IsRegular (aa)) :

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) [HeytingAlgebra α] :
Type u_1

The boolean algebra of Heyting regular elements.

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

The coercion Regular α → α

Equations
theorem Heyting.Regular.prop {α : Type u_1} [HeytingAlgebra α] (a : Regular α) :
@[simp]
theorem Heyting.Regular.coe_inj {α : Type u_1} [HeytingAlgebra α] {a b : Regular α} :
a = b a = b
instance Heyting.Regular.top {α : Type u_1} [HeytingAlgebra α] :
Equations
instance Heyting.Regular.bot {α : Type u_1} [HeytingAlgebra α] :
Equations
instance Heyting.Regular.inf {α : Type u_1} [HeytingAlgebra α] :
Equations
instance Heyting.Regular.himp {α : Type u_1} [HeytingAlgebra α] :
Equations
Equations
@[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 α) :
(ab) = ab
@[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)
@[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

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

Equations
@[simp]
theorem Heyting.Regular.coe_toRegular {α : Type u_1} [HeytingAlgebra α] (a : α) :
@[simp]
theorem Heyting.Regular.toRegular_coe {α : Type u_1} [HeytingAlgebra α] (a : Regular α) :
toRegular a = a

The Galois insertion between Regular.toRegular and coe.

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

A decidable proposition is intuitionistically Heyting-regular.